SAT Solver: SAT4J - evaluating only a subset of clauses

Question

I have a formula in a .dimacs/.cnf file as in the following:

  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

Is it possible to extract only those clauses that contain e.g., the variables 2, 3, and 4, in SAT4j ? Then, I need to check the consistency only for this new set of clauses, i.e., for:

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

I tried to use Assumptions, I tried to use Constraints, but I still cannot find a way to do this.

Thank you for any suggestion.

Edit

I thought that there is a method like solver.addClause(clause), but in reverse solver.getClause(clause)...Although, I am feeding the solver with clauses from a .cnf file.

Edit 2

First, assumptions have the same syntax with a clause,

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

but the variables are conjunctions in assumptions and disjunctions in a clause. This is a difference. Right? My test examples are saying so. (I just needed to get an extra approval on this).

Second, my issue with using the selector variables is this one:

A simple formula a V b has three models:

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

When I add a selector variable, e.g., s, and its assumption is -s, then I have the same number of models, i.e., 3 models:

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

When the assumption is true, i.e., s, then I have 4 models instead of 0 that I want:

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

Of course when s = T, then (s V a V b) = (T V a V b) = T, but is this a deletion way for the clause (a V b)? What I need are the number of models, real models! Is there a way to find the exact models while 'removing' somehow these variables (i.e., a and b) that we want to exclude by an assumption?

For this case, this is my current code in 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)
}

Thank you, for any help.

Answer 1

I would like to add another way. Using a blocking clause.

You can count models by enumerating different solutions and obtaining the exact models. You would then negate one solution, conjunct it with the rest of the formula and solve again. This negated solution clause is called a blocking clause. It will not let the solver pick the same solution again.

Now, in your case, you should add a blocking clause that is in terms of only the variables you want.

Suppose you have the CNF formula

x and (y or z)

and you get the solution x = 1, y = 1, z = 0.

But, say, you are interested in x and z only.

From this solution, the blocking clause would be

!(x and !z)

This will disallow the solution

x = 1, y = 1, z = 0, and also x = 1, y = 0, z = 0

You will get only one solution

x = 1, z = 1 (y does not matter)

Hope this helps.

If you are using some model counter, look for the option to add projection variables (sometimes also called independent variables). You basically want to project all solutions on to a subset of variables. The different combinations of the other variables should not affect the number of models.

Answer 2

The way to proceed is to prefix each clause with a new selector variable

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

And then you just need to assign the extra variable to true to discard a clause and to false to enable it, as assumptions. In your case, the assumption would be 7,-8,-9,10,11,-12,-13,14,-15.

This is not specific to Sat4j, it is a way to proceed proposed originally by minisat, and that most SAT solver provide.

edit 2:

Here is the way to use assumptions and model counting

    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;
}