Abstract

Satisfiability problem or SAT is the problem of deciding whether a Boolean function evaluates
to true for at least one of the assignments in its domain. The satisfiability problem
is the first problem to be proved NP-complete. Therefore, the problems in NP can be encoded
into SAT instances. Many hard real world problems can be solved when encoded
efficiently into SAT instances. These facts give SAT an important place in both theoretical
and practical computer science.
In this thesis we address the problem of integrating a special class of equivalency reasoning
techniques, the strongly connected components or SCC based reasoning, into the
class of conflict driven clause learning or CDCL SAT solvers. Because of the complications
that arise from integrating the equivalency reasoning in CDCL SAT solvers, to our knowledge,
there has been no CDCL solver which has applied SCC based equivalency reasoning
dynamically during the search. We propose a method to overcome these complications.
The method is integrated into a prominent satisfiability solver: MiniSat. The equivalency
enhanced MiniSat, Eq-MiniSat, is used to explore the advantages and disadvantages of the
equivalency reasoning in conflict clause learning satisfiability solvers. Different implementation
approaches for Eq-MiniSat are discussed. The experimental results on 16 families
of instances shows that equivalency reasoning does not have noticeable effects for the instances
in one family. The equivalency reasoning enables Eq-MiniSat to outperform MiniSat
on eight classes of instances. For the remaining seven families, MiniSat outperforms Eq-
MiniSat. The experimental results for random instances demonstrate that almost in all
cases the number of branchings for Eq-Minisat is smaller than Minisat.