Zchaff2004

The Boolean Satisfiability Problem (SAT) is a well known NP-complete problem. While its complexity remains a source of many interesting questions for theoretical computer scientists, the problem has found many practical applications in recent years. The emergence of efficient SAT solvers which can handle large structured SAT instances has enabled the use of SAT solvers in diverse domains such as electronic design automation and artificial intelligence. These applications continue to motivate the development of faster and more robust SAT solvers. In this paper, we describe the popular SAT solver zchaff with a focus on recent developments.


References in zbMATH (referenced in 20 articles , 1 standard article )

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

  1. Hutter, Frank; Xu, Lin; Hoos, Holger H.; Leyton-Brown, Kevin: Algorithm runtime prediction: methods & evaluation (2014)
  2. Ansótegui, Carlos; Bofill, Miquel; Palahí, Miquel; Suy, Josep; Villaret, Mateu: Solving weighted CSPs with meta-constraints by reformulation into satisfiability modulo theories (2013)
  3. Ibaraki, Toshihide; Imamichi, Takashi; Koga, Yuichi; Nagamochi, Hiroshi; Nonobe, Koji; Yagiura, Mutsunori: Efficient branch-and-bound algorithms for weighted MAX-2-SAT (2011)
  4. Pipatsrisawat, Knot; Darwiche, Adnan: On the power of clause-learning SAT solvers as resolution engines (2011)
  5. Moha, Naouel; Sen, Sagar; Faucher, Cyril; Barais, Olivier; Jézéquel, Jean-Marc: Evaluation of Kermeta for solving graph-based problems (2010)
  6. Nadel, Alexander; Ryvchin, Vadim: Assignment stack shrinking (2010)
  7. Schewe, Lars: Nonrealizable minimal vertex triangulations of surfaces: showing nonrealizability using oriented matroids and satisfiability solvers (2010)
  8. Babić, Domagoj; Hu, Alan J.: Approximating the safely reusable set of learned facts (2009)
  9. Bokowski, Jürgen; Grünbaum, Branko; Schewe, Lars: Topological configurations $(n_4)$ exist for all $n\geq 17$ (2009)
  10. Pipatsrisawat, Knot; Darwiche, Adnan: Width-based restart policies for clause-learning satisfiability solvers (2009)
  11. Buss, Samuel R.; Hoffmann, Jan; Johannsen, Jan: Resolution trees with lemmas: resolution refinements that characterize DLL algorithms with clause learning (2008)
  12. Kullmann, Oliver: Present and future of practical SAT solving (2008)
  13. Narain, Sanjai; Levin, Gary; Malik, Sharad; Kaul, Vikram: Declarative infrastructure configuration synthesis and debugging (2008)
  14. Xu, L.; Hutter, F.; Hoos, H.H.; Leyton-Brown, K.: SATzilla: portfolio-based algorithm selection for SAT (2008)
  15. Esponda, Fernando; Ackley, Elena S.; Helman, Paul; Jia, Haixia; Forrest, Stephanie: Protecting data privacy through hard-to-reverse negative databases (2007)
  16. Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander: A scalable algorithm for minimal unsatisfiable core extraction (2006)
  17. Schewe, Lars: Generation of oriented matroids using satisfiability solvers (2006)
  18. Dershowitz, Nachum; Hanna, Ziyad; Nadel, Alexander: A clause-based heuristic for SAT solvers (2005)
  19. Mahajan, Yogesh S.; Fu, Zhaohui; Malik, Sharad: Zchaff2004: An efficient SAT solver (2005)
  20. Zarpas, Emmanuel: Benchmarking SAT solvers for bounded model checking (2005)


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