# 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: ${\displaystyle (\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!).

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

* 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:]]