1
$\begingroup$

Suppose we have following 2-QCNF problem:

$$\forall x_1...\forall x_m\exists y_1...\exists y_k:\varphi(x_1,...,y_k)$$

where $\varphi$ is 2-CNF.

When the formula is false?

Rules that I found:

  1. $\exists y_i:(y_i\rightarrow \overline{y_i})\land(\overline{y_i}\rightarrow y_i).$ Existentially quantified variable and it's negation are strongly connected.
  2. $\exists\{x_i,x_j\}:(x_i\rightarrow x_j)\lor(\overline{x_i}\rightarrow x_j)\lor(x_i\rightarrow \overline{x_j})\lor(\overline{x_i}\rightarrow \overline{x_j}).$ Two (or one and it's negation) totally quantified variables are connected.
  3. $\exists\{x_i,y_j\}:((y_j\rightarrow x_i)\land(\overline{y_j}\rightarrow x_i))\lor((y_j\rightarrow \overline{x_i})\land(\overline{y_j}\rightarrow \overline{x_i})).$ Totally quantified variable is reachable from existentially quantified variable and it's negation.

Is there any other rule to solve 2-QCNF or, maybe, there is better way to solve it?

$\endgroup$
2
$\begingroup$

Aspvall, Plass and Tarjan describe a linear time algorithm determining the truth value of quantified 2CNFs in their paper A linear-time algorithm for testing the truth of certain quantified Boolean formulas. Their algorithm is an extension of the well-known algorithm for solving 2SAT using directed reachability; their initial step is computing the strongly connected components of the implication graph.

$\endgroup$
  • $\begingroup$ I can't understand what their rule 3(ii) means as well I don't see if it equals my 3rd rule. However, now I know that 3 rules is enough. $\endgroup$ – rus9384 Aug 7 '17 at 15:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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