Prolog SAT 求解器

Question

我正在尝试构建一个简单的 Prolog SAT 求解器。我的想法是，用户应该使用 Prolog 列表输入要在 CNF（合取范式）中求解的布尔公式，例如 (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 问题。

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

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

有时会发现以下编码。条款是
通过分配不同的正非零来表示
整数到命题变量：

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

Answer 3

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

sat(Stmt) :-
  call(Stmt).

，然后你可以通过执行（btw ; 是或）

?- 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 来找到满意的术语。没有智能启发法或任何东西。

Answer 4

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