# Course:3-SAT-isfy-me

## GQL2SQL

#### Authors: Greg, Aaron

### 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: , 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:

- 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?
- 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:

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