Solver: SAT4J -只计算一组子句

Question

我在..dimacs/..cnf文件中有一个公式，如下所示：

  p cnf 6 9
  1 0
 -2 1 0
 -1 2 0
 -5 1 0
 -6 1 0
 -3 2 0
 -4 2 0
 -3 -4 0
  3 4 -2 0

是否可以仅提取中包含变量2、3和4的子句(如SAT4j中的变量2、3和4)？然后，我只需要检查这组新子句的一致性，即：

  p cnf 4 6
 -2 1 0
 -1 2 0
 -3 2 0
 -4 2 0
 -3 -4 0
  3 4 -2 0

我试着使用假设，我尝试使用约束，但我仍然找不到一种方法来做到这一点。

谢谢你的建议。

编辑

我认为有一个类似于solver.addClause(clause)的方法，但是在反向solver.getClause(clause)...Although中，我用来自.cnf文件的子句来给求解器提供信息。

编辑2

首先，假设与子句具有相同的语法，

val assumption: IVecInt = new VecInt(Array(1, 2))
val clause: IVecInt = new VecInt(Array(1, 2))

但是变量在假设中是conjunctions，在子句中是disjunctions。这是不同的。对吗？我的测试例子就是这么说的。(我只是需要得到额外的批准)。

其次，我使用选择器变量的问题是：

一个简单的公式a V b有三个模型：

(a, b), 
(a, -b), 
(-a, b)

当我添加一个选择器变量，例如s，假设它是-s时，那么我有相同数量的模型，即3个模型：

(a, b, -s),
(a, -b, -s),
(-a, b, -s)

假设是true，即s，那么我有4个模型，而不是我想要的0：

(a, b, s), 
(a, -b, s), 
(-a, b, s), 
(-a, -b, s)

当然，当s = T，然后(s V a V b) = (T V a V b) = T，但是这是一种删除方式的子句(a V b)？我需要的是数量的模型，真正的模型！是否有一种方法可以在“删除”这些变量(即a和b)的同时找到精确的模型，这些变量是我们想要通过假设排除的？

在本例中，这是我在Scala中的当前代码：

object Example_01 {

  val solver: ISolver = new ModelIterator(SolverFactory.newDefault())
  val reader: DimacsReader = new DimacsReader(solver)
  val problem: IProblem = reader.parseInstance("example_01.cnf")    

  def main(args: Array[String]): Unit = {

    var nrModels: Int = 0
    val assumptions: IVecInt = new VecInt(Array(10))

    try {
      while(solver.isSatisfiable(assumptions)) {
        println(reader.decode(problem.model()))
        nrModels += 1
      }
    } catch {
      case e: ContradictionException => println("UnSAT: ", e)
    }

    println("The number of models is: " + nrModels)
}

谢谢你的帮助。

Answer 1

我想补充另一种方式。使用阻塞子句。

您可以通过枚举不同的解决方案并获得精确的模型来计算模型。然后，你将否定一个解，将它与公式的其余部分结合起来，然后再求解。这个被否定的解决方案子句称为阻塞子句。它不会让求解者再次选择相同的解决方案。

现在，在您的例子中，您应该添加一个阻塞子句，它只针对您想要的变量。

假设你有CNF公式

x and (y or z)

得到解x= 1，y= 1，z= 0。

但是，比如说，您只对x和z感兴趣。

从这个解决方案中，阻塞子句将是

!(x and !z)

这将不允许解决方案。

x = 1, y = 1, z = 0和x = 1, y = 0, z = 0

你只能得到一个解决方案

x = 1, z = 1 (y不重要)

希望这能有所帮助。

如果您正在使用某些模型计数器，请查找添加投影变量(有时也称为独立变量)的选项。基本上，您希望将所有解决方案投影到变量的子集上。其他变量的不同组合不应影响模型的数量。