0

我在 .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

是否可以在 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

我尝试使用 Assumptions，我尝试使用 Constraints，但我仍然找不到这样做的方法。

谢谢你的任何建议。

编辑

我认为有一种类似的方法solver.addClause(clause)，但反过来solver.getClause(clause)......虽然，我正在为求解器提供 .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)
}

感谢您的任何帮助。

4

2 回答 2

2

我想添加另一种方式。使用阻塞子句。

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

现在，在您的情况下，您应该添加一个仅针对您想要的变量的阻塞子句。

假设你有 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没关系）

希望这可以帮助。

如果您使用一些模型计数器，请寻找添加投影变量（有时也称为自变量）的选项。您基本上希望将所有解决方案投影到变量子集上。其他变量的不同组合不应影响模型的数量。

于 2017-06-14T04:23:28.930 回答
0

继续的方法是在每个子句前面加上一个新的选择器变量

p cnf 15 9
7 1 0
8 -2 1 0
9 -1 2 0
10 -5 1 0
11 -6 1 0
12 -3 2 0
13 -4 2 0
14 -3 -4 0
15 3 4 -2 0

然后，您只需将额外变量分配给 true 以丢弃子句，并将其分配给 false 以启用它，作为假设。在您的情况下，假设为 7,-8,-9,10,11,-12,-13,14,-15。

这不是 Sat4j 特有的，它是 minisat 最初提出的一种继续方式，并且大多数 SAT 求解器都提供。

编辑2：

这是使用假设和模型计数的方法

    ISolver solver = SolverFactory.newDefault();
    ModelIterator iterator = new ModelIterator(solver);
    iterator.newVar(2); // for a and b
    int selector = iterator.nextFreeVarId(true);
    assert selector == 3;
    IVecInt clause = new VecInt();
    // (a, b),
    clause.push(1).push(2);
    solver.addClause(clause);
    clause.clear();
    // (s, -a, -b)
    clause.push(-1).push(-2).push(3);
    solver.addClause(clause);
    clause.clear();
    IVecInt assumptions = new VecInt();
    // we activate the second clause in the solver
    assumptions.push(-3);
    while (iterator.isSatisfiable(assumptions)) {
        System.out.println("1:>" +new VecInt(iterator.model()));
    }
    assert iterator.numberOfModelsFoundSoFar() == 2;
    // need to reset the solver, since iterating over the model
    // adds new constraints in the solver
    iterator.reset();
    clause = new VecInt();
    // (a, b),
    clause.push(1).push(2);
    solver.addClause(clause);
    clause.clear();
    // (s, -a, -b)
    clause.push(-1).push(-2).push(3);
    solver.addClause(clause);
    clause.clear();
    // we disable the second clause in the solver
    assumptions.clear();
    assumptions.push(3);
    while (iterator.isSatisfiable(assumptions)) {
        System.out.println("2:>" + new VecInt(iterator.model()));
    }
    assert iterator.numberOfModelsFoundSoFar() == 3;
}
于 2017-01-25T13:23:03.890 回答