Problem F
3SAT
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 |