我正在尝试解决prolog中的约束处理问题.
我需要在10x10的网格中打包4个5x5,4x4,3x3和2x2的正方形.它们可能不重叠.
我的变量看起来像这样:
Name: SqX(i), i=1..10, domain: 1..10
其中X是5,4,3或2.索引i表示行,域表示网格中的列.
我的第一个约束试图定义正方形的宽度和高度.我这样制定它:
Constraint: SqX(i) > SqX(j)-X /\ i>j-X, range: i>0 /\ j>0
这样可能的点被约束在彼此的X行和列之内.然而,Prolog会停止这些约束并给出以下结果:
Adding constraint "(Sq5_I > Sq5_J-5) /\ (I>J-5)" for values:
I=1, J=1,
I=1, J=2,
I=1, J=3,
I=1, J=4,
I=1, J=5,
I=1, J=6,
=======================[ End Solutions ]=======================
所以它停在那里,甚至没有检查其他方块.我的约束很可能太紧张,但我不明白为什么或如何.有什么建议？
我正在尝试构建一个简单的Prolog SAT求解器.我的想法是用户应该使用Prolog列表输入要在CNF(Conjuctive Normal Form)中解决的布尔公式,例如(A或B)和(B或C)应该表示为sat([[A,B]] ,[B,C]])和Prolog试图找到A,B,C的值.
我的以下代码不起作用,我不明白为什么.在这一行跟踪调用:(7)sat([[true,true]])？ 我期待start_solve_clause([_ G609,_G612]]).
免责声明:对不起几天前我甚至不知道Prolog或SAT问题的糟糕代码.
PS:欢迎提出解决SAT问题的建议.
跟踪
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, …我正在尝试编写一种天真寻找布尔公式(NNF,但不是CNF)模型的算法.
我所拥有的代码可以检查一个现有的模型,但是当被要求查找模型时它会失败(或者没有完成),似乎因为它产生了无数的解决方案member(X, Y).[X|_], [_,X|_], [_,_,X|_]...
到目前为止我所拥有的是:
:- 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, …library(clpb)目前可用于 SICStus（原始版本）和 SWI（通过 mat）。让我很快进入本质：
?- X = 1+1, sat(X), X = 1+1.
X = 1+1.
?- sat(X), X = 1+1.
false.
所以这是一个类似的问题，因为它存在于library(clpfd).
遇到这种情况怎么办？
更新：在library(clpfd)垫子中，现在有用# /1于此目的的函子。理想情况下，加上操作符声明op(150,fx,#)，我们现在可以写：
?- X = 1+1, #X #= Y.
ERROR: Type error: `integer' expected, found `1+1' (a compound)
为了确保完全代数性质，必须声明：
:- set_prolog_flag(clpfd_monotonic, true).
现在，不明确的变量（因此，只能是整数或表达式）会产生实例化错误：
?- 1 + 1 #= Y.
ERROR: Arguments are not sufficiently instantiated
?- 1 + 1 #= #Y.
Y = 2.
我需要找到所有 16 位数字 ( x, y, z) 的三元组（实际上只有在不同三元组中与相同位置的位完美匹配的位），这样
y | x = 0x49ab
(y >> 2) ^ x = 0x530b
(z >> 1) & y = 0x0883
(x << 2) | z = 0x1787
直接使用 8700K 的策略需要大约 2 天，这太多了（即使我会使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。
如果位移位不在等式中，那么这样做将是微不足道的，但是使用位移位很难做同样的事情（甚至可能是不可能的）。
所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（类似于“x XOR 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用 Prolog 语言之类的语言编写（或只是解释他们使用真值表操作）执行所有明确的位将被发现。这个解决方案也很困难：我不知道如何编写这样的解析器，也没有 Prolog 的经验。(*)
所以问题是：这样做的最佳方法是什么？如果是 (*) 那么怎么做呢？
编辑：为了更容易在此处编码数字的二进制模式：
0x49ab = 0b0100100110101011
0x530b = 0b0101001100001011
0x0883 = 0b0000100010000011
0x1787 = 0b0001011110000111
在学习Prolog时,我尝试编写解决CNF问题的程序(性能不是问题),所以我最终得到了以下代码来解决(!x||y||!z)&&(x||!y||z)&&(x||y||z)&&(!x||!y||z):
vx(t).
vx(f).
vy(t).
vy(f).
vz(t).
vz(f).
x(X) :- X=t; \+ X=f.
y(Y) :- Y=t; \+ Y=f.
z(Z) :- Z=t; \+ Z=f.
nx(X) :- X=f; \+ X=t.
ny(Y) :- Y=f; \+ Y=t.
nz(Z) :- Z=f; \+ Z=t.
cnf :-
(nx(X); y(Y); nz(Z)),
(x(X); ny(Y); z(Z)),
(x(X); y(Y); z(Z)),
(nx(X); ny(Y); z(Z)),
write(X), write(Y), write(Z).
有没有更简单,更直接的方法来解决使用这种声明性语言的CNF？
我想在序言中实现以下谓词并将它们用于真值表：and / 2或or / 2，nand / 2，nor / 2，xor / 2
也许有人可以向我展示如何实现and / 2，例如，我可以自己做其他人并将其发布在这里。
解决以下Caliban问题,将每条线索"忠诚地"翻译成Prolog,即尽可能忠诚.
作为一种抽象的简单练习,假设四个无意义的符号a,b,c和d以一个或另一个顺序对应于同样无意义的符号w,x,y和z,并且进一步假设
如果a不是x,那么c不是y.
如果b是y或z,则a是x.
如果c不是w,则b是z.
如果d是y,则b不是x.
如果d不是x,则b是x.两组符号以什么顺序对应？
我尝试了以下代码:
vban(L) :-
L=[[a,C1],[b,C2],[c,C3],[d,C4]],
( member(C1,[w,y,z]) -> member(C3,[w,x,z])),
( member(C2,[y,z]) -> member(C1,[x])),
( member(C3,[x,y,z]) -> member(C2,[z])),
( member(C4,[y]) -> member(C2,[w,y,z])),
( member(C4,[w,y,z]) -> member(C2,[x])).
但它显示失败.任何帮助将不胜感激.
我即将在Prolog中实现逻辑术语的证明者.我当前的代码并不是真的可以呈现,因此,我只是说,我想要我的程序做什么,希望你可以给我一些很好的建议:)
它应该采用变量列表(也就是说逻辑参数),其次是包含这些参数的逻辑公式(例如'not'(A 'and' B) 'or' 'not'(B 'and' C) 'or' ...,依此类推).
作为输出,我希望我的程序能够以可能的一致性分配进行响应.单个参数可以是true(1)或false(0).
所以我的目标是回归A=0, B=0, C=0 ; A=1等等.
我很高兴有关我的计划的每一个帮助:)