k-SAT .n Boolean variables:x1,x2,...,xnEtrue,false} conjunctive normal form: k-CNFΦ=C1∧C2∧·∧Cm “ils satisfiable?' ·n clauses::Cl,C2,,Cm .each clause Ci=iveiv...vli is a disjunction of k distinct literals ·each literal::lj∈{xr,xr}for some r degree d:each clause shares variables with at most d other clausesk-SAT • n Boolean variables: x1,x2,...,xn 2 {true, false} • m clauses: C1,C2,...,Cm • each clause Ci = `i1 _`i2 _···_`ik • each literal: for some r • degree d : is a disjunction of k distinct literals `j 2 {xr ,¬xr } each clause shares variables with at most d other clauses k-CNF ¡ = C1 ^C2 ^···^Cm • conjunctive normal form: “Is φ satisfiable?