Пролог САТ Солвер

Question

Я пытаюсь создать простой решатель Prolog SAT.Моя идея состоит в том, что пользователь должен ввести булеву формулу, которая должна быть решена в CNF (Conjctive Normal Form) с использованием списков пролога, например (A или B) и (B или C) должны быть представлены как sat ([[A, B], [B, C]]) и Пролог продолжает поиск значений для A, B, C.

Мой следующий код не работает, и я не понимаю, почему.В этой строке следа Вызов: (7) сел ([[истина, правда]])? Я ожидал 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).

Answer 1

Существует замечательная статья Хоу и Кинга о SAT Solving в (SICStus) Prolog (см. 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 приведены следующие предложения:1007 *

Answer 2

Можно использовать CLP (FD) для решения SAT. Просто начните с 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.

Bye

Программирование логики ограничений по конечным доменам
http://www.swi -prolog.org / человек / clpfd.html

Answer 3

Иногда встречается следующая кодировка.Предложения
представлены назначением различных положительных ненулевых
целых чисел пропозициональным переменным:

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

Кажется, что следующий код Пролога работает достаточно хорошо:

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

Вот пример выполнения теста Джо Леманна:

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

Код, вдохновленный https://gist.github.com/rla/4634264.
Я полагаю, что это вариант алгоритма DPLL сейчас.

Answer 4

Хотелось бы, чтобы передо мной был мой интерпретатор пролога ... но почему вы не можете написать правило типа

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, чтобы найти удовлетворяющие термины.никакой умной эвристики или чего-то еще.