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

序言源

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

score 6 · Accepted Answer

Howe 和 King 有一篇精彩的论文，关于 (SICStus) Prolog 中的 SAT 求解（参见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

score 4 · Accepted Answer

可以使用 CLP(FD) 来解决 SAT。只需从 CNF 开始，然后观察一个子句：

x1 v .. v xn

可以表示为一个约束：

x1 + .. + xn #> 0

进一步对于否定文字：

~x

只需使用：

1-x

您需要将变量限制为域 0..1 并调用标签。只要标签为变量返回一些值，您就知道您的原始公式是可以满足的。

这是一个运行示例，运行 Joe Lehmann 的测试：

Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 6.5.2)
Copyright (c) 1990-2013 University of Amsterdam, VU Amsterdam

?- use_module(library(clpfd)).

?- L = [X,Y,Z], L ins 0..1, X+1-Y #> 0, 1-X+1-Y #> 0, X+Z #> 0, label(L).
X = Y, Y = 0,
Z = 1 ;
X = 1,
Y = Z, Z = 0 ;
X = Z, Z = 1,
Y = 0.

再见

有限域上的约束逻辑编程
http://www.swi-prolog.org/man/clpfd.html

score 3 · Accepted Answer

有时会发现以下编码。
通过将不同的正非零
整数分配给命题变量来表示子句：

x1 v .. v xn --> [x1, .. , xn]
~x           --> -x

似乎以下 Prolog 代码运行良好：

% mem(+Elem, +List)
mem(X, [X|_]).
mem(X, [_|Y]) :-
    mem(X, Y).

% sel(+Elem, +List, -List)
sel(X, [X|Y], Y).
sel(X, [Y|Z], [Y|T]) :-
    sel(X, Z, T).

% filter(+ListOfList, +Elem, +Elem, -ListOfList)
filter([], _, _, []).
filter([K|F], L, M, [J|G]) :-
    sel(M, K, J), !,
    J \== [],
    filter(F, L, M, G).
filter([K|F], L, M, G) :-
    mem(L, K), !,
    filter(F, L, M, G).
filter([K|F], L, M, [K|G]) :-
    filter(F, L, M, G).

% sat(+ListOfLists, +List, -List)
sat([[L|_]|F], [L|V]):-
    M is -L,
    filter(F, L, M, G),
    sat(G, V).
sat([[L|K]|F], [M|V]):-
    K \== [],
    M is -L,
    filter(F, M, L, G),
    sat([K|G], V).
sat([], []).

这是 Joe Lehmanns 测试用例运行的示例：

?- sat([[1,-2],[-1,-2],[1,3]], X).
X = [1,-2] ;
X = [-1,-2,3] ;
No

受https://gist.github.com/rla/4634264启发的代码。
我猜它现在是DPLL 算法的一种变体。

score 1 · Accepted Answer

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

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

顺便说一句——这个 impl 只是简单地做一个 DFS 来找到令人满意的条款。没有智能启发式或任何东西。

prolog - Prolog SAT求解器

4 回答 4

Related

Reference