This sat solver implements well-known sat-solving techniques including unit propagation and branching on partial truth assignments in order to determine whether an input, given in CNF, is satisfiable.
Optimisation has been a key aspect of development; the sat solver presented in this project runs several orders of magnitude times faster than the basic initial implementation initially written up, which uses brute force.
Each question number is labelled with an increasing level of complexity. To run the full program, download and run q8.py.