Generating Hard Random Boolean Formulas and Disjunctive Logic Programs
Authors: Giovanni Amendola, Francesco Ricca, Miroslaw Truszczynski
IJCAI 2017 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We provide theoretical bounds for the phase transition region in the new model, and show experimentally the presence of the easy-hard-easy pattern. Importantly, we show that the model is well suited for assessing solvers tuned to real-world instances. Moreover, to the best of our knowledge, our model and results on random disjunctive logic programs are the first of their kind. |
| Researcher Affiliation | Academia | Giovanni Amendola University of Edinburgh, UK gamendol@exseed.ed.ac.uk Francesco Ricca University of Calabria, Italy ricca@mat.unical.it Miroslaw Truszczynski University of Kentucky, USA mirek@cs.uky.edu |
| Pseudocode | No | The paper describes mathematical models and transformations but does not include any pseudocode or algorithm blocks. |
| Open Source Code | No | The paper states: "Formulas were generated with a tool we developed in Java." However, it does not provide any link or explicit statement about making this tool open-source or publicly available. |
| Open Datasets | No | The paper generates random instances based on proposed models rather than using existing, publicly available datasets. Therefore, it does not provide access information for a training dataset. |
| Dataset Splits | No | The paper describes experiments on randomly generated instances and does not mention using standard training/validation/test splits of a fixed dataset for reproduction. |
| Hardware Specification | Yes | Experiments were run on a Debian Linux with 2.30GHz Intel Xeon E5-4610 v2 CPUs and 128GB of RAM. Each execution was constrained to one single core by using the taskset command. |
| Software Dependencies | Yes | the SAT solvers GLUCOSE 4.0 [Audemard et al., 2013] LINGELING, version of 2015 [Biere, 2014], and KCNFS, version of SAT 07 competition [Dequen and Dubois, 2006]; the QBF solvers BQ-CEGAR1, AIGSOLVE [Pigorsch and Scholl, 2010]; RAREQS [Janota et al., 2016], and AQUA-S2V2 and the ASP solvers CLASP 3.1.3 [Gebser et al., 2007] and WASP 2.1 [Alviano et al., 2015], both paired with gringo 4.5.3. |
| Experiment Setup | Yes | All solvers were run in their default configurations. [...] Formulas were generated with a tool we developed in Java.The results are averaged over 128 samples of the same size. [...] To study the satisfiability of multi-component model instances (the location of the phase transition), we considered the setting with the number of variables (propositional atoms) fixed. [...] The x-axis gives the ratio of the numbers of clauses and variables (m/200), the y-axis shows the frequency of SAT. |