Prolog SAT求解器 [英] Prolog SAT Solver

问题描述

我正在尝试构建一个简单的 Prolog SAT 求解器.我的想法是用户应该使用Prolog列表输入要在CNF(Conjuctive Normal Form)中求解的布尔公式，例如(A或B)和(B或C)应该表示为sat([[A，B], [B, C]]) 和 Prolog 继续查找 A、B、C 的值.

I'm trying to build a simple Prolog SAT solver. My idea is that the user should enter the boolean formula to be solved in CNF (Conjuctive Normal Form) using Prolog lists, for example (A or B) and (B or C) should be presented as sat([[A, B], [B, C]]) and Prolog procedes to find the values for A, B, C.

我的以下代码不起作用，我不明白为什么.在跟踪的这一行 Call: (7) sat([[true, true]]) ? 我期待 start_solve_clause([_G609, _G612]]).

My following code is not working and I'm not understanding why. On this line of the trace Call: (7) sat([[true, true]]) ? I was expecting start_solve_clause([_G609, _G612]]).

免责声明:抱歉，几天前我什至不知道 Prolog 或 SAT 问题的糟糕代码.

Disclaimer: Sorry for the crappy code I didn't even know about Prolog or the SAT problem a few days ago.

P.S.:欢迎提供有关解决 SAT 的建议.

P.S.: Advice on solving the SAT is welcome.

追踪

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

序言源

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

推荐答案

我希望我的 prolog 解释器在我面前...但是你为什么不能写一个规则像

i wish i had my prolog interpreter in front of me... but why cant you write a rule like

sat(Stmt) :-
  call(Stmt).

然后您将通过执行 (btw ; 是或)

and then you would invoke your example by doing (btw ; is or)

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

也许你需要一些东西来限制它们是真还是假，所以添加这些规则......

maybe you need something to constrain that they are either true or false so add these rules...

is_bool(true).
is_bool(false).

查询

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

顺便说一句——这个 impl 只是简单地做一个 DFS 来找到令人满意的条款.没有智能启发式或任何东西.

BTW -- this impl simply would simply be doing a DFS to find satisfying terms. no smart heuristic or anything.

这篇关于Prolog SAT求解器的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！