Hide

# Problem E3SAT

Given as input a description of a 3SAT sentence, determine whether it is satisfiable 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

$(a \vee b \vee b) \wedge (\neg {a} \vee \neg {b} \vee \neg {b}) \wedge (a \vee \neg {b} \vee \neg {b})$

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

\begin{align*} (x \vee y \vee z) \wedge (x \vee y \vee \neg {z}) \wedge (x \vee \neg {y} \vee z) \wedge (x \vee \neg {y} \vee \neg {z}) \wedge (\neg {x} \vee y \vee z) \\ \wedge ~ (\neg {x} \vee y \vee \neg {z}) \wedge (\neg {x} \vee \neg {y} \vee z) \wedge (\neg {x} \vee \neg {y} \vee \neg {z}) \end{align*}

is not satisfiable.

## Input

The first line of input contains an integer $1 \le n \le 100$. 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 is a lowercase letter in the range $a$ to $z$.

## Output

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

Sample Input 1 Sample Output 1
3
a b b
!a !b !b
a !b !b

yes

Sample Input 2 Sample Output 2
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

CPU Time limit 5 seconds
Memory limit 1024 MB
Statistics Show