Trivial Cases Problem (k-SAT) Input:k-CNF formula Output:determine whether is satisfiable. Clauses are disjoint: Φ=(x1V2Vx3)Λ(x4Vx5Vx6)Λ(xV7 Xs VX9). resolve each clause independently(is alwsays satisfiable!) 。m<2k=Φis always satisfiable. m:of clausesProblem ( -SAT) Input: -CNF formula . Output: determine whether is satisfiable. k k Φ Φ • Clauses are disjoint: resolve each clause independently (Φ is always satisfiable!) • ⟹ is always satisfiable. Φ = (x1 ∨ ¬x2 ∨ x3) ∧ (x4 ∨ x5 ∨ x6) ∧ (x7 ∨ ¬x8 ∨ ¬x9) m < 2k Φ Trivial Cases m: # of clauses