问题标签 [clpb]

我即将在 Prolog 中实现逻辑术语的证明器。我当前的代码不是很漂亮，因此，我只想说明我想让我的程序做什么，希望你能给我一些好的建议:)

它应该有一个变量列表（可以说是逻辑参数），其次是一个包含这些参数的逻辑公式（例如'not'(A 'and' B) 'or' 'not'(B 'and' C) 'or' ...等等）。

作为输出，我希望我的程序以可能的一致分配来响应。单个参数可以是true ( 1) 或false ( 0)。

所以我的目标是像A=0, B=0, C=0 ; A=1这样的回报。

我很高兴为我的程序提供每一个帮助:)

我正在尝试创建一个 SAT 求解器，它通过 Boolean Grobner Bases 的实现从结合范式 (CNF) 转换：

a) 对特定变量的否定，例如-x将转换为1+x。
b）添加相同的变量将导致0。例如x + x = 0。（将需要使用 XOR）。
c) 相同变量的乘法将产生相同的变量。例如x*x = x。

目前，我仍在尝试弄清楚如何开始，因为输入必须是文本文件，就像他们在 SAT 比赛中一样，如下所示：

谢谢。

编辑

对于 SWI-Prolog 的 CLP(B) 库，我想实现sat_count/2的加权版本

我没有找到用于修改代码的库的详细文档。如何实现 sat_count/2 的加权版本？

编辑 1（2017 年 1 月 11 日）：

感谢@mat 的回复，我无法添加评论，因为我没有足够的声誉。

weighted_sat_count/3应该采用一对权重列表，每个变量一个权重（True 的权重和 False 状态的权重），然后其他两个参数与sat_count/2.

计数是每个可接受分配的权重之和。每个可接受分配的权重是每个变量权重的乘积。

计算结果的算法是：

使用与计算的权重相关联的访问节点的地图，该算法可以更有效。 weight[,]是权重对的列表，1 表示 True，0 表示 False。

编辑 2（2017 年 3 月 11 日）：

例如：

1. A+B+C，一个简单的SAT公式

2. 权重对列表：[(0.7, 0.3), (0.9, 0.1), (0.5, 0.5)]，每个变量一个

?- weighted_sat_count([(0.7, 0.3), (0.9, 0.1), (0.5, 0.5)], +([A, B, C]), Count).

有三个人（亚历克斯、布鲁克和科迪），其中一个是骑士，一个是流氓，一个是间谍。骑士总是说真话，流氓总是撒谎，间谍要么撒谎要么说真话. 亚历克斯说：“科迪是个无赖。” 布鲁克说：“亚历克斯是个骑士。” 科迪说：“我是间谍。” 谁是骑士，谁是无赖，谁是间谍？通过 prolog clpb 解决这个难题

SWI-Prolog CLP(B) 有一个 sat_count/2 谓词。SICStus Prolog CLP(B) 中的替代品是什么？到目前为止，我选择了：

但以上只是使用标签蛮力，所以不是一个真正的智能解决方案。有没有更好的方法在 SICStus Prolog 中执行 sat_count/2 ？

SWI-Prolog CLP(B) 有一个 weighted_maximum/2 谓词。SICStus Prolog CLP(B) 中的替代品是什么？这是一个例子：

我还没有建议。对于 weighted_maximum/3 内的伪布尔约束，我是否需要退回到 SICStus CLP(FD)？这甚至会起作用吗？

我需要找到所有 16 位数字 ( x, y, z) 的三元组（嗯，实际上只有在不同三元组中与相同位置的位完全匹配的位），这样

直截了当的策略在 8700K 上需要大约 2 天，这太多了（即使我将使用我可以访问的所有 PC（R5-3600、i3-2100、i7-8700K、R5-4500U、3xRPi4、RPi0/W）这将花费太多时间）。

如果位移不在方程式中，那么这样做将是微不足道的，但是使用位移来做同样的事情太难了（甚至可能是不可能的）。

所以我想出了一个非常有趣的解决方案：将方程解析为关于数字位的语句（例如“x 的第 3 位 XOR y 的第 1 位等于 1”），并且所有这些语句都用类似 Prolog 语言的语言编写（或者只是解释他们使用运算的真值表）执行所有明确的位将被发现。这个解决方案也很难：我不知道如何编写这样的解析器，也没有使用 Prolog 的经验。(*)

所以问题是：最好的方法是什么？如果是 (*) 那么该怎么做呢？

编辑：为了更容易在这里编码数字的二进制模式：

我正在使用 sat/1 和更自然的语言方法使用自定义命题 A 说 B 和 false() 编写一些骑士和无赖拼图。

问题 3 表述如下：

你遇到了三个居民，A、B 和 C。

A 说：“我们三个都是流氓”。

B 说：“我们当中正好有一个是骑士”。

但是，由于某种原因，在我使用自定义命题的解决方案中，prolog 给了我未知的过程 card/2。这是代码（参见 question3_again 命题）。

我尝试计算骑士的数量并改用下面的这个解决方案，但它给了我不正确的答案（我添加了false(A #= B) :- A #\= B.这样的错误可能是关于整数的原因）：

谁能给我一盏灯？

先感谢您！