Prolog SAT Solver

Question

J'essaye de construire un simple solveur Prolog SAT. Mon idée est que l'utilisateur doit entrer la formule booléenne à résoudre dans CNF (forme normale conjugale) en utilisant des listes de prolog, par exemple (A ou B) et (b ou c) doit être présentée comme SAT ([[A, B] , [B, c]]) et procédures de prolog pour trouver les valeurs pour a, b, C.

Mon code suivant ne fonctionne pas et je ne comprends pas pourquoi. Sur cette ligne de la trace Appel: (7) SAT ([[true, true]])? je m'attendais à start_solve_clause ([_ G609, _G612]]).

Clause de non-responsabilité: Désolé pour le code merdique que je ne connaissais même pas sur Prolog ou le problème SAT il y a quelques jours.

PS: Les conseils sur la résolution du SAT sont les bienvenus.

Trace

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]]) ?  

Source de 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).