Finding Minimum Satisfying Assignments of Boolean Formulas

In this thesis we examine algorithms and techniques used for solving Boolean satisfiability (SAT). Then we inspect the possibility to use them in solving the weighted short SAT problem, which is a generalization of the satisfiability problem. Given that each variable has a weight, this generalization is the problem of finding a satisfying truth assignment while using the smallest sum of weights. To solve this problem, we introduce three truth assignments of variables - True, False and Unassign. We show that not all algorithms and techniques used in modern SAT solvers can be used in our program. Those that can be converted, will be implemented using our three truth assignments. This will yield several versions of our new solver, which will be compared. Powered by TCPDF (www.tcpdf.org