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

Я пытаюсь создать простой решатель 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).
Источник

4 ответа

Решение

Мне бы хотелось, чтобы передо мной был мой пролог-переводчик... но почему вы не можете написать такое правило?

sat(Stmt) :-
  call(Stmt).

и тогда вы бы вызвали свой пример, выполнив (кстати ; is или)

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

Источник

Есть замечательная статья Хоу и Кинга о 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 как это:

| ?- 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
Источник

Можно использовать 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.

до свидания

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

Источник

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

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

Вот пример запуска для теста Джо Леманна:

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

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

Источник
Другие вопросы по тегам