constraint-programming - Minisat 中的 Unsat 核心

Question

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

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

Answer 1

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

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

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