k-SAT Conjunctive Normal Form(CNF): Liberals Φ=xVV)∧1VV4∧③V V7x5) clause Boolean variables:x1,x2,...,{True,False} k-CNF:each clause contains exactly k variables Problem(k-SAT) Input:k-CNF formula Output:determine whether is satisfiable. 。[Cook-Levin]NP-hard if k≥3• Conjunctive Normal Form (CNF): Boolean variables: • -CNF: each clause contains exactly variables • [Cook-Levin] NP-hard if Φ = (x1 ∨ ¬x2 ∨ x3) ∧ (x1 ∨ x2 ∨ x4) ∧ (x3 ∨ ¬x4 ∨ ¬x5) x1, x2,…, xn ∈ {𝚃𝚛𝚞𝚎, 𝙵𝚊𝚕𝚜𝚎} k k k ≥ 3 k-SAT clause literals Problem ( -SAT) Input: -CNF formula . Output: determine whether is satisfiable. k k Φ Φ