Prolog SAT求解器

Question

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

我的以下代码不起作用，我不明白为什么。在跟踪的这一行 Call: (7) sat([[true, true]]) ? 我期待 start_solve_clause([_G609, _G612]])。

免责声明：抱歉，几天前我什至不知道 Prolog 或 SAT 问题的糟糕代码。

P.S.：欢迎提供有关解决 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).

Answer 1

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

Answer 2

可以使用 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

Answer 3

有时会找到以下编码。子句是
通过分配不同的正非零表示
整数到命题变量：

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 algorithm 的变体。

Answer 4

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

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 来找到令人满意的条款。没有智能启发式或任何东西。