As stated in the final project description, every time a player wishes to move a piece in the game you are to implement, the player must solve a simple problem: he is given a set of switches, and descriptions for how various traps can be disarmed, and he must find a configuration of the switches that gives him what he deems suitably low risk of passage.

This is an example of a satisfiability problem. The most generic way to describe a satisfiability problem is: given a boolean expression over some set of variables, does there exist a truth assignment that satisfies the expression? This is known to be an NP-complete problem. You'll learn all about that in 482, but all you need to know now is that it means that we don't know how to solve it in polynomial time, and many computer scientists believe it to be impossible.

The specific version of satisfiability you face is known as "3-SAT" -- that is, your expression will take the form of a conjunction of length-3 disjunctions over the variables. Here, the variables are switches, and each disjunction corresponds to a trap. The terms of the disjunction each symbolize one of the three conditions that will disable that trap.

It has been proven that 3-SAT is as hard as the more general satisfiability problem; that is, if 3-SAT can be solved in polynomial time, then so can more general satisfiability. This doesn't particularly help us. So, faced with a problem you know to be NP-complete, what can you do?

There are a few options, traditionally, for dealing with NP-complete problems: first, you can always simply attempt the brute-force exponential-time algorithm. You can look for an approximation algorithm that has sub-optimal performance but can be proven to find output within a certain range from the optimum. You can attempt a probabilistic approach that yields good average behavior, but still might take exponential time. Or you can attempt a heuristic -- an algorithm that does not provably perform in polynomial time, but does so for some or most inputs.

Brute Force

What would it mean to attempt a "brute force" solution to 3-SAT? The easiest imaginable solution to any problem with a finite solution space is as follows: enumerate the solutions, and test them one by one. In this case, the possible solutions are truth assignments over all of the variables/switches. Obviously, the number of possible truth assignments is 2^n, where n is the number of variables -- here, "switches" -- in the problem. Checking each assignment requires, assuming constant-time lookup within a truth assignment, O(m) where m is the number of disjunctions -- here, traps. A brute force approach, then, has a running time of O(m2^n).

Improvements

When looking to improve on an algorithm, a good strategy is to look for, and attempt to eliminate, any work that the algorithm does unnecessarily or performs repeatedly. Here, we can find several such instances of repeated or unnecessary work.

For instance: if the term -S1 never appears anywhere in the input, it seems strange to ever examine any solutions that have switch 1 turned to "off." Even if we only find one such term, we have just halved the solution space we need to search, without any fear of having thrown out the optimal solution.

Now, imagine that every conjunction that contains the term S2 also contains S3. In this scenario, we should not consider any solutions that include switches 2 and 3 both being set to "on." For any such solution, it is impossible that the quality of the solution degrades if we turn off one of the two.

Using these guidelines, we can be a bit more clever than we were before. Instead of simply generating every solution and testing it, we can generate a subset of the total solution space that we know to contain the answer, and test every solution in that subspace.

Davis-Putnam-Logemann-Loveland

This is a good start, but we can do better. We're still repeating work. For instance: say that we are looking at solutions with all switches 1, 2, and 3 turned off. Since we have 25 switches total, we can tell that there are 2^22, or roughly 4 million such solutions. If we are looking for a pure solution, and it turns out that one of my conjunctions is "S1 || S2 || S3", we should immediately throw out all of these 4 million solutions. More importantly, we shouldn't generate those solutions to begin with. That's the key behind the DPLL algorithm.

The idea is as follows: imagine a tree; each leaf is a solution, and each branching point is a boolean choice over one of the variables. So, if a node represents a boolean choice over variable 1, then descendants of that node's left child will all assign a value of true to variable 1, and descendants of the right will all assign a value of false. Of course, there are many such trees, because we can branch on the variables in different orders.

The idea of DPLL is to walk down such a tree -- think of a depth-first search -- in search of a valid solution. Only, instead of stopping whenever we hit solutions and testing them for validity, we try, whenever possible, to detect when entire subtrees are invalid, and turn back as soon as we detect that we are currently in one such subtree. The other key, obviously, is to never explicitly generate the tree.

If we strip it of almost all optimizations, the algorithm would read as follows:

As we can see, this would detect the scenario described in the beginning of this section -- if it had set the first three switches in a manner that immediately made satisfying the entire disjunction impossible, it would stop and and change one of the assignments without generating or analyzing 4 million invalid combinations. On the other hand, this version still lacks some simple optimizations that DPLL includes.

When DPLL is choosing the next variable to set, it can look for some "short cuts" -- some variables that we don't have to guess at values for, but instead can deduce values for if the guesses we have already made are accurate. This pertains to the improvements on brute-force search we saw before. There are two improvements in particular.

First, if there are any disjunctions such that are reduced to "unit clauses" under the current truth assignment -- that is, they only have one term that is not already rendered false by the current "guesses" -- then we know that we must satisfy that term, and so we should do so for our next assignment. Second of all, we said before that, if a variable only appears in positive or negative terms, it should be assigned a positive or negative value. Here, we can get even more use out of this: if a variable appears only in positive or negative terms within the clauses that have not yet been satisfied, then we should immediately assign the appropriate value to that variable.

There is one snafu: now that we have made our system of choosing variables and values to assign to them more complicated than simply "try true first, then false," our system of rolling back incorrect guesses seems like it needs to become more complicated. Thankfully, this is not the case. As it turns out, thanks to a handy feature of SML, we can rewrite the pseudocode above as: 

fun simplifiedDPLL(expr,truthassignment)=
  if satisfied(expr,truthassignment)
    then return true
  else if unsatisfiable(expr,truthassignment)
    then return false
  else let
         val l = choosenextliteral(expr,truthassignment)
       in
         simplifiedDPLL(expr,TRUE(l)::truthassignment) orelse
         simplifiedDPLL(expr,FALSE(l)::truthassignment)
       end

Here, the handy feature is SML's short-circuiting of the orelse operator. We never have to explicitly "roll back" old guesses because we can simply use "or" to evaluate both sides of any guess, and we know that if we ever get a solution that evaluates to true, SML will not evaluate the second half the "orelse" statement.

Now, we can make a simple change to the above code to replace "choosenextliteral" for a function that chooses the next literal and, optionally, suggests or dictates a value for that literal. We can implement this function to check for unit clauses or variables that only appear in positive or negative terms.

There's one snafu: as it's normally stated, 3-SAT is a decision problem, and isn't concerned with actually finding the specific truth assignment that satisfied the expression. You'll note that the code above just returns a boolean value, and the trick with "orelse" wouldn't be so easy if it had to return anything else. If you want to return a non-boolean value from this function, then, you will have to be a tiny bit cleverer.

The most obvious question, now, is: if there are no obvious choices, how do we choose the next literal to branch on? There have been many heuristics suggested and researched; we leave this to the implementer to experiment with. For a simple start, try always branching on the variable that can be assigned to immediately satisfy the most clauses. One thing to keep in mind is that a good branching criterion that cannot be computed quickly is not worthwhile; that is, you may find that your algorithm runs more quickly if you choose a branching scheme that makes decisions very quickly rather than always making clever branching decisions.

Probabilistic Approaches

Another approach taken to the SAT problem is a local search within the solution space, from a randomized starting space. This is more intuitive than it sounds, and it works like this: the algorithm picks a random truth assignment, and tests it. Assuming it hasn't stumbled by chance onto a satisfactory solution, it looks to find the one change -- switching one variable from true to false or false to true -- that yields the most improvement in terms of number of clauses satisfied. It makes this change, and continues. The hope is that this path will lead to an optimal, or at least acceptable, solution. Of course, it may not; this algorithm often runs into local maxima. When it does so, the algorithm simply restarts with a new random starting point.

To help avoid running into local maxima, some flavors of this algorithm periodically, or randomly with a fixed probability at every timestep, make one random change instead of one optimal change.

This algorithm has one natural advantage over DPLL for your purposes, and that is that it is better suited to looking for "adequate" solutions rather than perfect ones. It requires remarkably minor changes to this algorithm to run it for a set period of time -- say, 10 restarts -- and to return the best solution that it finds in that time. It is also very easy to implement.