luogu#P9798. [NERC2018] Harder Satisfiability

[NERC2018] Harder Satisfiability

题目背景

翻译自 NERC 2018 H 题。

题目描述

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

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

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

  • 否则,我们使用递归计算公式:Fz=Q2x2QnxnF(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,则返回 F0F1F_0 \lor F_1OR\mathtt{OR} 运算)。否则符号为 \forall 返回 F0F1F_0 \land F_1

输入格式

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

接下来 tt 组数据,每组数据第一行两个整数 n(1n105)n(1 \leq n \leq 10^5)m(1m105)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(nui,vin)u_i,v_i(-n \leq u_i,v_i \leq n),如果 ui1u_i \geq 1 则第 ii 个变量是 xuix_{u_i},如果 ui1u_i \leq -1 则第 ii 个变量是 (xui)-(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

提示

数据保证 1t1051 \leq t \leq 10^51n,m1051 \leq n,m \leq 10^5nui,vin-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=x1x_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 = 1x3=1x_3 = 1,则没有 x2x_2 的值可以使得句子赋值为真,所以公式为假。