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 21 articles , 1 standard article )

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

1 2 next

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

1 2 next

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