Risolutore Prolog solutore di forza Brute-force per formule booleane

Question

Sto provando a scrivere un algoritmo che cerca ingenuamente modelli di una formula booleana (NNF, ma non CNF).

Il codice che ho può controllare un modello esistente, ma sarà a mancare (o non finire) quando viene chiesto di trovare modelli, apparentemente perché genera infinite soluzioni per member(X, Y) lungo le linee di [X|_], [_,X|_], [_,_,X|_]...

Quello che ho hanno finora è questo:

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

c'è una struttura di dati migliore per la F, o qualche altro modo le liste parzialmente istanziati possono essere tagliati fuori?

Modifica: aggiunte definizioni ed esempi.

Answer 1

ho risolto scrivendo una generate_model predicato che ha creato un elenco predefinito con esattamente un elemento per ogni variabile:

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

Usa clpb!

 
:- use_module (library(clpb)). 

interrogazione campione utilizzando sat/1:

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

Alcune variabili (A e B) già sono stati legati ad esattamente un valore booleano (nel precedente query), ma la ricerca non è ancora completa (che è indicato da obiettivi residui).

Per attivare la smart forza bruta enumerazione di tutte le soluzioni utilizzano labeling/1 in questo modo:

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

Ti capisco, che si è soddisfatti con un unico modello. Tu non hai bisogno di etichettatura o sat_count. Ecco un'alternativa model finder, che è simile alla tua, ma restituirà solo modelli coerenti.

Poiché trova modelli contatore, è necessario fornire la negazione della formula per trovare un modello. Il labirinto predicato/3 è stato sviluppato come un'implementazione negativo del predicato positiva prova/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). 

Può trovare modelli contatore per tutti i seguenti errori:

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

Ecco un run esempio :

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

È interessante notare che la cosa è molto più veloce di CLP (B). Ecco alcuni tempi con lo stesso problema in CLP (B) e con labirinto:

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