Propositional Logics are the most fundamental class of logics. Despite their simplicity, they enjoy real industrial interest. Consequently, a good number of SAT solvers has been developed over the last decades, some of which are industrial-strength systems that can cope with problems arising in industrial applications. The huge variety of systems however is implemented on the basis of a smaller number of well-understood algorithm families.

The goals of this project are: (i) understand various implementation techniques for SAT solving algorithms, (ii) to implement specific algorithms that solve the SAT problem for propositional logic , (iii)  to investigate optimization techniques for the implementations and (iv) to evaluate the prototype performances amongst each other and with state-of-the-art implementations.

The implementation will be done in Java.