Please enable JavaScript.

Coggle requires JavaScript to display documents.

Normal Forms & DPLL - Coggle Diagram

- - - - 首先转化为NNF
      - 使用以下公式：
        F1∧(F2 ∨F3)≡(F1 ∧F2)∨(F1 ∧F3)
        (F1 ∨F2)∧F3 ≡(F1 ∧F3)∨(F2 ∧F3)
  - - - 首先转化为NNF
      - 使用以下公式：
        (F1 ∧F2)∨F3 ≡(F1 ∨F3)∧(F2 ∨F3)
        F1 ∨(F2 ∧F3)≡(F1 ∨F2)∧(F1 ∨F3)
  - - - F1 and F2 are equisatisfiability, iff F1 is satisfiable iff F2 is satisfiable
      - 假如F1和F2满足equisatisdiability，他们不一定equivalent
  - - - Tseitin's Transformation
        
        with only a linear increase in size
        
        F is unsat iff F' is unsat
        
        Any model of F' is a model of F, if we disregard additional variables
    - - DPLL (Davis-Putnam-Logemann-Loveland)
      - convert to CNF using Tseitin's Transformation
      - Deductive principle underlying DPLL is propositional resolution
      - can only be applied to formulas in CNF
      - 实现
        
        C 1 ≙ (l 1 ∨ ... ∨ p ∨ ... ∨ l k )
        
        C 2 ≙ (l 1 ’ ∨ ... ∨ ¬p ∨ ... ∨ l k’ )
        
        deduce a new clause called the resolvent:
        C 3 ≙ (l 1 ∨ ... ∨ l k ∨ l 1 ’ ∨ ... ∨ l k’ )
        
        Suppose p is assigned ⊤, then ¬p is ⊥, and therefore l1’ ∨ ... ∨ lk’ must be true Suppose p is assigned ⊥, then p is ⊥, and therefore l1 ∨ ... ∨ lk must be true
        
        Thus C3 must be true