编写算法解决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.