TY - GEN
T1 - The quest for efficient Boolean satisfiability solvers
AU - Zhang, Lintao
AU - Malik, Sharad
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 2002.
PY - 2002
Y1 - 2002
N2 - The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.
AB - The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.
UR - http://www.scopus.com/inward/record.url?scp=84937545785&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84937545785&partnerID=8YFLogxK
U2 - 10.1007/3-540-45657-0_2
DO - 10.1007/3-540-45657-0_2
M3 - Conference contribution
AN - SCOPUS:84937545785
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 17
EP - 36
BT - Computer Aided Verification - 14th International Conference, CAV 2002, Proceedings
A2 - Brinksma, Ed
A2 - Larsen, Kim Guldstrand
PB - Springer Verlag
T2 - 14th International Conference on Computer Aided Verification, CAV 2002
Y2 - 27 July 2002 through 31 July 2002
ER -