## 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.