Algorithm: SAT implementation

Announce
1

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.

1 Like
2

The sat solver of Howe & King may be of interest. It is a 20 line Prolog program, implementing DPLL with watched literals and unit propagation.
See
Howe, J. M. and King, A. 2012. “A pearl on SAT and SMT solving in Prolog”. Theoretical Computer Science 435, 43–55.
Paper
Drabent, W. 2018. “Logic + control: On program construction and verification”. Theory and Practice of Logic Programming 18 (1): 1–29 (also [1110.4978] Logic + control: On program construction and verification)
presents a systematic derivation of this program.

Here is the program, for explanations see one of these papers.

%A sat solver, utilising delay declaration to implement
%watched literals
%
%Authors: Jacob Howe and Andy King
%Last modified: 3/11/09
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


sat(Clauses, Vars) :- 
    problem_setup(Clauses), elim_var(Vars). 

elim_var([]). 
elim_var([Var | Vars]) :- 
    elim_var(Vars), (Var = true; Var = false). 

problem_setup([]). 
problem_setup([Clause | Clauses]) :- 
    clause_setup(Clause), 
    problem_setup(Clauses). 

clause_setup([Pol-Var | Pairs]) :- set_watch(Pairs, Var, Pol). 

set_watch([], Var, Pol) :- Var = Pol. 
set_watch([Pol2-Var2 | Pairs], Var1, Pol1):- 
    watch(Var1, Pol1, Var2, Pol2, Pairs). 

:- block watch(-, ?, -, ?, ?). 
watch(Var1, Pol1, Var2, Pol2, Pairs) :- 
    nonvar(Var1) -> 
        update_watch(Var1, Pol1, Var2, Pol2, Pairs); 
        update_watch(Var2, Pol2, Var1, Pol1, Pairs). 

update_watch(Var1, Pol1, Var2, Pol2, Pairs) :- 
    Var1 == Pol1 -> true; set_watch(Pairs, Var2, Pol2).
2 Likes
3

Really interesting! Im working through the Logic + Control paper as i didn’t really understand the program.
Since my background is C and imperative languages, my solution is pretty much as close to that as i could with logic programming.
Anyways, thanks for the pointer!