In the paper "Resolution for Quantified Boolean Formulas", I am unable to understand the proof of theorem 3.4. Please help me with the basic concept used on page 4:

theorem 3.4

The concept that I am referring to is:

Then $\mathit{\Phi}$ is false if and only if there exists a clause $\phi \in N^+_\mathit{\Phi}$ or $\phi \in N_\mathit{\Phi}$ such that $\forall x_1\exists y_1\cdots y_{k-1}\forall x_k(P_\mathit{\Phi} \land \phi)$ is false.

  • 1
    $\begingroup$ That's a badly phrased question. You should try to be more specific about what exactly you find unclear. For starters, which concept are you referring to? $\endgroup$ Jun 15 '14 at 21:26
  • 1
    $\begingroup$ Well, the problem with this question is that in order for anyone to answer it they have to read 15 pages, and for all we know you're just asking for something that was defined on page 3, and you missed it. $\endgroup$ Jun 15 '14 at 21:53
  • 1
    $\begingroup$ I have no problem understanding the definitions, but I don't know why the claim you mention is true. Assuming the claim is true, probably after some effort you will be able to prove it. So are you having problems understanding the concepts/definitions or why the claim is true? $\endgroup$ Jun 16 '14 at 2:21
  • 3
    $\begingroup$ Please try to make the question self contained, not just referring to the paper, but so that one could understand the question without reading the paper. $\endgroup$
    – jmite
    Jun 16 '14 at 3:35
  • 2
    $\begingroup$ If we don't have to read the paper, then it should be possible to make a self-contained question. This will also be a very good verification for you that you understood the definitions correctly -- trying to explain something to another person is often all that is needed. When I am confused about something I grab a colleague and make him listen, usually I end up explaining the confusion to myself. $\endgroup$ Jun 16 '14 at 6:52

An unquantified CNF formula consisting of clauses containing a single positive literal plus any number of negated literals is always satisfiable. To produce a satisfying assignment, you simply set all the positive literals to true, satisfying all the clauses. If you existentially quantify the variables associated with the positive literals and allow arbitrary quantification of the remaining variables, the formula is still satisfiable, and for the same reason. In the proof of the theorem, $P_\mathit{\Phi}$ is the subset of such clauses from the Horn formula $\mathit{\Phi}$. Thus $P_\mathit{\Phi}$ by itself is always satisfiable. It follows that $\mathit{\Phi}$ can only be unsatisfiable if, out of the sets of remaining clauses (denoted $N^+_\mathit{\Phi}$ and $N_\mathit{\Phi}$), a clause requires one of the previously set positive literals in $P_\mathit{\Phi}$ to be set false and there is no other way to satisfy the previously satisfied clause.


Not the answer you're looking for? Browse other questions tagged or ask your own question.