Minisat中的不饱和核心

Question

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

我想为解算器的每次调用提取未饱和核心，然后处理未饱和核心。

Answer 1

MiniSat在这一点上是一个相当古老的程序。至少，你应该调查一下最近参加SAT比赛的一位解算者，例如葡萄糖。自2013年以来，竞赛要求SAT求解者发出DRAT证明不合格。运行您选择的任何解算器，并让它将其DRAT证明转储到proof.out中。使用-c选项将proof.oout馈送到DRAT trim实用程序中，这将生成DIMACS格式的UNSAT核心。即

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

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