问题标签 [sat]

我们给定一个 n*m 网格，它在各个点都有障碍物，即机器人的起始和结束位置。任务是找到一条从头到尾的无碰撞路径。这个问题将被建模为 SAT 问题。

请指导我在这种情况下应该做什么以获得最佳解决方案。

我是 sat4j 库的新手。我如何定义含义，例如(A1 v A2 v A3) => (A1 ∧ A4)使用 sat4j 并找到所有变量的布尔值？

我找到了 sat4j 的单元测试，而不是我在下面的清单中尝试过的东西。问题是hasASolution()返回 true 但solution变量为空。

离开python有一段时间了，所以格式化技能不存在。希望转换这种格式的东西：

变成这样的东西：

然后能够将每个数字作为单独的输入引用，以更改为 T 或 F。任何指导都将不胜感激。

我试图从http://amit.metodi.me/research/bee/编译 bumblebee sat-solver 。我已经安装了 SWI-Prolog 和 MinGW，但是在 cmd 中输入“make-minisat”后，我得到：

看起来 g++ 无法访问 prolog 头文件。有任何想法吗？我在win 10、64位上工作。

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

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

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

谢谢。

编辑

我在 Verilog 中有一个示例组合循环，我可以按照说明进行逻辑综合并生成 blif 文件。

但是，我需要的是从电路中生成 CNF 公式。ABC 等工具仅允许从组合斜接生成（即，具有 1 个输出）。

我尝试了 yosys 指令“sat -dump_cnf FILE”，确实可以生成 CNF 文件。但是，我不确定如何将 CNF 中的变量与电路中的 I/O 映射。

有没有人研究过 Yosys 的“sat -dump_cnf”功能并可以给我一个指针？

I'm looking at doing some verification work where I've got regular tree grammars as an underlying theory.

Z3 lets you define your own stuff with uninterpreted functions, but that doesn't tend to work well any time your decision procedures are recursive. They used to allow for plugins but that has been depricated, I think.

I'm wondering, does anybody have a recommendation of a decent SMT solver that allows you to write decision procedures for custom theories?

我正在尝试从这个 git repo - https://github.com/fbacchus/MaxHS设置 MaxHS SAT 求解器。

我收到一条错误消息，显示“/usr/bin/ld: 找不到 -lcplex”。谁能指导我什么是 lcplex 库以及如何解决这个问题？我的控制台看起来像这样..

当使用 MiniSat 作为 C++ 库时，每个新变量都可以创建为决策变量或非决策变量。

我对此的粗略理解是，当求解器决定在分支过程中接下来使用哪个变量时，不考虑非决策变量。但是，在我的项目中，当非决策变量位于蕴涵左侧而不是等价关系时，我遇到了麻烦，因为求解器返回 SAT，即使公式实际上是 UNSAT。

进一步的实验表明，这只发生在非决策变量位于超过 2 个变量的公式中时（我猜 2 变量公式路径是求解器中的一种特殊情况，因此它的行为不同）。

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