Prolog SAT解算器 [英] Prolog SAT Solver

问题描述

我正在尝试构建一个简单的Prolog SAT解算器.我的想法是，用户应使用Prolog列表输入要在CNF(共轭范式)中求解的布尔公式，例如(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.

我的以下代码无法正常工作，我也不明白为什么.在跟踪的这一行上，致电:(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).

推荐答案

我希望我能在我面前看到我的序言解释器...但是为什么你不能写这样的规则

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

顺便说一句-这暗示只是简单地做一个DFS来找到满意的条件.没有灵巧的启发法.

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

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