Breaking Symmetries in Quantified Graph Search: A Comparative Study
Authors: Mikoláš Janota, Markus Kirchweger, Tomáš Peitl, Stefan Szeider
AAAI 2025 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Table 2 shows the performance of the three main approaches on problem instances from Section 4, with a time limit of 4 hours for each instance. All solvers are run with a single thread. Table 3 shows the number of solved instances by each solver. |
| Researcher Affiliation | Academia | 1 Czech Technical University in Prague 2 Algorithms and Complexity Group, TU Wien, Austria |
| Pseudocode | Yes | Algorithm 1: A CEGAR-based 2-QBF solver |
| Open Source Code | Yes | Solvers and benchmark generators are included in supplementary material in the versions used in this paper (Janota et al. 2025). For detailed instructions on how to create the encodings and use the solvers, as well as for up-to-date version of solvers, visit https://satmodulo-symmetries.readthedocs.io/en/latest/applications#qbf. |
| Open Datasets | No | The paper describes problem classes for graph search and mentions 'generator scripts' for instances, but does not refer to specific pre-existing public datasets or provide access information for them. |
| Dataset Splits | No | The paper evaluates solvers on generated graph problem instances rather than using traditional machine learning datasets with explicit training/test/validation splits. |
| Hardware Specification | Yes | We evaluated all solvers on all benchmark problems, on a cluster of machines with different processors2, running Ubuntu 18.04 on Linux 4.15.3 ... 2Intel Xeon {E5540, E5649, E5-2630 v2, E5-2640 v4}@ at most 2.60 GHz, AMD EPYC 7402@2.80GHz |
| Software Dependencies | Yes | We use Ca Di Ca L (Biere et al. 2020) as the underlying SAT solver... Qfun (Janota 2018b), CQesto (Janota 2018a) and Qute (Peitl, Slivovsky, and Szeider 2019)... running Ubuntu 18.04 on Linux 4.15. |
| Experiment Setup | Yes | We evaluated all solvers on all benchmark problems... with a time limit of 4 hours for each instance. All solvers are run with a single thread. |