问题标签 [sat-solvers]

我有一个如图所示的网状网络。现在，我正在为这个 sat 网络中的所有边分配值。我想在我的程序中提出，我的分配中没有闭环。例如，左上角最正方形的约束可以写成 -

E0 = 0 or E3 = 0 or E4 = 0 or E7 = 0，因此任何一个链接都必须处于非活动状态才能不形成循环。然而，在这种网络中，存在许多可能的环路。

例如由边缘形成的循环 - E0, E3, E7, E11, E15, E12, E5, E1。

现在我的问题是我必须描述这个网络中可能发生的每个可能的循环组合。我试图在一个可能的公式中编写约束，但是我无法成功。

如果有可能的方法来编码这种情况，任何人都可以抛出任何指针吗？仅供参考，我正在使用 Z3 Sat Solver。

我正在尝试解决仅包含单热约束的 SAT 问题。现在我正在使用 Claessen 在 Sec. 中提出的 one-hot 编码。[1] 的 4.2 和 MiniSAT。

我想知道是否有解决此类问题的更好方法，例如与基于 CNF 的 SAT 求解器相比，一类求解器更适合此类问题。我搜索了一下，但根本找不到关于 SAT 和 one-hot 约束的太多信息。

[1]成功的 SAT 编码技术。马格努斯·比吉尔克。2009 年 7 月 25 日

我正在使用 Z3 来提取无法满足的公式的 unsat-core。我正在使用 Z3@Rise 界面（基于 Web）编写以下代码，

check-sat 正确返回 'unsat' 但 (get-unsat-core) 返回空。我错过了一些配置/选项吗？还是我让这个例子变得复杂了？

我从 Z3 的运行中获得了一些统计数据。我需要明白这些是什么意思。对于 sat 和 SMT 解决方案的最新发展，我相当生疏和不了解最新情况，因此我试图自己寻找解释，但我可能大错特错。所以我的问题主要是：

1) 措施的名称是什么意思？

2）如果错了，你能给我指点以更好地理解他们所指的吗？

其他观察如下，概念上属于上述两个问题。提前致谢！

我的解释如下。

• 锁相环。以下所有指标均参考 DPLL 算法的行话，这是大多数求解器的基础。

  • ：决定
    • 决定数
  • :传播
    • 传播次数（我猜是单位传播）
  • :binary-propagations, :三元传播
    • 一次传播两个和三个文字
  • ：冲突
    • 冲突数

• 解决方案。粗略地说，操作将解释子句作为集合；从分辨率中提取的技术是解决 SAT 的另一种范式。

  • : 包含
  • :subsumption-resolution
    • 以上两者有什么区别？
  • :dyn-subsumption-resolution
    • 应该在这里描述：学习动态包容，Hamadi 等人。

• 其他技术

  • :minimized-lits
    • 没有明确的想法。它可能与从句学习有关吗？
  • :probing-assigned
    • 我猜它计算了“探测”时所做的分配数量，我猜这是某种前瞻技术。
  • :del 子句
    • 删除子句的数量（出于什么原因？冗余？）
  • : elim-literals : elim-clauses : elim-bool-vars : elim-blocked-clauses
    • 消除后的实体数量。这些指标指的是特定的 SAT 求解技术（参见 M.Järvisalo 等人的 Blocked Clause Elimination，以获取参考）
  • :重启
    • 重启次数。

• 其他方面

  • :mk-bool-var : mk-binary-clause : mk-ternary-clause : mk-clause
    • 创建的布尔变量和二元、三元和通用子句的数量。
  • ：记忆
    • 使用的最大内存量。
  • :gc 子句
    • 垃圾回收条款...？
    • 根据我的实验，这种解释是合理的，因为情况总是如此
      • : gc-clause <= : del-clause ; 就我而言，不平等是严格的。
    • 并非总是如此
      • : gc-clause <=: elim-clauses ; 它也可以是：gc-clause > : elim-clauses

链接：
Z3 定理证明者
picosat 与 pyhton 绑定

我使用 Z3 作为 SAT 求解器。对于较大的公式，似乎存在性能问题，这就是为什么我想检查 picosat 看看它是否是一个更快的选择。我现有的 python 代码以 z3 语法生成一个命题公式：

输出/结果

然而，Picosat 使用数字列表/数组，如下例所示（“clauses1”：6 指变量 P，-6 表示“非 P”等）：

您推荐什么作为将表示 CNF 中的公式的 Z3 变量（如代码示例中的变量“f”）转换为上述格式 picosat 用于表示 CNF 中的公式的简单解决方案？我真的尝试使用Z3的python API，但是文档不足以自己解决问题。

（请注意，上面的例子只是说明概念。变量C表示的公式将是动态生成的，并且过于复杂，无法直接被z3高效处理）

我使用 Z3 定理证明器，并且我有一个大公式（114 个变量）。我可以打印一个包含所有子句的大公式吗？正常print str(f)截断输出，最后只打印“...”，而不是所有子句。

我测试过print f.sexpr()，这总是打印所有的条款。但是仅在 sexpr 语法中。

我可以打印公式的所有子句但避免使用 s-expression 语法吗？

注意：代码示例非常小，无法显示问题，但发布大公式会占用太多空间。

简单的问题。我有一个非常大的 CNF 文件，它代表一个 mxn 矩阵。可以说具有相关术语的 >10000 个变量。因此，作为第一步，我想对 CNF 文件进行分区，或者甚至更好地将矩阵拆分为 100 个变量以用于并行求解概念。有没有说明适用什么规则？

感谢所有帮助。

问候阿德里安

假设我有两个要在 SMT 中建模的子句，最好将它们添加为单独的断言，例如

或者像这样使用 and 运算符添加一个断言

这对于 SMT 求解器性能方面的大规模问题是否重要。我正在使用 Z3。

我正在启动一个子进程，该进程应在​​定义的超时期限内按照以下几行结束：

子进程是 CPU 密集型计算引擎（SAT 求解器）。我的主程序是使用Visual Studio 2013和Windows 7 64-bitC#编写和开发的。

大多数情况下，上面的代码可以正常工作，并且完成了适当的进程超时终止。但在某些 5% 的情况下，process.Kill()没有明显的效果。子进程保持活动状态。

我试图以较低的优先级启动子进程。我还试图在杀死它之前暂停它。作为外部工具调用TASKKILL /F也并不总是有帮助。我注意到，并非所有 SAT 求解器都会出现此问题。我有管理权限，但不以管理员身份运行主程序。

我可以做些什么来可靠地终止我的应用程序的子进程？

已编辑：
除了超出其超时预算外，子进程的行为非常正常，可以使用 Process Explorer 手动终止（无需管理员提升）。问题是如何确保超时后没有进程继续运行。

解决方法：
我使用VC++ 2013实现了一个超时工具。我现在没有直接调用子进程，而是调用我的工具，该工具又调用子进程。该工具使用CreateProcess()和TerminateProcess()来启动和停止子进程。可能可以直接从程序调用CreateProcess()和TerminateProcess()C#而不产生额外的进程。
解决方法并不优雅，但确实解决了我的问题。

在 MiniZinc (windows IDE) 我如何解决：flatzinc：错误：FD 求解器后端不支持“var float”类型的变量。我意识到我需要一个不同的求解器，但找不到安装一个程序的过程，并且 Preferences dlg 似乎不起作用。另外，不清楚哪个求解器可以工作。