Problem F
3SAT

Given as input a description of a 3SAT sentence, determine whether it is satisfiable (i.e. evaluates to true) by some assignment of true/false values to the variables appearing in the sentence. A variable $a$ can either appear as a positive literal (e.g. $a$) or a negative literal (e.g. $\neg {a}$). A positive literal is true when its variable is true, and a negative literal is true when its variable is false. For example, the sentence

is satisfiable via the assignment of true to $a$ and false to $b$. However, the sentence

is not satisfiable.

Hints

There are several approaches you can take to solve this problem. Here are a few suggestions:

• If there are $26$ variables, there are $2^{26}$ possible variable settings. A reasonable program, efficiently written, should be able to try all of these within the time bound.

• Most modern programming languages support an integer type with at least $32$ bits, which is more than enough to encode $26$ variables. It is easy to try all $2^n$ variable assignments (where $n$ is the number of variables) by counting from $0$ to $2^n$, and using bit operations masking to extract the variable assignments.

• A more efficient method than trying all possible assignments is to use a bounded recursive search which tries to set a variable at each recursion level. If it finds that the current partial assignment cannot possibly satisfy some clause, then it can stop searching early (not recurse any deeper on that branch), which can save a lot of time.

Input

The first line of input contains an integer $1 \le n \le 10\, 000$, representing the number of clauses. The following $n$ lines each represent a clause containing $3$ space-separated literals. Each literal is either positive or negative. A positive literal is a variable name; a negative literal is an exclamation point followed by a variable name. Each variable name $v$ is a lowercase English letter (a to z).

We say that a clause is “trivially satisfiable” if it has opposing literals, such as $(\neg {x} \vee x \vee y)$ (both $x$ and $\neg {x}$ appear, so the clause is satisfied by any setting of the variables $x$ and $y$). No clause in the input for this problem is trivially satisfiable.

Output

Output ‘yes’ if the given sentence is satisfiable; ‘no’ otherwise.

Scoring

Your program will be tested on a set of test groups, each of which is worth a number of points. Each test group contains several test cases, and to receive the points for a test group your program must solve all of the test cases in that group. The score of your program is the sum of the points received on all of the test groups.

3
a b b
!a !b !b
a !b !b

yes

8
x y z
x y !z
x !y z
x !y !z
!x y z
!x y !z
!x !y z
!x !y !z

no