A Pearl on SAT Solving in Prolog

A succinct SAT solver is presented that exploits the control provided by delay declarations to implement watched literals and unit propagation. Despite its brevity the solver is surprisingly powerful and its elegant use of Prolog constructs is presented as a programming pearl.

• Type: Conference
• Year: 2010
• Where: FLOPS
• Authors: Jacob M. Howe, Andy King
• Keywords: Delay Declarations, FLOPS 2010, Hardware, Succinct Sat Solver, Unit Propagation