6.825: Techniques in Artificial Intelligence
Fall, 2001

Homework 1: (I Can't Get No) Satisfaction

Due: Friday, October 5th

Overview

A fundamental obstacle in logic-based AI is the difficulty of solving the satisfiability problem (usually referred to as SAT). SAT problems are statements in propositional logic, written in conjunctive normal form (CNF). CNF sentences consist of variables, literals, and clauses. A variable (A, for example) can be assigned true or false, a literal is a variable or its negation (A or NOT A). In a CNF sentence, a clause consists of a disjunction of literals (literals joined together by OR operations). A sentence is a conjunction of clauses (clauses joined by AND operations). We will represent AND with "^" and OR with "v", and we will use C/C++/Java syntax to represent NOT as "!".

Sentence Example: (A v C v !B) ^ (Z) ^ (!E v X v Y v W)

The SAT problem asks if any assignment of truth values to variables exists that makes a CNF logical sentence true. SAT problems are very difficult to solve. SAT is NP-complete, and therefore no known algorithms can solve it in less than an exponential amount time. If a sentence has n variables, it will take O(2n) operations to discover an assignment in the worst case - equivalent to checking every possible assignment. Many interesting AI problems are NP-complete or harder, which leads us to consider approximate methods of solution, or exact methods that have good average case running times.

Reading: Russell & Norvig, Chapters 4,6 (Search, Propositional Logic)

Davis, Putnam, Logemann and Loveland

This algorithm is popularly known as DPLL and is one of the most widely used methods of solving satisfiability problems exactly. By "exactly" we mean that DPLL is guaranteed to find a satisfying assignment if one exists or terminate and report that none exists otherwise. Therefore, it still runs in O(2n) operations in the worst case.

Reading: Cook and Mitchell, "Finding Hard Instances of the Satisfiability Problem: A Survey"

The crucial sections of this paper are 1-2.1, which explain notation and the DPLL algorithm. Also read Section 3 closely, it discusses the mathematical properties that distinguish hard SAT problems from easy ones.

GSAT & WALKSAT

GSAT and WALKSAT are stochastic algorithms. In order to speed the search for a true assignment, they pick random locations in the space of possible assignments and make limited, local searches from those locations. As a result, they might be able to find a solution to a problem that would take too long to solve using DPLL's complete, global search. But because they do not cover the entire search space, there is no guarantee that GSAT or WALKSAT will find a solution to every problem, even if one exists. Therefore, these algorithms can never determine if a sentence is unsatisfiable. Algorithms are frequently categorized as sound or complete. A sound algorithm guarantees that any answer it returns is correct, but does not necessarily return an answer to every problem. A complete algorithm, on the other hand, will always return an answer. DPLL is complete and sound, while GSAT and WALKSAT are sound, but not complete.

Reading: Selman and Kautz, "Domain-Independent Extensions to GSAT: Solving Large Structured Satisfiability Problems"

Reading: Selman, Kautz, and Cohen, "Local Search Strategies for Satisfiability Testing"

The WALKSAT algorithm evolved from the GSAT algorithm. The first paper has an early exploration of some extensions to GSAT, including "GSAT with Random Walk." The second paper has the actual WALKSAT algorithm, and a brief explanation of its development.

The Picture Puzzle

Logic is a natural way to represent many games and puzzles. But it is certainly not always the best way. It can be difficult to represent information efficiently using propositional logic, as Russell and Norvig demonstrate in the Wumpus World example..

The "Picture Puzzle" comes from the pages of Games magazine (February, 1993). It is a variation on the idea of run-length encoding, a common method for compressing images. A binary image is a picture composed only of black and white pixels. In a picture puzzle, we are given run-length statistics for each row and column of a binary image. The goal is to use the row and column information to reconstruct the original image.

Each row or column is described by a list of numbers, one for each group of contiguous black blocks. The numbers give the size of the groups they describe. Groups must be separated from one another by at least one white pixel. For example, consider the following row:

This row would be described by the list "2 3 1", the block sizes from right to left. Columns are described from top to bottom.

The description of this column is "1 2". A column or row without any black pixels is described by an empty list.

Here is a sample picture and all the row and column descriptions it produces.

It is important to note that multiple pictures may have the same puzzle representations. There is no guarantee that solving a puzzle will produce the original picture that was used to create the row and column data. This exercise's purpose is to demonstrate the use of systematic and randomized search methods to solve a SAT-like problem.

Solving the Picture Puzzle

How can we formulate these puzzles as search problems? One strategy would be to think of each pixel as a propositional variable. There is a sentence in propositional logic corresponding to each puzzle, such that a satisfying assignment to the variables in the sentence is a solution to the puzzle.

Consider an arbitrary row i. Given the number list for the row, there are Ki possible arrangements of pixels in the row. We call these these the line possibilities of the row, and label them rip1 through ripki. For example, given a row of length 5 and numbers (2,1) we have the following possibilities:

[X][X][ ][X][ ]    [X][X][ ][ ][X]    [ ][X][X][ ][X]

The same is true for column possibilities denoted ripj.

For a puzzle with n rows and n columns, the sentence has the following structure:
(r1p1 v r1p2 v ... v r1pk1) ^ ... ^ (rnp1 v rnp2 v ... v rnpkn) ^
(c1p1 v c1p2 v ... v c1pl1) ^ ... ^ (cmp1 v cmp2 v ... v cmplm)

We still don't have a propositional logic sentence. We have to translate each of the rp's and cp'sinto propositional logic. Let's think again of a row i of length 5 with specification (2, 1). If we call each pixel in the row Ppi then the formula for ripi = p1i ^ p2i ^ !p3i ^ p4i ^ !p5i
which is a logical translation of the first row of the pixels above.

Thus the whole sentence that we need to satisfy has the structure
((A ^ ... ^ B) v ... v (C ^ ... ^ D)) ^ ... ^ ((E ^ ... ^ F) v ... v (G^...^H)))
where (E ^ ... ^ F) is one line possibility and
((E ^ ... ^ F) v ... v (G^...^H))) is all the possibilities for a particular row or column.

Finally, one strategy would be to convert this entire sentence to CNF and then run our standard satisfiability algorithms directly on it. But the process of converting to CNF will cause the formula to grow expontentially.

So, instead, we encourage you to think of this problem at the level of choosing among the line possibilities for each row and column, rather than choosing assignments for the individual pixels. Your assignment is to apply insights from DPLL and WalkSAT to this somewhat different problem.

Resources

Tasks

There is an and/or structure at the level of the line-possibilities, sort of like a standard SAT problem. Make sure you read and understand the above section on 'Solving the Picture Puzzle.' We want to try three algorithms on the MegaSAT problem:
  1. Brute Force: Implement a brute force algorithm. It should try every combination of possibilities for each row, and test for consistency with the column constraints until it finds and solution.
  2. DPLL: Implement an algorithm analagous to DPLL, including these parts:
    • Prune possibilities after making each assignment (simplification).
    • Fill in any forced choices for line assignment.
    • Variable selection can be arbitrary.
  3. WalkSAT: Implement an algoritm analagous to WalkSAT, including these parts:
    • A reasonable cost function.
    • A reasonable movement operator/neighborhood relation
    • A way to choose from the possible neighbors.
For each of these three algorithms, turn in the following.
  1. A description of your algorithm (not code!) with enough details that others can replicate your code. Make sure you spend extra time describing the algorithms around the bulleted points above. Talk about why you made any choices you made.
  2. Produce a graph charting solution times vs. puzzle area for each of those algorithms Graph each up to the size at which the puzzles become impractical. Use square puzzles of consecutively larger sizes - (plot 2x2, 3x3, 4x4, etc.) and randomize 40% of the pixels to be black. Average the results from at least 5 trials at each size.
  3. Discuss your results, explaining carefully why you think they came out as they did.
  4. Extras: For extra credit: try making DPLL as fast as possible. try making DPLL and/or WalkSAT solve more problems by varying your algorithms. show experimentally how your changes have helped you solve larger problems.
Bonus Challenge: Picture Puzzles published in Games magazine are designed so a clever human can solve them without backtracking. These puzzles are very large and solving them requires a good set of heuristics. I will put up some mystery puzzles on the web. In order to win the prize (ice cream at Toscanini's - or some equivalent for those who dislike ice cream), you must be able to solve at least one of the puzzles. If more than one person solves the puzzles, the winner will be the person who solved the most puzzles. If there is a tie at that level, there will be a speed run-off to determine the winner. Feel free to add additional heuristics to your algorithms, so long as you maintain their soundness. The duck puzzle, which is 10x10, should be fairly easy and is a good test to make sure your code is working properly. Addendum: "Speed" will be measured in a machine-independent way. When we collect results for the contest, we will ask you to report the number of assignments to the variables your algorithm had to check before solving the problem.

Handing In The Assignment