Prolog SAT Solver

Question

私は単純なProlog SATソルバーを構築しようとしています。私が考えているのは、ユーザが、Prologリスト（例えばAまたはB）を使ってCNF（Conjuctive Normal Form）で解決される論理式を入力し、sat（[A、B] 、[B、C]]）とPrologがA、B、Cの値を見つけようとします。

私の次のコードは機能しません。トレースのこの行で呼び出し：（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]]) ? 

の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

私は私の前に私のプロローグ通訳があればいいのに...しかし、なぜあなたは

のようなルールを記述カント

sat(Stmt) :- 
    call(Stmt). 

してから...

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

多分あなたは、彼らはので、これらのルールを追加し、trueまたはfalseのいずれかであることを制約するために何かを必要とする（ところで; is or）実行して

is_bool(true). 
is_bool(false). 

と

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

を照会し、あなたの例を呼び出すウルド

BTW - これは、単に満足する用語を見つけるために単純にDFSを実行することです。スマートなヒューリスティックなものはありません。

Answer 2

（SICStus）PrologのSAT解答についてはHoweとKingの素晴らしい論文があります（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 3

一つは、SATを解決するために、CLP（FD）を使用することができます。ただ、CNF で始まり、その後句ことを守ってください。

x1 v .. v xn 

が制約として表すことができる。

x1 + .. + xn #> 0 

さらに負リテラルのために：

~x 

は単純に使用します。

1-x 

変数をドメイン0..1 に制限し、ラベリングを呼び出す必要があります。変数に の値が返されると、元の の式が充足可能であることがわかります。ここで

はジョー・レーマンのテストを実行している、例の実行です：有限領域を超える

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 4

時には次のコードが発見されました。句は、命題変数に明確な正の非ゼロ
整数を割り当てることによって
を表現している。ここで

% 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([], []). 

は例がために実行されます。

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

次のプロローグコードは非常にうまく機能しているようです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の亜種だと思います。