Login | Register

An implementation of the DPLL algorithm


An implementation of the DPLL algorithm

Ahmed, Tanbir (2009) An implementation of the DPLL algorithm. Masters thesis, Concordia University.

[thumbnail of MR63140.pdf]
Text (application/pdf)
MR63140.pdf - Accepted Version


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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Item Type:Thesis (Masters)
Authors:Ahmed, Tanbir
Pagination:xii, 126 leaves : ill. ; 29 cm.
Institution:Concordia University
Degree Name:M.A. Sc.
Program:Computer Science and Software Engineering
Thesis Supervisor(s):Chvátal, Vasek
Identification Number:LE 3 C66C67M 2009 A36
ID Code:976566
Deposited By: Concordia University Library
Deposited On:22 Jan 2013 16:28
Last Modified:13 Jul 2020 20:10
Related URLs:
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top