Prolog SAT Solver

Question

Estoy tratando de construir un simple solucionador de Prolog SAT. Mi idea es que el usuario debe ingresar la fórmula booleana a resolver en CNF (Forma Normal Conjugativa) usando listas de Prolog, por ejemplo (A o B) y (B o C) deben presentarse como sat ([[A, B] , [B, C]]) y Prolog procede a encontrar los valores para A, B, C.

Mi siguiente código no funciona y no entiendo por qué. En esta línea de la traza Llamada: (7) sat ([[true, true]])? Esperaba start_solve_clause ([_ G609, _G612]]).

Descargo de responsabilidad: Disculpa por el código de mierda que ni siquiera sabía sobre Prolog o el problema de SAT hace unos días.

P.S .: Asesoramiento para resolver el SAT es bienvenido.

traza

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

Prolog Fuente

% 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

Me gustaría tener mi intérprete Prolog frente a mí ... pero ¿por qué no puedo escribir una regla como

sat(Stmt) :- 
    call(Stmt). 

y luego tu Ould invocar el ejemplo haciendo (por cierto ; is or)

?- sat(((A ; B), (B ; C))). 

tal vez usted necesita algo para limitar que son verdaderas o falsas por lo que añadir estas reglas ...

is_bool(true). 
is_bool(false). 

y consultar

?- is_bool(A), is_bool(B), is_bool(C), sat(((A ; B), (B ; C))). 

BTW - esto impl simplemente sería hacer un DFS para encontrar términos satisfactorios. sin heurística inteligente ni nada.

Answer 2

Hay un maravilloso documento de Howe and King sobre SAT Resolviendo en (SICStus) Prolog (ver 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). 

Las cláusulas se dan en CNF como esto:

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

Answer 3

Uno puede usar CLP (FD) para resolver SAT.Simplemente comienza con una CNF y luego observar que una cláusula:

x1 v .. v xn 

se puede representar como una limitación:

x1 + .. + xn #> 0 

Además de un literal negativo:

~x 

simplemente usar:

1-x 

Debe restringir las variables al dominio 0..1 e invocar el etiquetado. Tan pronto como el etiquetado arroje un valor de para las variables, sabrá que su fórmula original es satisfactoria.

Aquí se muestra un ejemplo de ejecución, ejecutar la prueba de Joe Lehmann:

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. 

adiós

restricción lógica de programación sobre finitos Dominios
http://www.swi-prolog.org/man/clpfd.html

Answer 4

veces la siguiente codificación se encuentra. Cláusulas se
representados mediante la asignación de diferentes distintos de cero
enteros positivos a las variables proposicionales:

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

Parece que el siguiente código Prolog funciona bastante bien:

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

Aquí es un ejemplo funcione durante Caso de prueba de Joe Lehmanns:

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

Código inspirado en https://gist.github.com/rla/4634264.
Supongo que ahora es una variante del DPLL algorithm.