Brut-force Prolog Rozwiązywanie problemów SAT dla formuł logicznych

Question

Próbuję napisać algorytm, który naiwnie szuka modeli formuły logicznej (NNF, ale nie CNF).

Kod mam może sprawdzić istniejący model, ale to nie (lub nie zakończyć) pytany, aby znaleźć modele, z pozoru, ponieważ generuje on nieskończenie wiele rozwiązań dla member(X, Y) wzdłuż linii [X|_], [_,X|_], [_,_,X|_]...

Co ja do tej pory to:

:- 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]]). 

Czy istnieje lepsza struktura danych dla F, lub jakiś inny sposób, że częściowo wystąpienia listy mogą zostać odcięte?

Edytuj: Dodano definicje i przykłady.

Answer 1

Rozwiązałem go pisząc generate_model predykat, który stworzył wcześniej zdefiniowanej listy z dokładnie jednym elementem dla każdej zmiennej:

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 2

Zastosowanie clpb!

 
:- use_module (library(clpb)). 

zapytania próbki za pomocą sat/1:

 
?- sat (~(~ (A * B) + (C * D))). 
A = B, B = 1, sat(1#C*D). 

niektórych zmiennych (A i B) już zostały związały się dokładnie jedna wartość logiczną (w powyższym zapytaniu), ale wyszukiwarka nie jest jeszcze zakończona (co jest wskazywane przez pozostałe cele).

wyzwolić inteligentne brute-force wyliczenie wszystkich rozwiązań korzystania labeling/1 tak:

 
?- sat(~(~ (A * B) + (C * D))), labeling ([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 3

Czy ja rozumiem, że jesteś zadowolony z jednego modelu. Ty nie potrzebujesz etykiet ani sat_count. Oto alternatywa model finder, która jest podobna do twojej, ale zwraca tylko spójne modele.

Po znalezieniu modeli liczników należy podać negację wzoru, aby znaleźć model. Orzecznik labirynt/3 został opracowany jako negatywny realizacji pozytywnego orzecznika próbnym/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). 

Można znaleźć modele liczników do wszystkich poniższych złudnych:

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). 

Oto przykład run :

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)] 

Co ciekawe, rzecz jest znacznie szybsza niż CLP (B). Oto niektóre czasy działające z tym samym problemem w CLP (B) i z labiryntem:

?- 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