SAT-to-SAT: Declarative Extension of SAT Solvers with New Propagators
Authors: Tomi Janhunen, Shahab Tasharrofi, Eugenia Ternovska
AAAI 2016 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | Experimental Results: We implement our methods on top of Glucose (Audemard and Simon 2009) and show that introducing new reasoning mechanisms hugely boosts the solving time of a problem. Thus, we show that our new paradigm to solve problems by also describing their reasoning methods outperforms the existing ground and solve paradigm. |
| Researcher Affiliation | Academia | Tomi Janhunen and Shahab Tasharrofi {tomi.janhunen,shahab.tasharrofi}@aalto.fi Helsinki Institute for Information Technology HIIT Department of Computer Science Aalto University, FI-00076 AALTO, Finland Eugenia Ternovska ter@cs.sfu.ca Computing Science Department Simon Fraser University, Burnaby, BC, Canada |
| Pseudocode | Yes | Algorithm 1 shows that SAT-to-SAT extends CDCL by introducing a new propagation handling procedure S2Sprop in the common CDCL search method. |
| Open Source Code | No | The paper states 'We have implemented SAT-to-SAT by extending GLUCOSE 3.0' and 'We also use SATGRND (Gebser et al. 2015) as our grounder,' but it does not provide a link or explicit statement for the open-source release of the SAT-to-SAT solver or the P[R] language implementation. |
| Open Datasets | No | The instances of Hamiltonian path are randomly generated using a random planar graph generator that is developed as part of LEDA (Mehlhorn and N aher 1992) library. |
| Dataset Splits | No | The paper presents 'Hamiltonian Path Instances' and their solving times in Table 1 but does not specify any training, validation, or test dataset splits. |
| Hardware Specification | Yes | Table 1 summarizes the results of running our experiments on an Ubuntu 14.04 Linux desktop with kernel version 3.13.0-57, an Intel(R) Core(TM) i5-4590 CPU running at 3.30GHz, plus 16GB of memory. |
| Software Dependencies | Yes | We have implemented SAT-to-SAT by extending GLUCOSE 3.0 (Audemard and Simon 2009). Our Glucose extension closely matches Algorithm 1 except for using fast data structures such as Bit Sets to expedite problem solving. We also use SATGRND (Gebser et al. 2015) as our grounder. |
| Experiment Setup | Yes | The time limit for each instance is set at 15 minutes and the # columns in Table 1 show the number of instances that were solved using a particular encoding in 15 minutes. |