Algorithm: SAT implementation

Made this for a uni assignment, really excited to see it working and it’s also my first decent prolog project :sweat_smile:

There’s also a swish notebook:

I implemented a parser for boolean expressions and a separate parser for CNF formulas (DIMACS format);
a naive algorithm to transform arbitrary expressions in a subset of the logical operators \langle \to; \wedge;\lor;\neg \rangle into CNF format, using simple logic concepts such as the distributive property and De Morgan’s laws;
and finally the DPLL algorithm.