Computing Optimal Hypertree Decompositions with SAT
Authors: Andre Schidler, Stefan Szeider
IJCAI 2021 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We utilize this characterization to generate a new SAT encoding that we evaluate on an extensive set of benchmark instances. We compare it to state-of-the-art exact methods for computing optimal hypertree width. Our results show that the encoding based on the new characterization is not only significantly more compact than known encodings but also outperforms the other methods. |
| Researcher Affiliation | Academia | Andr e Schidler and Stefan Szeider Algorithms and Complexity Group, TU Wien, Vienna, Austria {aschidler,sz}@ac.tuwien.ac.at |
| Pseudocode | No | The paper does not contain structured pseudocode or algorithm blocks (clearly labeled algorithm sections or code-like formatted procedures). |
| Open Source Code | Yes | code4 of the experiments are available online. github.com/ASchidler/htdsmt, doi.org/10.5281/zenodo.4742100 |
| Open Datasets | Yes | We tested against the full set of Hyperbench11 instances. Hyperbench consists of instances gathered from various database queries and constraint satisfaction problem instances [Fischl et al., 2019; Bonifati et al., 2017; Bonifati et al., 2019; Pottinger and Halevy, 2001; Benedikt et al., 2017], for which hypertree width is of practical relevance. |
| Dataset Splits | No | The paper does not provide specific dataset split information (exact percentages, sample counts, citations to predefined splits, or detailed splitting methodology) needed to reproduce the data partitioning. |
| Hardware Specification | Yes | We used servers with two Intel Xeon E5540 CPUs, each running at 2.53 GHz per core. The servers used Ubuntu 18.04. Each run was limited to thirty minutes and 8 GB RAM. |
| Software Dependencies | Yes | We implemented the improved encoding presented in Section 4 using Pysat 1.6.05 and refer to it as Htd LEO... Both versions were run using Python 3.8.0... Optimathsat 1.7.28 was used for the SMT encodings... We used Glucose 3 for SAT instances... Max SAT instances were solved by Uwr Max SAT9... |
| Experiment Setup | Yes | For the SAT encoding, we start at an initial heuristically computed width. This width is then decremented until the formula is unsatisfiable. |