Prolog SAT Solver

Question

Sto cercando di costruire un semplice risolutore di set Prolog. La mia idea è che l'utente dovrebbe inserire la formula booleana da risolvere in CNF (forma normale congiuntiva) usando elenchi di prolog, ad esempio (A o B) e (B o C) devono essere presentati come SAT ([[A, B] , [B, c]]) e procedure prolog per trovare i valori per A, B, C.

Il mio codice seguente non funziona e non capisco perché. Su questa linea della traccia Chiama: (7) sab ([[vero, vero]])? stavo aspettando start_solve_clause ([_ g609, _g612]]).

Disclaimer: Ci scusiamo per il codice schifoso che non sapevo nemmeno di Prolog o del problema SAT qualche giorno fa.

PS: Il consiglio sulla risoluzione del SAT è il benvenuto.

Traccia

sat([[X, Y, Z], [X, Y]]).
Call: (6) sat([[_G609, _G612, _G615], [_G609, _G612]]) ? creep
Call: (7) start_solve_clause([_G609, _G612, _G615]) ? creep
Call: (8) solve_clause([_G615], _G726) ? creep
Call: (9) or(_G725, _G615, true) ? creep
Exit: (9) or(true, true, true) ? creep
Exit: (8) solve_clause([true], true) ? creep
Call: (8) or(_G609, _G612, true) ? creep
Exit: (8) or(true, true, true) ? creep
Exit: (7) start_solve_clause([true, true, true]) ? creep
Call: (7) sat([[true, true]]) ?  

Fonte prolog

% Knowledge base
or(true, true, true).
or(false, false, false).
or(true, false, true).
or(false, true, true).

or(not(true), true, true).
or(not(false), false, true).
or(not(true), false, false).
or(not(false), true, true).

or(true, not(true), true).
or(false, not(false), true).
or(true, not(false), true).
or(false, not(true), false).

% SAT solver
sat([]).
sat([Clause | Tail]) :- start_solve_clause(Clause), sat(Tail).

% Clause solver
start_solve_clause([Var1, Var2 | Tail]) :- solve_clause(Tail, Result), or(Var1, Var2, Result).

solve_clause([X | []], Result) :- or(Result, X, true).
solve_clause([X | Tail], Result) :- solve_clause(Tail, Result2), or(Result, X, Result2).