Measures and Algorithms for the Exact Satisfiability Problem and its variants
Abstract :
The Exact Satisfiability problem, XSAT, is an important variant of SAT. It asks if it is possible to find a satisfying assignment such that each clause has exactly one literal that evaluates to 1, while the rest of the literals are set to 0. If we restrict the length of the clause to k literals, then the problem is also known as XkSAT. XSAT and X3SAT are commonly studied problems and deciding them is NP-complete. In this thesis, we study XSAT and its variants and we propose faster exact algorithms to solve them.
The first problem that we study is XSAT itself. XSAT has seen numerous improvements to the development of its exact algorithm over the years. These algorithms were all designed with the standard measure in mind. By introducing a nonstandard measure, we propose an algorithm to solve XSAT running in O(1.1674^n) time, using polynomial space.
The second problem is the General k Exact Satisfiability problem, where for k >=2, a formula contains clauses that require i literals to be assigned 1, while the rest of the literals are assigned 0, for i <= k. Therefore, it asks if it possible to find an assignment such that the constraint in each clause is satisfied. These class of problems are also known to be NP-complete. We study the problems for k=2, k=3, k=4. By introducing a nonstandard measure, we propose an algorithm solving such decision problems in O(1.3674^n) time for k=2, O(1.5687^n) for k=3, and O(1.6545^n) for k=4 using polynomial space. If we are allowed to use exponential space, then we give faster algorithms to solve these problems in O(1.3188^n) time, O(1.3407^n) time and O(1.3536^n) time respectively.
The third problem is the #X3SAT problem. In this problem, we are interested to know the number of exact-satisfiable assignments to the given formula. #X3SAT is known to be #P-complete. We give an algorithm to solve the problem in O(1.1120^n) time. We use a result by Monien and Preis and a different way to analyse a special case of the algorithm to help us to tighten the analysis of the algorithm further.
The last problem is the Max Hamming Distance XSAT and X3SAT, where we are interested to know for any given pair of exact satisfiable assignments to the formula, what is the maximum number of variables that differ based on the values assigned. We propose an algorithm that uses a nonstandard measure to solve Max Hamming Distance XSAT in O(1.4983^n) time. Finally, for the Max Hamming Distance X3SAT problem, we give an algorithm in O(1.3298^n) time by relying on the Monien and Preis result again.