CSC 341 (Fall 2021)

Reading: Solving SAT Efficiently

Recall that when dealing with intractable problems, we must compromise on one of three pillars:

  1. Producing a correct/optimal solution.
  2. Finding a solution in polynomial time.
  3. Operating over arbitrary, unconstrained inputs.

We have seen in our study of approximation that we can compromise on one, or both, of points (1) and (3) to arrive at an approximation algorithm for our problem where we gain tractability at the cost of accepting a bound on the generated solution.

It seems rather pointless to compromise on (2) since intractability is precisely defined to be not having a polynomial time algorithm. However, if a problem admits an algorithm that has worst-case exponential complexity but those cases are rare or only occur in cases that “don’t matter,” then we would be likely to use such an algorithm “in practice.”

In today’s class, we’ll look at solving the boolean satisfiability problem, \(\mathsf{SAT}\), directly, but with appropriate heuristics so that our brute-force algorithm performs relatively well in practice. In preparation for our discussion, check out the 2021 SAT Competition where researchers compete in building the most efficient SAT solvers possible. You might find it useful to check out the summary descriptions of the various solver, found on the download page of the competition:

If you are interested in learning more about SAT solving and its applications to software verification, check out these longer readings: