Решатель грубой силы Prolog SAT для логических формул

Question

Я пытаюсь написать алгоритм, который наивно ищет модели булевой формулы (NNF, но не CNF).

У меня есть код, который может проверить существующую модель, но он потерпит неудачу (или не завершится), когда его попросят найти модели, по-видимому, потому что он генерирует бесконечно много решений для member(X, Y) по линии [X|_], [_,X|_], [_,_,X|_]...

То, что я до сих пор, это:

:- op(100, fy, ~).    
:- op(200, xfx, /\).  
:- op(200, xfx, \/).  
:- op(300, xfx, =>).  
:- op(300, xfx, <=>). 

formula(X) :- atom(X).
formula(~X) :- formula(X).
formula(X /\ Y) :- formula(X), formula(Y).
formula(X \/ Y) :- formula(X), formula(Y).
formula(X => Y) :- formula(X), formula(Y).
formula(X <=> Y) :- formula(X), formula(Y).

model(1, _).
model(X, F) :- atom(X), member([X, 1], F).
model(~X, F) :- atom(X), member([X, 0], F). % NNF
model(A /\ B, F) :- model(A, F), model(B, F).
model(A \/ B, F) :- (model(A, F); model(B, F)).
model(A => B, F) :- model(~A \/ B, F).
model(A <=> B, F) :- model((A => B) /\ (B => A), F).

sat(A) :- model(A, F), \+ (member([X, 1], F), member([X, 0], F)).


%%% examples:
% formula(~(~ (a /\ b) \/ (c => d))).
% model(a, [[a,1]]).

Есть ли лучшая структура данных для Fили каким-то другим способом частично обрезанные списки могут быть обрезаны?

Изменить: добавлены определения и примеры.

Answer 1

Используйте clpb!

: - use_module ( библиотека (clpb)).

Пример запроса с использованием sat/1:

? - сел (~(~ (A * B) + (C * D))).
A = B, B = 1, сб (1#C*D).

Некоторые переменные (A а также B) уже были привязаны только к одному логическому значению (в приведенном выше запросе), но поиск еще не завершен (на что указывают остаточные цели).

Для запуска умного перебора всех решений используйте перебор labeling/1 вот так:

? - сат (~(~ (A * B) + (C * D))), маркировка ([A,B,C,D]).
   A = B, B = 1, C = D, D = 0;  A = B, B = D, D = 1, C = 0;  A = B, B = C, C = 1, D = 0.

Answer 2

Я решил это, написав generate_model Предикат, который создал предопределенный список с ровно одним элементом для каждой переменной:

generate_model([], []).
generate_model([X|T], [[X,_]|T2]) :- generate_model(T, T2).

sat(A) :- 
  var_list(A, Vars),
  generate_model(Vars, F),
  model(A, F).

Answer 3

Понимаю ли я вас, что вы довольны единственной моделью. Вам не нужна маркировка или sat_count. Вот альтернативный искатель моделей, который похож на ваш, но вернет только согласованные модели.

Поскольку он находит счетные модели, вам нужно указать отрицательную формулу, чтобы найти модель. Предикатный лабиринт /3 был разработан как отрицательная реализация положительного предикатного доказательства /2:

% Find a counter model.
% maze(+Norm,+List,-List)
maze(or(A,_),L,_) :- member(A,L), !, fail.
maze(or(A,B),L,R) :- !, inv(A,C), maze(B,[C|L],R).
maze(and(A,_),L,R) :- maze(A,L,R), !.
maze(and(_,B),L,R) :- !, maze(B,L,R).
maze(A,L,_) :- member(A,L), !, fail.
maze(A,L,M) :- oneof(L,B,R), connective(B), !, 
                 inv(A,C), inv(B,D), maze(D,[C|R],M).
maze(A,L,[B|L]) :- inv(A,B).

Он может найти встречные модели для всех следующих ошибок:

Affirming a Disjunct: (p v q) & p => ~q.
Affirming the Consequent: (p => q) & q => p.
Commutation of Conditionals: (p => q) => (q => p).
Denying a Conjunct: ~(p & q) & ~p => q.
Denying the Antecedent: (p => q) & ~p => ~q.
Improper Transposition: (p => q) => (~p => ~q).

Вот пример запуска:

Jekejeke Prolog 2, Runtime Library 1.2.5
(c) 1985-2017, XLOG Technologies GmbH, Switzerland

?- negcase(_,N,F), norm(F,G), maze(G,[],L), 
   write(N), write(': '), sort(L,R), write(R), nl, fail; true.
Affirming a Disjunct: [pos(p),pos(q)]
Affirming the Consequent: [neg(p),pos(q)]
Commutation of Conditionals: [neg(p),pos(q)]
Denying a Conjunct: [neg(p),neg(q)]
Denying the Antecedent: [neg(p),pos(q)]
Improper Transposition: [neg(p),pos(q)]

Интересно, что это намного быстрее, чем CLP(B). Вот некоторые примеры выполнения той же проблемы в CLP (B) и в лабиринте:

?- time((between(1,1000,_), negcaseclp(_,N,F,L),
   sat(~F), once(labeling(L)), fail; true)).
% Up 296 ms, GC 3 ms, Thread Cpu 250 ms (Current 01/27/18 00:34:20)
Yes 
?- time((between(1,1000,_), negcase(_,_,F),
   norm(F,G), maze(G,[],_), fail; true)).
% Up 82 ms, GC 0 ms, Thread Cpu 78 ms (Current 01/27/18 00:30:21)
Yes