SAT-Based Tree Decomposition with Iterative Cascading Policy Selection

Authors: Hai Xia, Stefan Szeider

AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details

Reproducibility Variable Result LLM Response
Research Type Experimental We conducted our experiments over a comprehensive set of over 3000 benchmark graphs from various real-world applications. We randomly split these graphs 80 : 20 into a training set on which we performed the offline training and a test set on which we report the observed performance. The primary objective function counts the total sum of improvements (TΣ) of treewidth, a good proxy for the number of instances whose treewidth could be reduced (T#). The standard hand-tuned configuration used by Fichte, Lodha, and Szeider (2017) gives TΣ = 398 in the default 7800-second timeout they used for their experiments. With the clustering-based offline configuration, this value increases to 456 and 500, depending on whether the configuration is selected with Auto Folio (Lindauer et al. 2015) or the constrained-clustering model integrated by us.
Researcher Affiliation Academia Hai Xia, Stefan Szeider Algorithms and Complexity Group, TU Wien, Austria {hxia,sz}@ac.tuwien.ac.at
Pseudocode Yes Algorithm 1: Dynamic ICP
Open Source Code Yes We provide an external link for source code and detailed results (Xia and Szeider 2023).
Open Datasets Yes To obtain a comprehensive evaluation, we collected a large set of benchmark graphs from various collections (see Table 2). Table 2: Instances URLs (https://) functions sdcc.sourceforge.net PACE16 pacechallenge.org/2016/treewidth PACE17 pacechallenge.org/2017/treewidth UAI www.ics.uci.edu/ dechter/software.html Roadnet www.diag.uniroma1.it/challenge9 TWlib webspace.science.uu.nl/ bodla101/treewidthlib
Dataset Splits Yes After the whole data set is split randomly into a training set (80%) and a test set (20%), the training set and test set have 2664 and 667 instances, respectively.
Hardware Specification Yes All experiments are carried out on a Linux (Ubuntu 18.04.6 LTS) Sun Grid Engine cluster with 3 nodes, where each node has two AMD EPYC 7402 CPUs (each has 24 cores with a frequency of 2.80GHz).
Software Dependencies Yes Components related to TW-SLIM and Auto Folio run on Python 2.7.5 and Python 3.5, respectively. All other components run on Python 3.9.12. For a fair comparison, we set... the heuristic for computing the initial TD to HTD (version: v0.9.5beta)... the local solver to Jdrasil... and the SAT solver to Glucose.
Experiment Setup Yes Table 1: Key parameters and their meaning local budget (lb) budget of vertices for SLIM local time (lt) timeout for the local improvement SAT time (st) call timeout for the SAT solver switch flag (sf) replace GS if w(G S) = w(G) Table 3: The setting of SMAC Parameter name Value configuration lb [50, 300], 100 as default lt [90, 5000], 1800 as default st [90, 5000], 900 as default sf {0, 1}, 1 as default wallclock-limit 48 hours cutoff-time 4 hours memory limit 300 GB objective total improvements of widths limit resources False model type Gaussian process acquisition function expected improvement random state 42