编写算法解决NP问题中的Boolean Satisfiability问题。
Preamble
Boolean satisfiability (SAT) is the problem of deciding, via a yes or no
answer, if there is an assignment to the variables of a Boolean formula such
that the formula is satisfied (e.g., makes the formula “True”). Consider the
formula (a b) (a c). The assignment “b = True” and “c = False” satisfies the
formula.
Stephen Cook proved that SAT was NP-complete (nondeterministic polynomial
time) in 1971, thus becoming the first-known NP-complete problem. As an NP-
complete problem, SAT is a decision (yes/no) problem that when given a
solution, the solution can be verified in polynomial time. But, the problem of
finding a solution quickly (in polynomial time) is considered at least as hard
to solve as the hardest decision problem. NP-complete problems are of interest
to researchers because if any NP-complete problem can be solved quickly, then
every decision problem can be solved quickly.
Richard Karp’s subsequent paper, “Reducibility among combinatorial problems,”
generated renewed interest in Cook’s paper by providing a list of 21 NP-
complete problems. Cook and Karp received a Turing Award for this work. It is
interesting to note that Stephen Cook was denied tenure in 1970 by the
University of California, Berkeley. He then joined the faculty of University
of Toronto, Computer Science and Mathematics Departments as an associate
professor, where he was promoted to professor in 1975 and Distinguished
Professor in 1985. In a speech celebrating the 30th anniversary of the
Berkeley EECS department, fellow Turing Award winner and Berkeley professor
Richard Karp said that, “It is to our everlasting shame that we were unable to
persuade the math department to give him tenure.”
Despite the inherent inefficiency of algorithms to solve Boolean
satisfiability problems, Martin Davis, Hilary Putnam, George Logemann, and
Donald W. Loveland developed a solution using a backtrackingbased search
algorithm in 1962 (the DPLL algorithm), which is still the basis for the most
efficient complete SAT solvers today. SAT is useful for many practical
applications, such as model-checking (e.g., does a model match its
specifications), automated reasoning (e.g., theorem proving), and determining
whether a solution exists to a combinatorial search problem.
It is also used in AI planning, which is described as follows. Given a
description of possible initial states of the world, a description of the
desired goals, and a description of a set of possible actions, the planning
problem is to find a plan that is guaranteed to generate a sequence of actions
from any of the initial states that leads to one of the goal states. Outside
of AI, SAT is also useful for determining whether two logic circuits are
equivalent, allowing circuits to be simplified.
As a practical example, consider the following constraints:
- Kelly must schedule a meeting with John, Catherine, Ann, and Peter.
- No one is willing to meet on a weekend.
- John can only meet either on Monday, Wednesday, or Thursday.
- Catherine cannot meet on Wednesday.
- Anne cannot meet on Friday.
- Peter cannot meet on Tuesday or on Thursday.
- Question: When can the meeting take place?
This can be encoded into the following Boolean formula:
¬Sat ∧ ¬Sun ∧ (Mon ∨ Wed ∨ Thu) ∧ (¬Wed) ∧ (¬Fri) ∧ (¬Tue ∧ ¬Thu)
Thus, the meeting can only take place on Monday.
Assignment
Convert to CNF
Since SAT solvers typically only accept formulas in Conjunctive Normal Form
(CNF), your first task is to develop an algorithm that, given an input
formula, converts it to CNF, and outputs the formula in clause form. For
example, given the input formula A v (B ^ C), the equation would be converted
to CNF, giving (A v B) ^ (A v C) and output that in clause form {(A,B),(A,C)}.
Proof by Refutation
Given a set of premises and a conclusion, your next task is to determine
whether the conclusion logically follows from the premises. You will need to
convert premises and the conclusion to CNF, then implement the DPLL algorithm
to solve the problem. Premises will be on separate lines, and the line
containing the conclusion will begin “Therefore, “ and end with a period “.”
For instance, a sample input could be:
A v (B ^ C)
C
Therefore, B.
The output from your program would either be, “The conclusion follows
logically from the premises,” or “The conclusion does not follow logically
from the premises.”
Three-coloring problem
Given a set of edges in a graph, your third task is to solve the threecoloring
problem. This problem is as follows. Given a map, is it possible to color the
countries using three colors such that no two countries that are next to each
other have the same color? The countries are represented as nodes on a graph,
and the task is to assign values from a set of three possible colors (red,
green, or blue), such that no two nodes that are joined by an edge have been
assigned the same value. For this problem, the input is of the following form:
{(A,B),(A,C),(A,D),(B,C),(C,D)}, where each clause represents an edge. For
instance, there is an edge from A to B in this graph. The graph presented
looks like the following: This is an exmaple of a graph that can be three-
colored.
The output of your program will either be a solution to the problem (which is
unlikely to be a unique solution) or, “The graph cannot be three-colored.”
Since the example graph is satisfiable, a possible solution, and thus possible
output from your program, is “{AR, BG, CB, DG}”, where AR represents the fact
that A has been colored Red, BG represents that B has been colored Green, and
so on. Note that this isn’t the only solution. You only need to find one
solution. An implementation of DPLL will be needed for this program. This is
an example of a graph that cannot be three-colored. This graph is an example
of one that cannot be three-colored. The input to your program for this graph
would be {(A,B),(A,C),(A,D),(B,C),(B,D),(C,D)}. Your program would output,
“The graph cannot be three-colored.” Either spelling of colored / coloured is
acceptable.
Turn in the three programs
Turn in the three programs along with a technical document (which can be
combined in one document) and READMEs describing how to run the programs. You
will be graded on the quality of the technical document, but not on the
quality of the README (unless I can’t get your program to run using your
instructions). You can work in groups. I expect one submission per group. In
your submission, be sure to include the names and net IDs of all the group
members.
The technical document(s)
The technical document(s) should provide details about the algorithms you
implemented, along with each function and their purpose. The key things to
this document are that you explain your algorithm well and present it in the
best manner possible. The document is required because I allow any high-level
language.
Note
However, that PROLOG, Haskell, LISP, and similar languages are not allowed for
this assignment, as they would practically solve the problem for you. Use
high-level languages such as C, C++, C#, Java, JavaScript, PHP, Visual Basic,
MATLAB, etc. No matter which language you use, you (or your group) must
implement your own algorithms. You may certainly use example pseudocode, such
as the DPLL algorithm shown in this document, but you may not use someone
else’s full DPLL code/program.
Grading
There are four parts to the grading.
Part 1: Convert to CNF.
- a. Your CNF program will be run with several input formulas. You will be graded on the number of correct solutions.
- b. Part 1 is thus worth a maximum of 26 points.
Part 2: Proof by Refutation
- a. Your proof by refutation program will be run with several input statements (e.g., a set of premises with a conclusion). You will be graded on the number of correct solutions.
- b. Part 2 is thus worth a maximum of 26 points.
Part 3: Three-coloring Problem
- a. Your three-coloring program will be run with several input graphs (e.g., a set of edges). You will be graded on the number of correct solutions.
- b. Part 3 is thus worth a maximum of 26 points.
Part 4: Technical Document
- a. The fourth part is a grade on your technical document and algorithms. This is worth 22 points. I’ve weighted this less heavily this time since there is no competition component. The grade will include grammar, spelling, presentation quality, and the description of your algorithms. I should be able to know how your algorithms work.
The total points you can earn for this assignment is 100. This assignment is
17% of your total grade.
