ICS Theory Group

ICS 269, Spring 2003: Theory Seminar

2 May 2003:
Exact algorithms for Exact Satisfiability
Jesper Makholm Byskov

The Exact Satisfiability problem (XSAT) is the variant of the Satisfiability problem (SAT) in which we are given a formula in conjunctive normal form and are asked to find a truth assignment to the variables s.t. EXACTLY one literal in each clause is true. The Exact 3-Satisfiability problem (X3SAT) is the restriction of XSAT to formulas with at most three literals per clause.

We are interested in algorithms for these two problems with good worst-case complexity, i.e. better than the trivial O(2^n) which comes from trying all possible truth assignments. For XSAT we improve the running time from O(2^(0.2441*n)) to O(2^(0.2325*n)) and for X3SAT we improve the running time from O(2^(0.1626*n)) to O(2^(1379*n)).

Our algorithms work by analysing the formula and branching depending on a number of different cases. As the number of cases is rather large, I will give an overview of the ideas and only cover some of the cases in detail.

This is joint work with Bolette Ammitzb°ll Madsen and Bjarke Skjernaa. It has not been published yet, but if you are interested, lease send me an email at jespermn@ics.uci.edu.