#Lutece3388. 简单可满足性问题
简单可满足性问题
Description
布尔可满足性问题(SAT)问题的定义如下:
有 个变量 ,每个变量可以取值 0(假)或 1(真),每个变量有正文字 与负文字 两种形式。其中正文字 的值与变量相同,负文字 的值与变量相反。
一个子句为若干个文字相析取,即 $C_i=x_{a_{i,1}}\vee \dots \vee x_{a_{i,p}}\vee \bar{x}_{b_{i,1}}\vee \dots \vee \bar{x}_{b_{i,q}},1\leq a_{i,j},b_{i,k} \leq n$。这些文字中有任意一个文字的取值为 1,则该子句的值为 1;反之若所有文字的取值都为 0,则该子句的值为 0。
一个合取范式(CNF)为 个子句 相合取,即 。若所有子句的取值为 1,则该 CNF 的值为 1;反之若任意一个子句的取值为 0,则该 CNF 的值为 0。
SAT 问题即给出一个 CNF,问存不存在一种对变量的赋值,使该 CNF 的值为 1。
Bob Wang 知道要找到一组让所有子句都为真的变量赋值是一件很困难的事情,因此对于给出的 CNF ,Bob Wang 只需要找出一种变量赋值,使得至少 个子句的赋值为 1。可以证明满足要求的赋值一定存在。
Input
第一行两个整数 (),表示变量个数以及子句个数。
接下来 组数据,描述子句。
对于第 个子句,第一行一个整数 (),表示文字的数量。接下来 行,每行两个整数 ,描述该子句包含的文字。其中 表示变量编号, 表示正文字 , 表示负文字 。
保证 。
Output
一行 个整数,表示变量的赋值。其中 表示第 个变量赋值为 1, 表示第 个变量赋值为 0。输出使至少 个子句的赋值为 1 的任意一组赋值即可。
Samples
4 5
1
1 1
1
2 1
1
3 0
1
4 1
2
1 1
3 1
0 1 0 1
Note
样例表示的子句为 ,,,,,容易证明 是符合题意的一组赋值。
Resources
The 23rd UESTC Programming Contest Preliminary