Satisfiability Modulo User Propagators
Authors: Katalin Fazekas, Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, Armin Biere
JAIR 2024 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | To show that our interface is effective and efficient in varied use cases, we extended Ca Di Ca L (Biere et al., 2020, 2024), a state-of-the-art incremental SAT solver which implements the IPASIR interface, with IPASIR-UP. Our extension required 800 lines of C++ code in Ca Di Ca L, accompanied with another 700 lines in its model based tester. We provide an evaluation on two representative use cases: enumerating graphs with certain properties via SAT Modulo Symmetries (Kirchweger & Szeider, 2021), and integrating Ca Di Ca L as the main CDCL(T ) SAT engine in the SMT solver cvc5 (Barbosa et al., 2022). All evaluated tools of our experiments are available at Zenodo (Fazekas et al., 2024a). 5.1 Experiments with SMS 5.2 Experiments with SMT |
| Researcher Affiliation | Academia | Katalin Fazekas EMAIL TU Wien, Vienna, Austria Aina Niemetz EMAIL Mathias Preiner EMAIL Stanford University, Stanford, USA Markus Kirchweger EMAIL Stefan Szeider EMAIL TU Wien, Vienna, Austria Armin Biere EMAIL University of Freiburg, Freiburg, Germany |
| Pseudocode | Yes | Algorithm 1: CDCL loop with a connected external propagator (simplified). Algorithm 2: External propagation within a CDCL SAT solver (simplified). Algorithm 3: Addition of external clauses during the CDCL loop (simplified). Algorithm 4: Decision making with the external propagator (simplified). |
| Open Source Code | Yes | 1. The latest version of our IPASIR-UP implementation in Ca Di Ca L is available at https://github.com/arminbiere/cadical. |
| Open Datasets | Yes | We evaluate the overall performance of cvc5-ipasirup against cvc5 version 1.1.1 on all non-incremental and incremental benchmarks of the 2024 release of SMT-LIB (Preiner et al., 2024a, 2024b). |
| Dataset Splits | No | The paper mentions using SMT-LIB benchmarks and SMS graph generation tasks, but does not provide specific training/test/validation splits in terms of percentages or sample counts. It refers to incremental/non-incremental divisions within SMT-LIB. |
| Hardware Specification | Yes | All experiments with SMS ran on a cluster equipped with Intel Xeon E5-2640v4 CPUs at 2.40 GHz. ... We ran this experiment on a cluster equipped with AMD Ryzen 9 7950X CPUs and allocated one CPU core, 8GB of RAM and a time limit of 300 seconds for each solver and benchmark pair (unknown answers were treated as timeouts). |
| Software Dependencies | Yes | To show that our interface is effective and efficient in varied use cases, we extended Ca Di Ca L (Biere et al., 2020, 2024), a state-of-the-art incremental SAT solver which implements the IPASIR interface, with IPASIR-UP. ... We integrated Ca Di Ca L with the IPASIR-UP extension as main CDCL(T ) SAT engine of cvc5 while fully utilizing the IPASIR-UP notification and callback interface... The full integration of Ca Di Ca L as CDCL(T ) SAT engine of cvc5 required about 600 lines of C++ code on top of cvc5 1.1.1. |
| Experiment Setup | Yes | For Ca Di Ca L, the default configuration propagates literals, makes the symmetry breaking clauses not forgettable, and exhaustively enumerates all graphs using the IPASIR-UP interface when possible. Configuration enum-IPASIR propagates literals and adds symmetry-breaking clauses via IPASIR-UP but uses IPASIR for solution enumeration. Configuration no-prop corresponds to default without propagating literals but learning the clause immediately. Configuration no-inpro corresponds to default without inprocessing on the nonobserved variables (i.e., option inprocessing of Ca Di Ca L is turned off). Configuration forgettable corresponds to default but clauses added via the IPASIR-UP interface are forgettable. For clingo, we either add the clauses as redundant (configuration red), i.e., the symmetry-breaking clauses are part of the clause-deletion policy, or the clauses are irredundant (configuration irred). ... we allocated one CPU core, 8GB of RAM and a time limit of 300 seconds for each solver and benchmark pair (unknown answers were treated as timeouts). |