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.
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
- scientific article; zbMATH DE number 2050711 (Why is no real title available?)
- Algorithm runtime prediction: methods \& evaluation
- Automated testing and debugging of SAT and QBF solvers
- Blocked clause elimination
- Captain Jack: new variable selection heuristics in local search for SAT
- Choosing probability distributions for stochastic local search and the role of make versus break
- Conflict-driven answer set solving: from theory to practice
- Controlling a solver execution with the runsolver Tool
- Detecting cardinality constraints in CNF
- Efficient CNF simplification based on binary implication graphs
- Heavy-tailed phenomena in satisfiability and constraint satisfaction problems
- On the resolution complexity of graph non-isomorphism
- Paramils: an automatic algorithm configuration framework
- Principles and Practice of Constraint Programming – CP 2004
- Random forests
- SATenstein: automatically building local search SAT solvers from components
- SATzilla: portfolio-based algorithm selection for SAT
- Stochastic local search. Foundations and applications.
- Structural Abstraction of Software Verification Conditions
- The complexity of theorem-proving procedures
- Theory and Applications of Satisfiability Testing
- 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
- Theory and applications of satisfiability testing -- SAT 2011. 14th international conference, SAT 2011, Ann Arbor, MI, USA, June 19--22, 2011. Proceedings
- Theory and applications of satisfiability testing -- SAT 2012. 15th international conference, Trento, Italy, June 17--20, 2012. Proceedings
- Tools and Algorithms for the Construction and Analysis of Systems
- Toward leaner binary-clause reasoning in a satisfiability solver
Cited in
(18)- Instance-specific algorithm configuration
- On the importance of domain model configuration for automated planning engines
- MaxSAT by improved instance-specific algorithm configuration
- Boosting evolutionary algorithm configuration
- Paramils: an automatic algorithm configuration framework
- An improved algorithm for the \((n, 3)\)-MaxSAT problem: asking branchings to satisfy the clauses
- Meta-heuristics and artificial intelligence
- Targeted configuration of an SMT solver
- How we designed winning algorithms for abstract argumentation and which insight we attained
- Reoptimization of minimum latency problem revisited: don't panic when asked to revisit the route after local modifications
- SATenstein: automatically building local search SAT solvers from components
- Speeding up neural network robustness verification via algorithm configuration and an optimised mixed integer linear programming solver portfolio
- Efficient benchmarking of algorithm configurators via model-based surrogates
- scientific article; zbMATH DE number 7625207 (Why is no real title available?)
- SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers
- Synthesis of domain specific CNF encoders for bit-vector solvers
- SpyBug: automated bug detection in the configuration space of SAT solvers
- A refined branching algorithm for the maximum satisfiability problem
Describes a project that uses
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)
