k-SAT:satisfiability of k-CNF formula n variables x1,...xE0,1) m clauses,each being OR of k literals Literal:Xi or x 口e.g.(k=3):（x1)vX5vX7 3-CNF formula:AND of these m clauses 口e.g.(口x1)vx5YX)(2v(xs)Y(x7)(X1v7Y8) 3-SAT Problem:Given a 3CNF formula,decide whether there is an assignment ofvariables s.t.the formula evaluates to 1. For the above example,Yes:X5=1,X7=0,x1=1k-SAT: satisfiability of k-CNF formula ◼ n variables x1 , …, xn∊{0,1} ◼ m clauses, each being OR of k literals ❑ Literal: xi or ¬xi ❑ e.g. (k=3): (¬x1 ) ٧ x5 ٧ x7 ◼ 3-CNF formula: AND of these m clauses ❑ e.g. ((¬x1 ) ٧ x5 ٧ x7 ) ٨ (x2 ٧ (¬x5 ) ٧ (¬x7 )) ٨ (x1 ٧ x7 ٧ x8 ) ◼ 3-SAT Problem: Given a 3CNF formula, decide whether there is an assignment of variables s.t. the formula evaluates to 1. ❑ For the above example, Yes: x5=1, x7=0, x1=1