Prolog SAT Solver

Question

Tôi đang cố gắng xây dựng một giải pháp Prolog SAT đơn giản. Ý tưởng của tôi là người dùng nên nhập công thức boolean để được giải quyết trong CNF (Conjuctive Normal Form) sử dụng danh sách Prolog, ví dụ (A hoặc B) và (B hoặc C) nên được trình bày như sat ([[A, B] , [B, C]]) và quy trình Prolog để tìm các giá trị cho A, B, C.

Mã sau của tôi không hoạt động và tôi không hiểu tại sao. Trên dòng này của dấu vết Gọi: (7) sat ([[true, true]])? Tôi đã mong đợi start_solve_clause ([_ G609, _G612]]).

Tuyên bố từ chối trách nhiệm: Xin lỗi vì mã crappy mà tôi thậm chí không biết về Prolog hoặc bài toán SAT cách đây vài ngày.

P.S .: Lời khuyên về cách giải quyết SAT được hoan nghênh.

vết

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 Nguồn

% 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

tôi muốn tôi có thông dịch viên prolog của tôi trước mặt tôi ... nhưng tại sao bạn không thể viết một quy tắc như

sat(Stmt) :- 
    call(Stmt). 

và sau đó bạn Ould gọi ví dụ của bạn bằng cách thực hiện (btw ; is or)

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

có thể bạn cần một cái gì đó để hạn chế rằng họ là đúng hoặc sai để thêm các quy tắc ...

is_bool(true). 
is_bool(false). 

và truy vấn

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

BTW - impl này đơn giản chỉ đơn giản là làm một DFS để tìm các điều kiện thỏa mãn. không có heuristic thông minh hay bất cứ điều gì.

Answer 2

Có một bài báo tuyệt vời của Howe và King về SAT Solving in (SICStus) Prolog (xem 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). 

Các điều khoản được đưa ra trong CNF như thế này:

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

Người ta có thể sử dụng CLP (FD) để giải quyết thi SAT.Chỉ cần bắt đầu với một CNF và sau đó quan sát rằng một điều khoản:

x1 v .. v xn 

có thể được biểu diễn như một hạn chế:

x1 + .. + xn #> 0 

Tiếp tục cho một chữ tiêu cực:

~x 

Đơn giản chỉ cần sử dụng:

1-x 

Bạn cần hạn chế các biến đối với miền 0..1 và gọi nhãn. Ngay sau khi ghi nhãn trả về một số giá trị cho các biến, bạn biết rằng công thức ban đầu của bạn là là thỏa đáng.

Dưới đây là một ví dụ chạy, chạy sự thử thách của 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. 

Bye

Hạn chế logic lập trình trên Domains hữu hạn
http://www.swi-prolog.org/man/clpfd.html

Answer 4

Đôi khi các mã sau đây được tìm thấy. Các khoản được
đại diện bằng cách gán cho biệt tích cực khác không
số nguyên cho các biến mệnh đề:

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

Dường như mã Prolog sau hoạt động khá tốt:

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

Dưới đây là một ví dụ chạy Trường hợp kiểm tra Joe Lehmanns:

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

Mã lấy cảm hứng từ https://gist.github.com/rla/4634264.
Tôi đoán đây là biến thể của số DPLL algorithm ngay bây giờ.