Minisat 中的 Unsat 核心答案

【问题标题】：Unsat core in MinisatMinisat 中的 Unsat 核心
【发布时间】：2020-03-16 06:26:25
【问题描述】：

minisat 中是否有任何 API 调用来提取 unsat 核心或任何其他方法。

我想为求解器的每次调用提取 unsat 核心，然后处理 unsat 核心。

【问题讨论】：

查看迷你卫星analyzeFinal。但在投入大量工作之前（理解它，包括必要的假设），我建议在原型设计期间首先查看pysat。作为替代包装器或用于分析它们如何使用analyzeFinal（可能由于大量安装补丁而被混淆）
不幸的是，我只能使用 minisat。但是到目前为止我所做的是我用一个额外的变量标记了每个子句！lbl（负极性）并且在解决和假设时我假设 lbl（正极性）.. 所以 minisat 有这个向量称为冲突..其中包含未饱和核心中的所有 lbl 子句！

标签： constraint-programming sat sat-solvers

【解决方案1】：

MiniSat 在这一点上是一个相当古老的程序。至少，您应该查看输入 recent SAT competition 的求解器之一，例如Glucose。自 2013 年以来，竞赛要求 SAT 求解器发出 DRAT proofs 的不可满足性。运行您选择的任何求解器，并将其 DRAT 证明转储到proof.out。使用 -c 选项将 proof.out 输入到 drat-trim 实用程序中，这将生成 DIMACS 格式的 UNSAT 核心。即

drat-trim originalproblem.cnf proof.out -c core.cnf

请注意，您不必使用 MiniSat 克隆；任何发出 DRAT 证明的现代求解器都可以将其证明输入 drat-trim 以产生 UNSAT 核心。

【讨论】：

一定会调查的。不幸的是，我只能使用 minisat。但是到目前为止我所做的是我用一个额外的变量标记每个子句！lbl（负极性）并且在解决假设时我假设 lbl（正极性）.. 所以 minisat 有这个向量称为冲突..具有未饱和核心中的所有 lbl 子句！