This repository contains example implementations of the unit propagation part of the Davis–Putnam–Logemann–Loveland (DPLL) algorithm for determining the satisfiability of formulae in conjunctive normal form (CNF). They involve searching for unit clauses and propagating their truth values through a given formula, and outputting either a sorted set of obtained unit clauses, or else signalling a contradiction.
- The "basic" implementation runs in polynomial time, while the "linear" implementation runs in linear time in the average case.
- C implementations of Abstract Data Types are used for Literals, Clauses and Formulas.
- A psuedo-unit testing framework in C is defined for verification purposes.