zChaff is an implementation of the well known CHAFF, an algorithm for solving satisfiability (SAT) problems. It won the Best Complete Solver in both industrial and handmade benchmark categories in the SAT 2002 Competition, and the Best Complete Solver in the industrial benchmark in the SAT 2004 Competition. It is a popular solver and can be compiled into a linkable library for easy integration with user applications.

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

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

1 2 next

  1. Bikov, Aleksandar; Nenov, Nedyalko: On the independence number of ((3,3))-Ramsey graphs and the Folkman number (F_e(3,3;4)) (2020)
  2. Guo, Wen-Sheng; Yang, Guo-Wu; Hung, William N. N.; Song, Xiaoyu: Complete Boolean satisfiability solving algorithms based on local search (2013)
  3. Armand, Michael; Faure, Germain; Grégoire, Benjamin; Keller, Chantal; Théry, Laurent; Werner, Benjamin: A modular integration of SAT/SMT solvers to Coq through proof witnesses (2011)
  4. Armand, Michaël; Grégoire, Benjamin; Spiwack, Arnaud; Théry, Laurent: Extending Coq with imperative features and its application to SAT verification (2010)
  5. Shilov, N. V.; Bodin, E. V.; Shilova, S. O.: Guided tour inside F@BOOL@: a case-study for a SAT-based verifying compiler (2010)
  6. Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael: Propagation via lazy clause generation (2009)
  7. Weber, Tjark; Amjad, Hasan: Efficiently checking propositional refutations in HOL theorem provers (2009)
  8. Yadgar, Avi; Grumberg, Orna; Schuster, Assaf: Hybrid BDD and All-SAT method for model checking (2009)
  9. Biere, Armin: PicoSAT essentials (2008)
  10. Bruni, Renato; Santori, Andrea: New updating criteria for conflict-based branching heuristics in DPLL algorithms for satisfiability (2008)
  11. Dunets, Andriy; Schellhorn, Gerhard; Reif, Wolfgang: Automating algebraic specifications of non-freely generated data types (2008)
  12. Narain, Sanjai; Levin, Gary; Malik, Sharad; Kaul, Vikram: Declarative infrastructure configuration synthesis and debugging (2008) ioport
  13. Vasudevan, Shobha; Viswanath, Vinod; Abraham, Jacob A.; Tu, JiaJin: Sequential equivalence checking between system level and RTL descriptions (2008) ioport
  14. Bryant, Randal E.; Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer; Brady, Bryan: Deciding bit-vector arithmetic with abstraction (2007)
  15. Esponda, Fernando; Ackley, Elena S.; Helman, Paul; Jia, Haixia; Forrest, Stephanie: Protecting data privacy through hard-to-reverse negative databases (2007) ioport
  16. Jing, Minge; Zhou, Dian; Tang, Pushan; Zhou, Xiaofang; Zhang, Hua: Solving SAT problem by heuristic polarity decision-making algorithm (2007)
  17. Law, Yat Chiu; Lee, Jimmy H. M.; Smith, Barbara M.: Automatic generation of redundant models for permutation constraint satisfaction problems (2007)
  18. Bailleux, Olivier; Boufkhad, Yacine; Roussel, Olivier: A translation of pseudo-Boolean constraints to SAT (2006)
  19. Drechsler, Rolf; Fey, Görschwin: Automatic test pattern generation (2006)
  20. Fu, Zhaohui; Malik, Sharad: On solving the partial MAX-SAT problem (2006)

1 2 next