Prolog SAT解算器

Question

我正在尝试构建一个简单的Prolog SAT求解器.我的想法是用户应该使用Prolog列表输入要在CNF(Conjuctive Normal Form)中解决的布尔公式,例如(A或B)和(B或C)应该表示为sat([[A,B]] ,[B,C]])和Prolog试图找到A,B,C的值.

我的以下代码不起作用,我不明白为什么.在这一行跟踪调用:(7)sat([[true,true]])？ 我期待start_solve_clause([_ G609,_G612]]).

免责声明:对不起几天前我甚至不知道Prolog或SAT问题的糟糕代码.

PS:欢迎提出解决SAT问题的建议.

跟踪

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

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

Answer 1

Howe和King有一篇关于SAT求解(SICStus)Prolog的精彩论文(见http://www.soi.city.ac.uk/~jacob/solver/index.html).

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

这些条款在CNF中给出如下:

| ?- sat([[true-X,false-Y],[false-X,false-Y],[true-X,true-Z]],[X,Y,Z]).
 X = true,
 Y = false,
 Z = true ? ;
 X = false,
 Y = false,
 Z = true ? ;
 X = true,
 Y = false,
 Z = false ? ;
no

Answer 2

我希望我的序言解释器在我面前......但是为什么你不能写一个像这样的规则

sat(Stmt) :-
  call(Stmt).

然后你可以通过执行 (btw ; is or )来调用你的示例

?- sat(((A ; B), (B ; C))).

也许你需要一些东西来限制它们是真还是假，所以添加这些规则......

is_bool(true).
is_bool(false).

并查询

?- is_bool(A), is_bool(B), is_bool(C), sat(((A ; B), (B ; C))).

顺便说一句——这个实现只是简单地进行 DFS 来找到令人满意的术语。没有智能启发法或任何东西。