Chaff

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 471 articles )

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

1 2 3 ... 22 23 24 next

  1. Cabodi, G.; Camurati, P.E.; Mishchenko, A.; Palena, M.; Pasini, P.: SAT solver management strategies in IC3: an experimental approach (2017)
  2. de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
  3. Lagniez, Jean-Marie; Marquis, Pierre: On preprocessing techniques and their impact on propositional model counting (2017)
  4. Balyo, Tomáš; Biere, Armin; Iser, Markus; Sinz, Carsten: SAT race 2015 (2016)
  5. Beame, Paul; Beck, Chris; Impagliazzo, Russell: Time-space trade-offs in resolution: superpolynomial lower bounds for superlinear space (2016)
  6. Blanchette, Jasmin Christian; Fleury, Mathias; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2016)
  7. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: model representation (2016)
  8. Bright, Curtis; Ganesh, Vijay; Heinle, Albert; Kotsireas, Ilias; Nejati, Saeed; Czarnecki, Krzysztof: mathcheck2: a SAT+CAS verifier for combinatorial conjectures (2016)
  9. Hamadi, Youssef; Jabbour, Saïd; Saïs, Lakhdar: What we can learn from conflicts in propositional satisfiability (2016)
  10. Lierler, Yuliya; Truszczynski, Miroslaw: On abstract modular inference systems and solvers (2016)
  11. López, Nacho; Miret, Josep M.; Fernández, Cèsar: Non existence of some mixed Moore graphs of diameter 2 using SAT (2016)
  12. Monniaux, David: A survey of satisfiability modulo theory (2016)
  13. 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)
  14. Vaisman, Radislav; Botev, Zdravko I.; Ridder, Ad: Sequential Monte Carlo for counting vertex covers in general graphs (2016)
  15. Veksler, Michael; Strichman, Ofer: Learning general constraints in CSP (2016)
  16. Wang, Timothy; Jobredeaux, Romain; Pantel, Marc; Garoche, Pierre-Loic; Feron, Eric; Henrion, Didier: Credible autocoding of convex optimization algorithms (2016)
  17. Zhang, Hantao: An experiment with satisfiability modulo SAT (2016)
  18. Aziz, Rehan Abdul; Chu, Geoffrey; Muise, Christian; Stuckey, Peter: $\#\existsSAT$: projected model counting (2015)
  19. Balint, Adrian; Belov, Anton; Järvisalo, Matti; Sinz, Carsten: Overview and analysis of the SAT challenge 2012 solver competition (2015) ioport
  20. Balyo, Tomáš; Sanders, Peter; Sinz, Carsten: HordeSat: a massively parallel portfolio SAT solver (2015)

1 2 3 ... 22 23 24 next


Further publications can be found at: http://www.princeton.edu/~chaff/publication.html