Understanding basic examples.

[arey0pushpa]

Hi, I'm trying to create basic one level quantifier alternation and test all 4 possible cases. I have picked your first example as a basis.

 #include <string.h>
 #include <stdlib.h>  
 #include <stdio.h> 
 #include <assert.h>
 #include "../qdpll.h"

 int main (int argc, char** argv)
 {
      QDPLL *depqbf = qdpll_create ();
      qdpll_configure (depqbf, "--dep-man=simple");
      qdpll_configure (depqbf, "--incremental-use");

      qdpll_new_scope_at_nesting (depqbf, QDPLL_QTYPE_FORALL, 1);
      qdpll_add (depqbf, 1);
      qdpll_add (depqbf, 0);

      qdpll_new_scope_at_nesting (depqbf, QDPLL_QTYPE_EXISTS, 2);
      qdpll_add (depqbf, 2);
      qdpll_add (depqbf, 0);

      /* Add clause: 1 -2 0 */
      qdpll_add (depqbf, 1);
      qdpll_add (depqbf, -2);
      qdpll_add (depqbf, 0);

     /* Add clause: -1 2 0 */
      qdpll_add (depqbf, -1);
      qdpll_add (depqbf, 2);
      qdpll_add (depqbf, 0);

      qdpll_print (depqbf, stdout);

  unsigned int i = 0;
  QDPLLResult res;
  while ((res = qdpll_sat (depqbf)) == QDPLL_RESULT_SAT)
  {
      i++;
      if (i > 5) 
    break;
      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);
 
    // Block the previous result.
      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);
 }

The formula is : Forall [x, Exists [y, (x || !y) && (!x || y) ) ] ]
Cases :

1. Exists x , Exists y
   x = 1, y = 1. x = -1, y = -1.

2. Forall x and Forall y : Unsat.

3. Exists x, Forall y: Unsat. Everything is fine till now.

4. Forall x, Exists y ... The output is not what i except. The solver goes on adding the -1 , 1 assignment. How to get assignments in case of satisfying formula in alternation of quantifiers. because this formula is true for every value in universe of discourse (True, False) for the variable x.

Also,
I can see that the tool simplifies formula. Is that basic "simplify" or does depqbf eliminates quantifer? for example in the case of Exists x, Forall y (case 3) it removes y from the formula. I would like to understand the over-ahead for that.

[lonsing]

Hi,

the generation of assignments as shown in my basic example works only if the leftmost quantifier block is existential. It cannot be used to generate assignments to universal variables, if the formula is satisfiable.

In your example, the leftmost quantifier block is universal. If you want to extract assignments to the variables in the inner (i.e., rightmost) existential block, you need a different approach based on generating proofs and extracting certificates in terms of Skolem functions. This can be done with additional tools:

http://fmv.jku.at/qbfcert/

Regarding the simplification: the solver removes the variable 'Forall y' during parsing if the input formula has the prefix 'Exists x Forall y' to maintain an invariant that is relevant for the data structures. Apart from that, there is no quantifier elimination in DepQBF.

Best regards,
Florian

[arey0pushpa]

Thanks for the clarification. Just one follow up: What if the quantifier is of this type; Exists ( x, Forall (y, Exists (z, prop_fml ) ) ) ? and i'm interested in getting only the assignment value of the variable x? Does tool work in this case? Thanks for the reference.

[lonsing]

Yes, exactly, if the outermost quantifier is existential and the formula is satisfiable, then DepQBF can produce assignments to the outermost variables.