Using Symmetries to Lift Satisfiability Checking
Authors: Pierre Carbonnelle, Gottfried Schenner, Maurice Bruynooghe, Bart Bogaerts, Marc Denecker
AAAI 2024 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Our experimental evaluation shows large speedups for generative configuration problems. The top half of Table ?? shows results with Z3 (with automatic translation of the sentence), the bottom half with the OR-tools solver8 (with manual translation). |
| Researcher Affiliation | Collaboration | 1KU Leuven, Belgium 2Siemens, Austria 3Vrije Universiteit Brussels, Belgium |
| Pseudocode | No | The paper includes Table 1 which details transformations, but it does not contain structured pseudocode or algorithm blocks. |
| Open Source Code | Yes | The source code of our examples is available on Git Lab7. 7https://gitlab.com/pierre.carbonnelle/idp-z3-generative |
| Open Datasets | Yes | We evaluate our solving method on three representative GCP discussed in the literature: the House Configuration and Reconfiguration problem (Friedrich et al. 2011), the Organized Monkey Village (Reger, Suda, and Voronkov 2016) the Rack problem (Feinerer, Salzer, and Sisel 2011; Comploi-Taupe, Francescutto, and Schenner 2022) |
| Dataset Splits | No | The paper does not explicitly provide training/test/validation dataset splits or information on how data was partitioned for training and evaluation. |
| Hardware Specification | Yes | Tests were run using Z3 v4.12.1 on an Intel Core i7-8850H CPU at 2.60GHz with 12 cores, running Ubuntu 22.04 with 16 GB RAM. |
| Software Dependencies | Yes | Tests were run using Z3 v4.12.1... We run a modified version of IDP-Z3 v0.10.8 on Python 3.10. |
| Experiment Setup | Yes | A problem is solved iteratively, starting with empty lifted domains. Given a domain, the lifted sentence is reduced to a propositional sentence and its satisfiability is determined with a standard satisfiability solver capable of arithmetic reasoning. If the sentence is unsatisfiable with this domain, the sentence is reduced to a minimal unsatisfiable formula (Lynce and Marques-Silva 2004), and the domains of the types used in that formula are extended with one element. This process is repeated until a model of the sentence is found (it does not terminate if the original sentence is unsatisfiable for any domain size, unless one imposes an upper limit on the size of lifted domains). |