search

jeffgerickson / algorithms

Bug-tracking for Jeff's algorithms book, notes, etc.
7.92k stars 1.02k forks source link

3SAT algorithms in "Fast Exponential Algorithms" are incorrect #84

Open jeffgerickson opened 5 years ago

jeffgerickson commented 5 years ago

[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 commented 5 years ago

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 commented 5 years ago

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