An implementation of the DPLL algorithm
The satisfiability problem (or SAT for short) is a central problem in several fields of computer science, including theoretical computer science, artificial intelligence, hardware design, and formal verification. Because of its inherent difficulty and widespread applications, this problem has been i...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
2009
|
| Online Access: | http://spectrum.library.concordia.ca/976566/1/MR63140.pdf Ahmed, Tanbir <http://spectrum.library.concordia.ca/view/creators/Ahmed=3ATanbir=3A=3A.html> (2009) An implementation of the DPLL algorithm. Masters thesis, Concordia University. |
| Summary: | The satisfiability problem (or SAT for short) is a central problem in several fields of computer science, including theoretical computer science, artificial intelligence, hardware design, and formal verification. Because of its inherent difficulty and widespread applications, this problem has been intensely being studied by mathematicians and computer scientists for the past few decades. For more than forty years, the Davis-Putnam-Logemann-Loveland (DPLL) backtrack-search algorithm has been immensely popular as a complete (it finds a solution if one exists; otherwise correctly says that no solution exists) and efficient procedure to solve the satisfiability problem. We have implemented an efficient variant of the DPLL algorithm. In this thesis, we discuss the details of our implementation of the DPLL algorithm as well as a mathematical application of our solver. We have proposed an improved variant of the DPLL algorithm and designed an efficient data structure for it. We have come up with an idea to make the unit-propagation faster than the known SAT solvers and to maintain the stack of changes efficiently. Our implementation performs well on most instances of the DIMACS benchmarks and it performs better than other SAT-solvers on a certain class of instances. We have implemented the solver in the C programming language and we discuss almost every detail of our implementation in the thesis. An interesting mathematical application of our solver is finding van der Waerden numbers, which are known to be very difficult to compute. Our solver performs the best on the class of instances corresponding to van der Waerden numbers. We have computed thirty of these numbers, which were previously unknown, using our solver. |
|---|