3SAT algorithms in "Fast Exponential Algorithms" are incorrect

[jeffgerickson]

[reported by Moses Ganaradi via email]

The 3SAT-algorithms on pages 3 and 5 never return false and hence cannot be correct!
The problem becomes clear when considering the formula x AND \not x:
We have to compute phi given x and not x, and somehow this should be false.

[jeffgerickson]

The problem is in the base cases. The algorithms correctly handle formulas with zero clauses, but not clauses with zero literals!

If the input formula Φ contains the pure literal (or one-literal clause) not-x, then the formula Φ|x contains a ZERO-variable clause, which is impossible to satisfy! So both 3SAT and Faster3Sat should have two additional lines:

if Φ has any empty clauses
    return False

More generally, the 3Sat algorithm assumes every clause has exactly three literals, and Faster3Sat assumes every clause has either three literals or one. But neither of these assumptions holds for the recursive calls! Fixing both algorithms to handle one and two-literal clauses is straightforward; as usual, the vacuous base case is more subtle.

[jeffgerickson]

Boy, this is a bag of worms. Fixed (locally) and added discussion of low-hanging improvements to the conservative time analysis.