Chaff:engineering an efficient SAT solver. Boolean Satisfiability is probably the most studied of combinatorial optimization/search problems. Significant effort has been devoted to trying to provide practical solutions to this problem for problem instances encountered in a range of applications in Electronic Design Automation (EDA), as well as in Artificial Intelligence (AI). This study has culminated in the development of several SAT packages, both proprietary and in the public domain (e.g. GRASP, SATO) which find significant use in both research and industry. Most existing complete solvers are variants of the Davis-Putnam (DP) search algorithm. In this paper we describe the development of a new complete solver, Chaff, which achieves significant performance gains through careful engineering of all aspects of the search - especially a particularly efficient implementation of Boolean constraint propagation (BCP) and a novel low overhead decision strategy. Chaff has been able to obtain one to two orders of magnitude performance improvement on difficult SAT benchmarks in comparison with other solvers (DP or otherwise), including GRASP and SATO.

References in zbMATH (referenced in 483 articles )

Showing results 1 to 20 of 483.
Sorted by year (citations)

1 2 3 ... 23 24 25 next

  1. Beame, Paul; Beck, Chris; Impagliazzo, Russell: Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space (2016)
  2. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  3. Hamadi, Youssef; Jabbour, Saïd; Saïs, Lakhdar: What we can learn from conflicts in propositional satisfiability (2016)
  4. Lierler, Yuliya; Truszczynski, Miroslaw: On abstract modular inference systems and solvers (2016)
  5. López, Nacho; Miret, Josep M.; Fernández, Cèsar: Non existence of some mixed Moore graphs of diameter 2 using SAT (2016)
  6. Schnell, Alexander; Hartl, Richard F.: On the efficient modeling and solution of the multi-mode resource-constrained project scheduling problem with generalized precedence relations (2016)
  7. Vaisman, Radislav; Botev, Zdravko I.; Ridder, Ad: Sequential Monte Carlo for counting vertex covers in general graphs (2016)
  8. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  9. Aziz, Rehan Abdul; Chu, Geoffrey; Muise, Christian; Stuckey, Peter: $\#\existsSAT$: projected model counting (2015)
  10. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015)
  11. Balyo, Tomáš; Sanders, Peter; Sinz, Carsten: HordeSat: a massively parallel portfolio SAT solver (2015)
  12. Berger, Ulrich; Lawrence, Andrew; Forsberg, Fredrik Nordvall; Seisenberger, Monika: Extracting verified decision procedures: DPLL and resolution (2015)
  13. Biere, Armin; Fröhlich, Andreas: Evaluating CDCL variable scoring schemes (2015)
  14. Bilauca, Mihai; Gange, Graeme; Healy, Patrick; Marriott, Kim; Moulder, Peter; Stuckey, Peter J.: Automatic minimal-height table layout (2015)
  15. Bonacina, Maria Paola; Furbach, Ulrich; Sofronie-Stokkermans, Viorica: On first-order model-based reasoning (2015)
  16. Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
  17. Cabodi, Gianpiero; Loiacono, Carmelo; Vendraminetto, Danilo: Optimization techniques for Craig interpolant compaction in unbounded model checking (2015)
  18. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: Solving strong controllability of temporal problems with uncertainty using SMT (2015)
  19. Cimatti, Alessandro; Micheli, Andrea; Roveri, Marco: An SMT-based approach to weak controllability for disjunctive temporal problems with uncertainty (2015)
  20. De Cat, Broes; Denecker, Marc; Bruynooghe, Maurice; Stuckey, Peter: Lazy model expansion: interleaving grounding with search (2015)

1 2 3 ... 23 24 25 next

Further publications can be found at: