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

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

1 2 3 ... 28 29 30 next

  1. Banković, Milan; Marić, Filip: Faradžev Read-type enumeration of non-isomorphic CC systems (2021)
  2. Devriendt, Jo; Gleixner, Ambros; Nordström, Jakob: Learn to relax: integrating (0-1) integer linear programming with pseudo-Boolean conflict-driven search (2021)
  3. Giráldez-Cru, Jesús; Levy, Jordi: Popularity-similarity random SAT formulas (2021)
  4. Kyrillidis, Anastasios; Shrivastava, Anshumali; Vardi, Moshe Y.; Zhang, Zhiwei: Solving hybrid Boolean constraints in continuous space via multilinear Fourier expansions (2021)
  5. Robbins, Ed; King, Andy; Howe, Jacob M.: Backjumping is exception handling (2021)
  6. Witzig, Jakob; Berthold, Timo; Heinz, Stefan: Computational aspects of infeasibility analysis in mixed integer programming (2021)
  7. Witzig, Jakob; Gleixner, Ambros: Conflict-driven heuristics for mixed integer programming (2021)
  8. Achterberg, Tobias; Bixby, Robert E.; Gu, Zonghao; Rothberg, Edward; Weninger, Dieter: Presolve reductions in mixed integer programming (2020)
  9. Berkholz, Christoph; Nordström, Jakob: Supercritical space-width trade-offs for resolution (2020)
  10. Bromberger, Martin; Sturm, Thomas; Weidenbach, Christoph: A complete and terminating approach to linear integer solving (2020)
  11. Dodaro, Carmine; Ricca, Francesco: The external interface for extending WASP (2020)
  12. Drechsler, Rolf (ed.); Soeken, Mathias (ed.): Advanced Boolean techniques. Selected papers from the 13th international workshop on Boolean problems, Bremen, Germany, September 19--21, 2018 (2020)
  13. Hebrard, Emmanuel; Katsirelos, George: Constraint and satisfiability reasoning for graph coloring (2020)
  14. Kiesl, Benjamin; Rebola-Pardo, Adrián; Heule, Marijn J. H.; Biere, Armin: Simulating strong practical proof systems with extended resolution (2020)
  15. Kochemazov, Stepan: Improving implementation of SAT competitions 2017--2019 winners (2020)
  16. Lagniez, Jean-Marie; Lonca, Emmanuel; Marquis, Pierre: Definability for model counting (2020)
  17. Lammich, Peter: Efficient verified (UN)SAT certificate checking (2020)
  18. Le Berre, Daniel; Marquis, Pierre; Wallon, Romain: On weakening strategies for PB solvers (2020)
  19. Li, Chu-Min; Xiao, Fan; Luo, Mao; Manyà, Felip; Lü, Zhipeng; Li, Yu: Clause vivification by unit propagation in CDCL SAT solvers (2020)
  20. Li, Chunxiao; Fleming, Noah; Vinyals, Marc; Pitassi, Toniann; Ganesh, Vijay: Towards a complexity-theoretic understanding of restarts in SAT solvers (2020)

1 2 3 ... 28 29 30 next


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