#P9798. Fully Quantified Boolean 2-CNF Evaluation

    ID: 22944 Type: Default 1000ms 256MiB

Fully Quantified Boolean 2-CNF Evaluation

Fully Quantified Boolean 2-CNF Evaluation

We define a fully quantified Boolean 2-CNF formula in the following form:

$Q_1 x_1 \; Q_2 x_2 \; \ldots \; Q_n x_n \; F(x_1, x_2, \ldots, x_n)$,

where for each i, $Q_i$ is either the universal quantifier $\forall$ or the existential quantifier $\exists$. The formula F is in 2-CNF, i.e. a conjunction (AND, $\land$) of m clauses and each clause is a disjunction (OR, $\lor$) of two expressions. Each clause is of the form:

$s \lor t$,

where each of s and t is either a literal of a variable (optionally with a negation) or the constant false (represented by 0). In particular, if a literal is a positive integer i, it represents the variable $x_i$; if it is a negative integer -i, it represents the negation $\lnot x_i$; and if it is 0, it represents the constant false.

The formula is fully quantified (i.e. there are no free variables) so the answer is simply either true or false. To compute the value of the formula, we use the following recursive algorithm:

  1. If there are no quantifiers left, evaluate the remaining 2-CNF formula F (i.e. check if every clause evaluates to true).
  2. Otherwise, let the current quantifier be on variable $x_i$. Recursively compute the formula value for both assignments $x_i=0$ and $x_i=1$ (denoted by $F_0$ and $F_1$, respectively), and then:
    • If $Q_i = \exists$, return $F_0 \lor F_1$.
    • If $Q_i = \forall$, return $F_0 \land F_1$.

Your task is to implement this recursive evaluation. The input is given as follows:

inputFormat

The input begins with a line containing two integers n and m, where n is the number of variables and m is the number of clauses.

The second line contains n characters (separated by spaces) each representing the quantifier for a variable. Use A to denote the universal quantifier ($\forall$) and E for the existential quantifier ($\exists$).

Each of the following m lines contains two integers representing a clause. Each integer can be:

  • A positive integer i, representing the literal $x_i$.
  • A negative integer -i, representing the literal $\lnot x_i$.
  • 0, representing the constant false.

outputFormat

Output a single line: true if the formula evaluates to true, or false otherwise.

sample

1 1
E
1 0
true