Course:3-SAT-isfy-me

GQL2SQL

What is the problem?

The problem is, well, every NP-Complete problem ever. Fortunately, by the Cook-Levin theorem, all NP-Complete problems can be reduced to every other NP-Complete problem in polynomial time, so we just have to solve one of them. Let's do SAT. $1,000,000 (and god-like power) is awaiting our poly-time algorithm. Hot take of the year: P = NP.

In all seriousness, NP-Complete problems are a particular set of problems where an answer to the problem can be verified in polynomial-time, but no polynomial-time solver currently exists*.

The SAT problem is as follows:

- Given a boolean formula of this form: $(\neg x_{1}\lor x_{2}\lor x_{4})\land (\neg x_{3}\lor \neg x_{2}\lor x_{5})\land \dots \land (x_{1}\lor \neg x_{2}\lor x_{5})$, decide if there is a true interpretation.

- The SAT problem uses is the logical AND of an arbitrary number of clauses where a clause is the logical OR of three boolean variables

In this project, we give a solver for SAT that takes in an arbitrary SAT formula and outputs a satisfying assignment, or false if no such assignment exists.

What is the something extra?

Once we have tested the waters by using Prolog to solve SAT, we will use Prolog to solve two other famous NP-Complete problems, namely:

1. K-COLOUR - Given a description of a graph, can it be coloured using exactly K colours without any nodes connected by an edge having the same colour?
2. SUBSET SUM - Given a set and number, does there exist a subset such that the numbers in that subset add to the given number?

This will test Prolog's ability to not only solve NP-Complete problems in the domain of boolean variables, but also in the domain of graphs and numeric values.

Also, since we were on the topic on NP-Completeness, we decided to also demonstrate that any arbitrary instance of SAT can be reduced to 3-SAT (that is, SAT in 3 conjunction normal form). This fact happens to be incredibly useful when proving theorems about SAT, since its 3-SAT form is predictable and great for mathematical reductions!

What did we learn from doing this?

One of the interesting things about doing this project was noticing that writing a Prolog program to check if a solution to an NP-Complete problem is valid ended up solving the problem "for-free". This is due to Prolog's powerful pattern matching ability and declarative style. However, as to be expected when solving NP-Complete problems, the program is incredibly solve on even medium sized inputs. To solve issues with performance, we employed several strategies:

1. Memoization - In Graph Colour, we were able to improve the performance on larger inputs by passing in a map of already assigned nodes so that upon encountering these nodes the program can skip to the next one. Of course, this does not lead to a significant decrease in time complexity (otherwise we would be Millionaires), but the time savings is noticeable.
2. Not Re-Inventing the Wheel - It turns out we are not the only ones who have tried to solve NP-Complete problems with Prolog, and we leveraged this fact in our SAT solver. Specifically, rather than reinventing the SAT-Solver wheel, we researched a Prolog-friendly SAT solver algorithm outlined by Howe and King (2012)* and implemented their SAT-solver algorithm instead. We learned a lot from this paper, and ended up with a beautifully elegant solution as a result (as well as one that is more performant than the naive approach!).

Links to code etc

Section:
Instructor:
Email:
Office:
Office Hours:
Class Schedule:
Classroom:
Important Course Pages
	Syllabus
	Lecture Notes
	Assignments
	Course Discussion
[[Category:]]

Link to Github Code: https://github.com/aaronVerones/3-sat-isfy-me

* this is not a formal definition of NP-Completeness.

* Howe, J. M., & King, A. (2012). A pearl on SAT and SMT solving in Prolog. Theoretical Computer Science, 435, 43–55. doi: 10.1016/j.tcs.2012.02.024

Section:
Instructor:
Email:
Office:
Office Hours:
Class Schedule:
Classroom:
Important Course Pages
	Syllabus
	Lecture Notes
	Assignments
	Course Discussion
[[Category:]]