Satisfiability

Overview: Backtracking & the Power of Laziness

The lc program uses a particular strategy (called “outermost” reduction) for choosing where to $\beta$-reduce at each step, when it has a choice. Outermost reduction is guaranteed to (1) terminate when possible, and (2) not perform any work whose result is never needed. On the other hand, it may also duplicate work (exponentially often), making it wildly inefficient in practice.

When we introduced Haskell, we mentioned that Haskell’s evaluation strategy similarly has the power to avoid unnecessary work, but it also avoids duplicating needed work. This approach is commonly called lazy evaluation.

Some problems are much easier to solve with lazy evaluation. In this part of the assignment, we will look at how we can implement backtracking search with a lazy approach. We will use lazy backtracking to implement a program that solves the satisfiability problem (SAT) for propositional logic. Such a program is called a SAT solver.

Background: Satisfiability

Here is an example SAT problem: Can we find values for $p$, $q$, $r$, and $s$ (i.e., setting each to true or false) that make the following formula true

$( \lnot p \lor \lnot r \lor \lnot s ) \land ( q \lor r \lor \lnot s ) \land ( p \lor \lnot q \lor s ) \land ( p \lor r \lor s ) \land ( \lnot p \lor q \lor \lnot r )$

Similarly, can we find values for the variables that make the formula false?

More formally, a propositional formula is said to be satisfiable if there exists a way of setting variables to true or false that makes the whole formula true. It is said to be falsifiable if there are values for its variables that makes the formula false. Finally, it is said to be a tautology if all possible choices of values for the variables makes the formula true (i.e., if it is not falsifiable).

One way to determine whether a formula is satisfiable or falsifiable is to look at all possible assignments. This can be wasteful. For example, if the formula is $p \land \lnot p \land (q \lor r \lor s \lor t)$ we can stop trying to satisfy the formula almost immediately, rather than trying all 32 possibilities. Therefore, we can try to find a satisfying or falsifying assignment via search, short-circuiting whenever we realize that our goal is impossible (e.g., after seeing $p \land \lnot p$).

Examine a broken SAT solver [8%]

The file satsolver/SatAST.hs defines an AST for propositional formulas.

The file satsolver/BrokenSolveSAT.hs contains an initially plausible implementation for determining a satisfying assignment (i.e., a map or lookup table that associates variable names to booleans).

Load the file satsolver/UnderstandSAT.hs into ghci, and check that you get the same results for the broken SAT solver as we do:

    *UnderstandSAT> example1
    And (Var "a") (Or (Not (Var "a")) (Var "b"))
    *UnderstandSAT> Broken.satisfy example1
    Just [("b",True),("a",True)]
    *UnderstandSAT> Broken.falsify example1
    Just [("a",False)]

    *UnderstandSAT> example2
    Or (Var "v") (Not (Var "v"))
    *UnderstandSAT> Broken.satisfy example2
    Just [("v",True)]
    *UnderstandSAT> Broken.falsify example2
    Nothing

This looks good, it seems to work! But there is a third example to try.

    *UnderstandSAT> example3
    And (Or (Var "p") (Var "q")) (Not (Var "p"))
    *UnderstandSAT> Broken.satisfy example3
    Nothing

This result is wrong! A correct answer would have been

    Just [("p",False),("q",True)]

Review the code in satsolver/BrokenSolveSAT.hs and figure out the problem. There are no points associated with this task, but learning to read Haskell code is an important skill for this course, and time invested in understanding how Haskell works is time well spent. Additionally, you’ll need to understand what’s broken in order to do the next parts. To understand what’s broken, you could manually trace example3 through the code for satisfy in BrokenSolveSAT.hs.

(In essence the problem is that once the code decides that it seems sensible to set p to True, it can never revisit this choice and try a different option instead, which is in turn due to the implementation of Or. When running satisfyResult, if the left arm of the Or can be made true, it assumes it will never need to try the right arm of the Or and discards it.)

Your task: Define two example propositions:

Define example3alt to be a proposition that is logically equivalent to example3 (because it’s just a reordering) but for which Broken.satisfy produces the correct answer.
Show a similar problem exists with Broken.falsify by coming up with a similarly simple expression for example4 that should be falsifiable but instead also erroneously generates Nothing.

Make sure you understand what went wrong before you continue to the next part!

Fixing the problem [21%]

There are several ways to fix this problem, including a very powerful technique called continuation functions. But there is a conceptually simpler approach to solving the problem: take advantage of lazy lists.

If the issue is that operations like Or prematurely discard their righthand operands because it seems like the lefthand side is satisfiable, an alternative approach is to return both solutions (and in general, always return all possible solutions). Then if one of those solutions doesn’t pan out, we can always try one of the other ones.

Laziness is key to making this strategy efficient. The list of all possible solutions might be long. For example, a standard search of all solutions to

    And (Or (Or (Var "p") (Var "q")) (Or (Var "r") (Var "s")))
        (Or (Or (Var "t") (Var "u")) (Or (Var "v") (Var "w")))

will report 16 solutions (four ways to satisfy the first argument of And, and four independent ways to satisfy the second argument).

If we just want to know whether a proposition is or is not satisfiable, computing the list of 16 possibilities is overkill. Laziness can rescue us because the elements of a Haskell list will not be computed until they are used. If we ask for the head of the list, we will get the first solution (which says to set p to True) without computing any of the other alternatives!

An implementation of the SAT solver using laziness is provided in LazySolveSAT.hs. Review this code carefully. Confirm that this time you get the correct answer for Lazy.falsify example4.

Your task: To confirm your understanding of how the code works, hand-trace the execution of the code for evaluating some of the example expressions. For details, see the comments in UnderstandSAT.hs for how to modify the file to show the results of your tracing.

As you modify the file, be sure to load UnderstandSAT.hs into ghci, to make sure that your changes are valid Haskell. If your file has parse or type errors, we may not be able to test it properly and you’ll lose points.

Go on to the next part…

Make sure you have updated UnderstandSAT.hs in all the places where it says FIXME and that UnderstandSAT.hs loads in ghci. Then, head over to the next part, where we will work with a little language to match patterns in text.