#P9798. [NERC 2018] Harder Satisfiability

[NERC 2018] Harder Satisfiability

背景

翻译自 NERC 2018 H 题。

题目描述

我们定义一个“完全量化的布尔类型的 2-CNF 公式”(下简称 2-CNF)是以 Q1x1…QnxnF(x1,…xn)Q_1 x_1 \ldots Q_n x_n F(x_1,\ldots x_n) 构成的,QiQ_i 只有两种,一种是“通用量词” ∀\forall,另一种是“存在量词” ∃\exists。然后 FF 是一个 mm 子句的 s∨ts \lor t(OR\mathtt{OR} 运算) 的连词(AND\mathtt{AND} 运算),其中 ss 和 tt 不一定不同且不一定是否定(为 false\texttt{false})。由于 2-CNF 公式是给定的,所以并没有自由变量(即答案固定为 true\texttt{true} 或 false\texttt{false})。

至于计算 2-CNF 公式的值,我们可以使用一个简单的递归算法来求:

  • 如果没有量词(即 ∀\forall 或 ∃\exists ),则返回剩余表达式的返回值。

  • 否则,我们使用递归计算公式:Fz=Q2x2…QnxnF(z,x2,…,xn)F_z = Q_2x_2 \ldots Q_nx_n F(z,x_2,\ldots,x_n),此处 z=0,1z = 0,1。

  • 如果当前符号为 ∃\exists,则返回 F0∨F1F_0 \lor F_1(OR\mathtt{OR} 运算)。否则符号为 ∀\forall 返回 F0∧F1F_0 \land F_1。

输入格式

第一行是一个整数 t(1≤t≤105)t (1 \leq t \leq 10^5),表示数据组数。

接下来 tt 组数据,每组数据第一行两个整数 n(1≤n≤105)n(1 \leq n \leq 10^5) 和 m(1≤m≤105)m (1 \leq m \leq 10^5),nn 表示量词的长度,mm 表示在 FF 中的元素个数。

然后一行,一串长度为 nn 的字符串 ss,如果 si=s_i = A,则 Qi=∀Q_i = \forall,否则若 si=s_i = E,则 Qi=∃Q_i = \exists。

接下来 mm 行,一行两个整数 ui,vi(−n≤ui,vi≤n)u_i,v_i(-n \leq u_i,v_i \leq n),如果 ui≥1u_i \geq 1 则第 ii 个变量是 xuix_{u_i},如果 ui≤−1u_i \leq -1 则第 ii 个变量是 −(x−ui)-(x_{-u_i}),viv_i 同理。

输出格式

对于每组数据,如果 2-CNF 公式为真输出 TRUE,否则输出 FALSE。

3
2 2
AE
1 -2
-1 2
2 2
EA
1 -2
-1 2
3 2
AEA
1 -2
-1 -3

TRUE
FALSE
FALSE

提示

数据保证 1≤t≤1051 \leq t \leq 10^5,1≤n,m≤1051 \leq n,m \leq 10^5,−n≤ui,vi≤n-n \leq u_i,v_i \leq n。

第一个 2-CNF 公式可以化简为 $\forall x_1 \exists x_2(x_1 \lor \overline{x_2}) \land (\overline{x_1} \lor x_2) = \forall x_1 \exists x_2 x_1 \oplus x_2$,对于任意的 x1x_1 都存在 x2=x1‾x_2 = \overline{x_1} 使得答案为真。

第二个 2-CNF 改变了公式的顺序,对于任意的 x1x_1,都可以选择 x2=x1x_2 = x_1,使得表达式为 FALSE。

第三个表达式是 $\forall x_1 \exists x_2 \forall x_3 (x_1 \lor \overline{x_2}) \land (\overline{x_1} \lor \overline{x_3})$,如果令 x1=1x_1 = 1,x3=1x_3 = 1,则没有 x2x_2 的值可以使得句子赋值为真,所以公式为假。