Chaff swMATH ID: 6916 Software Authors: Moskewicz, Matthew; Madigan, Conor; Zhao, Ying; Zhang, Lintao; Malik, Sharad Description: 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. Homepage: http://www.princeton.edu/~chaff/software.html Keywords: SAT solver Related Software: MiniSat; BerkMin; SATO; z3; Walksat; Siege; Velev SAT Benchmarks; DIMACS; Lingeling; PicoSAT; SCIP; CPLEX; Plingeling; Glucose; SATIRE; Sat4j; zChaff; NuSMV; ManySAT; Isabelle/HOL Cited in: 581 Documents Further Publications: http://www.princeton.edu/~chaff/publication.html all top 5 Cited by 882 Authors 17 Stuckey, Peter James 14 Biere, Armin 13 Giunchiglia, Enrico 13 Nordström, Jakob 11 Marques-Silva, João P. 11 Strichman, Ofer 10 Junttila, Tommi A. 9 Cimatti, Alessandro 9 Clarke, Edmund Melson jun. 9 Sebastiani, Roberto 9 Simon, Laurent S. R. 8 Armando, Alessandro 8 Bryant, Randal E. 8 Gomes, Carla P. 8 Manyà, Felip 8 McMillan, Kenneth L. 8 Tacchella, Armando 8 Weidenbach, Christoph 7 Heule, Marijn J. H. 7 Lauria, Massimo 7 Li, Chumin 7 Lynce, Inês 7 Maratea, Marco 7 Penczek, Wojciech 7 Sabharwal, Ashish 7 Saïs, Lakhdar 7 Sakallah, Karem A. 7 Schaub, Torsten H. 6 Audemard, Gilles 6 Berthold, Timo 6 Drechsler, Rolf 6 Ganesh, Vijay 6 Gebser, Martin 6 Goldberg, Eugene L. 6 Heljanko, Keijo 6 Kröning, Daniel 6 Le Berre, Daniel 6 Nadel, Alexander 6 Niemelä, Ilkka N. F. 6 Nieuwenhuis, Robert 6 Oliveras, Albert 6 Prestwich, Steven D. 6 Sinz, Carsten 6 Van Gelder, Allen 6 Zhang, Lintao 5 Becker, Bernd 5 de Moura, Leonardo 5 Ganai, Malay K. 5 Giráldez-Cru, Jesús 5 Gupta, Aarti 5 Järvisalo, Matti 5 Johannsen, Jan 5 Malik, Sharad 5 Markov, Igor L. 5 Schütt, Andreas 5 Vinyals, Marc 4 Achterberg, Tobias 4 Amla, Nina 4 Ashar, Pranav 4 Beame, Paul W. 4 Bonacina, Maria Paola 4 Bozzano, Marco 4 Bruttomesso, Roberto 4 Chu, Geoffrey 4 Compagna, Luca 4 Dechter, Rina 4 Elffers, Jan 4 Feydy, Thibaut 4 Fleury, Mathias 4 Fränzle, Martin 4 Gent, Ian Philip 4 Gleixner, Ambros M. 4 Hebrard, Emmanuel 4 Herde, Christian 4 Jovanović, Dejan 4 Kaufmann, Benjamin 4 Kautz, Henry A. 4 Khomenko, Victor 4 Kukula, James H. 4 Lagniez, Jean-Marie 4 Lahiri, Shuvendu Kumar 4 Lammich, Peter 4 Leone, Nicola 4 Lierler, Yuliya 4 Marić, Filip 4 Meier, Andreas 4 Nightingale, Peter W. 4 Ricca, Francesco 4 Roveri, Marco 4 Schubert, Tobias 4 Selman, Bart 4 Sheini, Hossein M. 4 Somenzi, Fabio 4 Sorge, Volker 4 Tinelli, Cesare 4 Truszczyński, Mirosław 4 van Rossum, Peter 3 Aloul, Fadi A. 3 Amjad, Hasan 3 Ansótegui, Carlos ...and 782 more Authors all top 5 Cited in 73 Serials 37 Artificial Intelligence 31 Journal of Automated Reasoning 23 Annals of Mathematics and Artificial Intelligence 21 Constraints 17 Journal of Satisfiability, Boolean Modeling and Computation 14 The Journal of Artificial Intelligence Research (JAIR) 11 Formal Methods in System Design 8 Discrete Applied Mathematics 8 Annals of Operations Research 6 Fundamenta Informaticae 6 Logical Methods in Computer Science 5 Theoretical Computer Science 5 Theory and Practice of Logic Programming 4 SIAM Journal on Computing 4 Computers & Operations Research 4 AI Communications 4 INFORMS Journal on Computing 4 ACM Transactions on Computational Logic 4 Mathematical Programming Computation 3 Information and Computation 3 European Journal of Operational Research 3 Mathematical Programming. Series A. Series B 3 Journal of Applied Logic 2 Information Processing Letters 2 Journal of Algorithms 2 Science of Computer Programming 2 Journal of Symbolic Computation 2 Formal Aspects of Computing 2 Journal of Logic and Computation 2 Journal of Heuristics 2 International Journal of Applied Mathematics and Computer Science 2 Journal of Applied Mathematics 2 Discrete Optimization 2 Science in China. Series F 2 Encyclopedia of Mathematics and Its Applications 2 Lecture Notes in Computer Science 1 Acta Informatica 1 Discrete Mathematics 1 Journal of the Franklin Institute 1 Commentationes Mathematicae Universitatis Carolinae 1 IEEE Transactions on Automatic Control 1 Journal of Computer and System Sciences 1 Kybernetika 1 Annals of Pure and Applied Logic 1 Journal of Computer Science and Technology 1 Algorithmica 1 International Journal of Parallel Programming 1 International Journal of Approximate Reasoning 1 JETAI. Journal of Experimental & Theoretical Artificial Intelligence 1 Computational Geometry 1 Journal of Global Optimization 1 Discrete Event Dynamic Systems 1 Computational Complexity 1 Journal of Computer and Systems Sciences International 1 Journal of Applied Non-Classical Logics 1 Journal of the Egyptian Mathematical Society 1 International Transactions in Operational Research 1 Journal of Combinatorial Optimization 1 Journal of Scheduling 1 Bulletin of the European Association for Theoretical Computer Science EATCS 1 Optimization and Engineering 1 OR Spectrum 1 4OR 1 ACM Journal of Experimental Algorithmics 1 Journal of Discrete Algorithms 1 Studies in Computational Intelligence 1 Mathematics in Computer Science 1 Optimization Letters 1 Foundations and Trends in Electronic Design Automation 1 Theory of Computing 1 Statistics and Computing 1 Computer Science Review 1 Prikladnaya Diskretnaya Matematika all top 5 Cited in 20 Fields 529 Computer science (68-XX) 87 Mathematical logic and foundations (03-XX) 82 Operations research, mathematical programming (90-XX) 19 Combinatorics (05-XX) 18 Information and communication theory, circuits (94-XX) 7 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 6 General and overarching topics; collections (00-XX) 4 Order, lattices, ordered algebraic structures (06-XX) 4 Systems theory; control (93-XX) 2 Commutative algebra (13-XX) 2 Calculus of variations and optimal control; optimization (49-XX) 2 Statistics (62-XX) 2 Numerical analysis (65-XX) 2 Biology and other natural sciences (92-XX) 1 Number theory (11-XX) 1 Group theory and generalizations (20-XX) 1 Convex and discrete geometry (52-XX) 1 Probability theory and stochastic processes (60-XX) 1 Fluid mechanics (76-XX) 1 Statistical mechanics, structure of matter (82-XX) Citations by Year