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.