SAT (SATisfiability) Problem

• Instance: CNF (Conjunctive Normal Form; POS: Product Of Sum)

  

• Problem: check if CNF can be true

  

• Naive approach: 진리표 쓰기 → $2^n$

• Some varients

  • Horn Formula: all clauses contain most One positive literal → greedy; linear time
  • 2SAT: all clauses have two literals → SCC; linear time

Circuit SAT : Generalization of SAT

위 clause들을 and, or, not으로 표현한 것

ANY NP Problem → Circuit SAT

Circuit SAT is NP-Complete

• Any Algorithm that takes n bit input, produce Y/N can be represented as a circuit.
• consider problem X in NP, poly-time certifier C(s,t) then certificate t has length poly(|s|) then X is to find a solution t, that satisfies C(s,t) is true
• now view C(s,t) has |s|+poly(|s|) input → convert it into poly-size circuit K
• now circuit K is satisfiable ↔ C(s,t)=yes

Any NP Problem (C(s,t)) is reduced into Circuit SAT

therefore circuit SAT is NP, reduced → NP Complete

Circuit SAT → 3SAT

3SAT: each clause has max 3 literals

3SAT is NP-Complete (Circuit-SAT ≤ 3SAT)