The configurable SAT solver challenge (CSSC)
From MaRDI portal
Publication:502389
DOI10.1016/J.ARTINT.2016.09.006zbMATH Open1402.68161arXiv1505.01221OpenAlexW2962929300WikidataQ59585860 ScholiaQ59585860MaRDI QIDQ502389FDOQ502389
Authors: Adrian Balint, Sam Bayless, Holger H. Hoos, Frank Hutter, Marius Lindauer, Kevin Leyton-Brown 
Publication date: 5 January 2017
Published in: Artificial Intelligence (Search for Journal in Brave)
Abstract: It is well known that different solution strategies work well for different types of instances of hard combinatorial problems. As a consequence, most solvers for the propositional satisfiability problem (SAT) expose parameters that allow them to be customized to a particular family of instances. In the international SAT competition series, these parameters are ignored: solvers are run using a single default parameter setting (supplied by the authors) for all benchmark instances in a given track. While this competition format rewards solvers with robust default settings, it does not reflect the situation faced by a practitioner who only cares about performance on one particular application and can invest some time into tuning solver parameters for this application. The new Configurable SAT Solver Competition (CSSC) compares solvers in this latter setting, scoring each solver by the performance it achieved after a fully automated configuration step. This article describes the CSSC in more detail, and reports the results obtained in its two instantiations so far, CSSC 2013 and 2014.
Full work available at URL: https://arxiv.org/abs/1505.01221
Recommendations
- SATenstein: automatically building local search SAT solvers from components
- SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
- MaxSAT by improved instance-specific algorithm configuration
- Paramils: an automatic algorithm configuration framework
- SATzilla: portfolio-based algorithm selection for SAT
Cites Work
- Theory and Applications of Satisfiability Testing
- Paramils: an automatic algorithm configuration framework
- SATenstein: automatically building local search SAT solvers from components
- Controlling a solver execution with the runsolver Tool
- Random forests
- Title not available (Why is that?)
- The complexity of theorem-proving procedures
- SATzilla: portfolio-based algorithm selection for SAT
- Algorithm runtime prediction: methods \& evaluation
- Conflict-driven answer set solving: from theory to practice
- Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
- Stochastic local search. Foundations and applications.
- Principles and Practice of Constraint Programming – CP 2004
- Automated testing and debugging of SAT and QBF solvers
- Blocked clause elimination
- Tools and Algorithms for the Construction and Analysis of Systems
- Toward leaner binary-clause reasoning in a satisfiability solver
- Theory and applications of satisfiability testing -- SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19--22, 2011. Proceedings
- Efficient CNF simplification based on binary implication graphs
- Theory and applications of satisfiability testing -- SAT 2012. 15th international conference, Trento, Italy, June 17--20, 2012. Proceedings
- Choosing probability distributions for stochastic local search and the role of make versus break
- Captain Jack: new variable selection heuristics in local search for SAT
- Structural Abstraction of Software Verification Conditions
- Theory and Applications of Satisfiability Testing
- Theory and applications of satisfiability testing -- SAT 2009. 12th international conference, SAT 2009, Swansea, UK, June 30--July 3, 2009. Proceedings
- Detecting cardinality constraints in CNF
- On the resolution complexity of graph non-isomorphism
Cited In (18)
- How we designed winning algorithms for abstract argumentation and which insight we attained
- SATenstein: automatically building local search SAT solvers from components
- A refined branching algorithm for the maximum satisfiability problem
- MaxSAT by improved instance-specific algorithm configuration
- Synthesis of domain specific CNF encoders for bit-vector solvers
- Instance-specific algorithm configuration
- Targeted configuration of an SMT solver
- Meta-heuristics and artificial intelligence
- Title not available (Why is that?)
- Boosting evolutionary algorithm configuration
- On the importance of domain model configuration for automated planning engines
- An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses
- SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
- Speeding up neural network robustness verification via algorithm configuration and an optimised mixed integer linear programming solver portfolio
- Paramils: an automatic algorithm configuration framework
- Reoptimization of minimum latency problem revisited: don't panic when asked to revisit the route after local modifications
- Efficient benchmarking of algorithm configurators via model-based surrogates
- SpyBug: automated bug detection in the configuration space of SAT solvers
Uses Software
This page was built for publication: The configurable SAT solver challenge (CSSC)
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q502389)
