14

シンプルな Prolog SAT ソルバーを構築しようとしています。私の考えでは、ユーザーは Prolog リストを使用して CNF (Conjucutive 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).
4

4 に答える 4

6

(SICStus) Prolog ( http://www.soi.city.ac.uk/~jacob/solver/index.htmlを参照) に SAT 解法に関する Howe と King による素晴らしい論文があります。

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
于 2011-02-12T13:17:55.047 に答える
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 Lehmann のテスト ケースの実行例です。

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

https://gist.github.com/rla/4634264に触発されたコード。現在はDPLL アルゴリズム
の変種だと思います。

于 2013-09-08T14:47:39.670 に答える
1

プロローグのインタープリターが目の前にあればいいのに...でも、次のようなルールを書けないのはなぜですか

sat(Stmt) :-
  call(Stmt).

次に、 (btw ; is or )を実行して例を呼び出します

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

おそらく、それらが true または false であることを制約する何かが必要なので、これらのルールを追加してください...

is_bool(true).
is_bool(false).

とクエリ

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

ところで -- この impl は単に DFS を実行して満足のいく用語を見つけるだけです。スマートヒューリスティックなどはありません。

于 2011-02-10T15:02:20.307 に答える