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

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

1 2 3 ... 25 26 27 next

  1. Belahcène, K.; Labreuche, C.; Maudet, N.; Mousseau, V.; Ouerdane, W.: An efficient SAT formulation for learning multiple criteria non-compensatory sorting rules from examples (2018)
  2. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  3. Blanchette, Jasmin Christian; Fleury, Mathias; Lammich, Peter; Weidenbach, Christoph: A verified SAT solver framework with learn, forget, restart, and incrementality (2018)
  4. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  5. Kreter, Stefan; Schutt, Andreas; Stuckey, Peter J.; Zimmermann, Jürgen: Mixed-integer linear programming and constraint programming formulations for solving resource availability cost problems (2018)
  6. Lauria, Massimo: Cliques enumeration and tree-like resolution proofs (2018)
  7. Lauria, Massimo: A note about $k$-DNF resolution (2018)
  8. Lyu, Yinrun; Chen, Li; Zhang, Changyou; Qu, Dacheng; Min-Allah, Nasro; Wang, Yongji: An interleaved depth-first search method for the linear optimization problem with disjunctive constraints (2018)
  9. Marques-Silva, Joao; Malik, Sharad: Propositional SAT solving (2018)
  10. Nadel, Alexander: Solving MaxSAT with bit-vector optimization (2018)
  11. Audemard, Gilles; Lagniez, Jean-Marie; Szczepanski, Nicolas; Tabary, Sébastien: A distributed version of Syrup (2017)
  12. Baud-Berthier, Guillaume; Giráldez-Cru, Jesús; Simon, Laurent: On the community structure of bounded model checking SAT problems (2017)
  13. Blinkhorn, Joshua; Beyersdorff, Olaf: Shortening QBF proofs with dependency schemes (2017)
  14. Bonacina, Ilario; Talebanfard, Navid: Strong ETH and resolution via games and the multiplicity of strategies (2017)
  15. Bonacina, Maria Paola; Plaisted, David A.: Semantically-guided goal-sensitive reasoning: inference system and completeness (2017)
  16. Cabodi, G.; Camurati, P. E.; Mishchenko, A.; Palena, M.; Pasini, P.: SAT solver management strategies in IC3: an experimental approach (2017)
  17. Carlsson, Mats; Johansson, Mikael; Larson, Jeffrey: Scheduling double round-robin tournaments with divisional play using constraint programming (2017)
  18. Chihani, Zakaria; Marre, Bruno; Bobot, François; Bardin, Sébastien: Sharpening constraint programming approaches for bit-vector theory (2017)
  19. de Nivelle, Hans: Theorem proving for classical logic with partial functions by reduction to Kleene logic (2017)
  20. Devriendt, Jo; Bogaerts, Bart; Bruynooghe, Maurice: Symmetric explanation learning: effective dynamic symmetry handling for SAT (2017)

1 2 3 ... 25 26 27 next


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