[CERC2016] Lost Logic

题意翻译

给定 $3$ 组随机布尔变量 $v_{i,1},...,v_{i,n}(1\leq i\leq 3)$,每组均为 $n$ 个。你需要构造关于布尔变量 $x_1,...,x_n$ 的若干组**条件**,使得满足全部条件的布尔变量赋值**有且仅有** $(v_{i,1},...,v_{i,n})(1\leq i\leq 3)$ 这 $3$ 组。 由于机器限制,你所构造每组条件的形式均应为:$A\rightarrow B$。这组条件的限制了:当 $A$ 为 $1$ 时 $B$ 一定为 $1$。其中,$A,B$ 可能形如: - $x_i$:表示第 $i$ 个变量的值。 - $!x_i$:表示第 $i$ 个变量取反后的值。 例如,如果你构造了 $x_1\rightarrow x_2$,那么表示你规定 $x_1=1$ 时必有 $x_2=1$;如果你构造了 $!x_1\rightarrow x_2$,那么你规定了 $x_1=0$ 时必有 $x_2=1$。你需要找到一种使用不超过 $500$ 组条件来满足题意的方法,或者判定这样的条件组合不可能存在。如果有多组解,输出任意一组均可。 数据保证 $2\leq n\leq 50,v_{i,j}\in\{0,1\}(1\leq i\leq 3,1\leq j\leq n)$。

题目描述

Gustav is reading about *2-satisfiability*, a well known problem of assigning truth values to boolean variables in order to satisfy a list of *constraints* — simple logical formulas involving two variables each. We are using $n$ variables $x_1, x_2, \cdots , x_n$ that can take on values $0$ (false) and $1$ (true). A constraint is a formula of the form $a\to b$ where both $a$ and $b$ are possibly negated variables. As usual, $\to$ denotes logical implication: $a \to b$ is $0$ only when $a$ is $1$ and $b$ is $0$. The negation of variable $a$ is denoted by $!a$. Given an assignment of values to variables, we say that the constraint is *satisfied* if it evaluates to $1$. Gustav has constructed a list of constraints and correctly concluded that there are *exactly three* different assignments of values to variables that satisfy all the constraints. Gustav has wrote down all three assignments but has, unfortunately, lost the list of constraints. Given three assignments of $n$ values to variables, find any list consisting of at most $500$ constrains such that the three given assignments are the *only* assignments that satisfy all the constraints.

输入输出格式

输入格式


The first line contains an integer $n (2 \leq n \leq 50)$ — the number of variables. Three lines follow, each describing one assignment. The $k$-th line contains $n$ space-separated integers $v_1^k,v_2^k,\cdots,v_n^k$, where each $v_i^k$ is either $0$ or $1$ and denotes the value of the variable $x_i$ in the $k$-th assignment. All three assignments will be different.

输出格式


If there is no solution output a single line containing the integer $−1$. Otherwise, the first line should contain an integer $m$ where $1 \leq m \leq 500$ — the number of constraints in your solution. The $k$-th of the following $m$ lines should contain the $k$-th constraint. Each constraint should be a string constructed according to the following rules: - A *variable* is a string of the form “$\texttt{x}i$” where $i$ is an integer between $1$ and $n$ inclusive written without leading zeros. - A *literal* is a string consisting of a variable possibly preceded by the “$\texttt{!}$” character. - A *constraint* is a string of the form “$a\texttt{ -> }b$” where both $a$ and $b$ are literals. The implication sign consists of the “minus” character and the “greater-than” character and there is a single space character both before and after the implication sign.

输入输出样例

输入样例 #1

3
0 0 0
0 1 0
1 0 0

输出样例 #1

3
x1 -> !x2
x3 -> x1
x3 -> x2

输入样例 #2

4
0 0 1 0
1 0 0 0
1 0 1 1

输出样例 #2

-1