1812.
Lost Logic
时间限制 1000 ms
内存限制 512 MB
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 , ..., x_n$ that can take on values `0` (false) and `1` (true). A constraint is a formula of the form $a → b$ where both $a$ and $b$ are possibly negated variables. As usual, $→$ denotes logical implication: $a → 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.
输入数据
输出数据
If there is no solution output a single line containing the integer $-1$.
Otherwise, the first line should contain an integer $m$ where $1 ≤ m ≤ 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 "$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 "!" character.
- A constraint is a string of the form $a -> 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.
样例输入
复制
3
0 0 0
0 1 0
1 0 0 \n
· · \n
· · \n
· · \n
样例输出
special judge
复制
3
x1 -> !x2
x3 -> x1
x3 -> x2 \n
· · \n
· · \n
· · \n