Question about all the possible outputs.

[virtualliu]

Hi.
I am new to the satisfiability problem. I found DepQBF is a great thing to help me, but I noticed that option "--qdo" will show only one output of the QBF, so could you please tell me whether there is a way to show all the outputs?
Thanks a lot.

[lonsing]

Hi!

Thank you very much for your kind feedback!

Below, I have attached a C program which enumerates all the possible values of the outermost (i.e., leftmost) existential variables in a simple example formula.

Compilation works as usual, e.g.:
gcc -o example example.c -L.. -lqdpll
assuming that the library file 'libqdpll.a' and header file 'qdpll.h' are in the parent directory.

The idea is to solve the formula, extract the values, and then add a new clause (a so-called 'blocking clause') which prevents the solver from finding the same values again. To this end, the values are negated. This process continues until the formula becomes unsatisfiable.

This approach can be generalized to arbitrary formulas.

Best regards,
Florian

C code of example starts below:

#include <stdio.h>
#include "../qdpll.h"

int main (int argc, char** argv)
{
  QDPLL *depqbf = qdpll_create ();
  /* Configure for incremental use and output generation. */
  qdpll_configure (depqbf, "--dep-man=simple");
  qdpll_configure (depqbf, "--incremental-use");
  qdpll_configure (depqbf, "--qdo");

  /* Add the following formula:
     p cnf 10 4
     e 1 2 0
     a 10 0
     e 3 0
     1 2 -10 -3 0
     1 2 10 3 0
     -1 -2 -10 3 0
     -1 -2 10 -3 0
  */

  /* Add prefix. */
  qdpll_new_scope (depqbf, QDPLL_QTYPE_EXISTS);
  qdpll_add (depqbf, 1);
  qdpll_add (depqbf, 2);
  qdpll_add (depqbf, 0);
  qdpll_new_scope (depqbf, QDPLL_QTYPE_FORALL);
  qdpll_add (depqbf, 10);
  qdpll_add (depqbf, 0);
  qdpll_new_scope (depqbf, QDPLL_QTYPE_EXISTS);
  qdpll_add (depqbf, 3);
  qdpll_add (depqbf, 0);

  /* Add clauses. */
  qdpll_add (depqbf, 1);
  qdpll_add (depqbf, 2);
  qdpll_add (depqbf, -10);
  qdpll_add (depqbf, -3);
  qdpll_add (depqbf, 0);

  qdpll_add (depqbf, 1);
  qdpll_add (depqbf, 2);
  qdpll_add (depqbf, 10);
  qdpll_add (depqbf, 3);
  qdpll_add (depqbf, 0);

  qdpll_add (depqbf, -1);
  qdpll_add (depqbf, -2);
  qdpll_add (depqbf, -10);
  qdpll_add (depqbf, 3);
  qdpll_add (depqbf, 0);

  qdpll_add (depqbf, -1);
  qdpll_add (depqbf, -2);
  qdpll_add (depqbf, 10);
  qdpll_add (depqbf, -3);
  qdpll_add (depqbf, 0);

  fprintf (stderr, "Input formula:\n");
  qdpll_print (depqbf, stderr);

  /* In the following loop, we enumerate all possible values for the outermost
     existential variables '1' and '2'. */

  unsigned int i = 0;
  QDPLLResult res;
  while ((res = qdpll_sat (depqbf)) == QDPLL_RESULT_SAT)
    {
      i++;
      fprintf (stderr, "\nResult after iteration %u: %u\n", i, res);
      /* Get current values for variables '1' and '2'. */
      QDPLLAssignment val1 = qdpll_get_value (depqbf, 1);
      QDPLLAssignment val2 = qdpll_get_value (depqbf, 2);
      fprintf (stderr, "Value of 1: %d\n", val1);
      fprintf (stderr, "Value of 2: %d\n", val2);
      /* Add a new clause to block previous assignments to outermost
         existential variables. NOTE: must reset the solver first. */
      qdpll_reset (depqbf);
      fprintf (stderr, "Adding a new blocking clause.\n");
      if (val1 != QDPLL_ASSIGNMENT_UNDEF)
        qdpll_add (depqbf, val1 == QDPLL_ASSIGNMENT_FALSE ? 1 : -1);
      if (val1 != QDPLL_ASSIGNMENT_UNDEF)
        qdpll_add (depqbf, val2 == QDPLL_ASSIGNMENT_FALSE ? 2 : -2);
      qdpll_add (depqbf, 0);
      fprintf (stderr, "Formula with blocking clause:\n");
      qdpll_print (depqbf, stderr);
    }

  qdpll_delete (depqbf);

  return 0;
}

This is the output generated by the above program (note the blocking clauses that are appended to the formula in each iteration of the loop):

Input formula:
p cnf 10 4
e 1 2 0
a 10 0
e 3 0
1 2 -10 -3 0
1 2 10 3 0
-1 -2 -10 3 0
-1 -2 10 -3 0

Result after iteration 1: 10
Value of 1: 1
Value of 2: 1
Adding a new blocking clause.
Formula with blocking clause:
p cnf 10 5
e 1 2 0
a 10 0
e 3 0
1 2 -10 -3 0
1 2 10 3 0
-1 -2 -10 3 0
-1 -2 10 -3 0
-1 -2 0

Result after iteration 2: 10
Value of 1: 1
Value of 2: -1
Adding a new blocking clause.
Formula with blocking clause:
p cnf 10 6
e 1 2 0
a 10 0
e 3 0
1 2 -10 -3 0
1 2 10 3 0
-1 -2 -10 3 0
-1 -2 10 -3 0
-1 -2 0
-1 2 0

Result after iteration 3: 10
Value of 1: -1
Value of 2: 1
Adding a new blocking clause.
Formula with blocking clause:
p cnf 10 7
e 1 2 0
a 10 0
e 3 0
1 2 -10 -3 0
1 2 10 3 0
-1 -2 -10 3 0
-1 -2 10 -3 0
-1 -2 0
-1 2 0
1 -2 0

Result after iteration 4: 10
Value of 1: -1
Value of 2: -1
Adding a new blocking clause.
Formula with blocking clause:
p cnf 10 8
e 1 2 0
a 10 0
e 3 0
1 2 -10 -3 0
1 2 10 3 0
-1 -2 -10 3 0
-1 -2 10 -3 0
-1 -2 0
-1 2 0
1 -2 0
1 2 0

[virtualliu]

Hi,

Thank you for the reply! It really helps me a lot!

I really appreciate it!

Regards,
Liu