[인공지능] propositional logic - 4

Satisfiability and Entailment

Satisfiable

• 정의: 문장이 만족 가능(satisfiable)하다는 것은 그 문장이 적어도 하나의 세계에서 참이라는 것을 의미한다.

Entailment Testing with SAT Solver:

만약 우리가 매우 효율적인 SAT(Satisfiability) solver를 가지고 있다면, 이를 사용하여 함의(entailment)를 테스트하는 방법은 다음과 같다

• 주어진 α가 β를 함의한다고 표현되면 α⊨β.
• 이는 α⇒β가 모든 세계에서 참이라는 것과 동일하다.
• 이는 ¬(α⇒β)가 모든 세계에서 거짓이라는 것과 동일하다.
• 이는 α∧¬β가 모든 세계에서 거짓이라는 것과 동일하며, 즉, 만족 불가능(unsatisfiable)하다는 것을 의미한다.

Procedure

• 결론의 부정(negated conclusion)을 추가하고 만족 가능성(불만족 가능성)을 테스트한다. 이 방법은 'reductio ad absurdum'라고도 알려져 있다.

CNF and SAT Solvers

• 효율적인 SAT solver들은 대부분 Conjunctive Normal Form (CNF)에서 작동한다.

Conjunctive Normal Form (CNF)

CNF는 모든 문장이 절(clauses)의 연결<교집합 and 집합>(conjunction)로 표현될 수 있는 형태이다.

각 절은 리터럴 (literals) 의 분리<합집합> (disjunction)로 이루어져있다.

리터럴(Literal): 리터럴은 기호(symbol) 또는 부정된 기호(negated symbol)이다.

 

문장을 CNF로 변환하는 것은 일련의 표준 변환을 통해 이루어진다.

• 주어진 문장: A⇒(W⇔B)
• 양조건식 제거: A⇒((W⇒B)∧(B⇒W))
  • 양조건식 W⇔B를 두 개( biconditional )의 함의( implications )로 분리(replace)한다.
•  함의 제거: ¬A∨((¬W∨B)∧(¬B∨W))
  • 함의 α⇒β를 ¬α∨β로 변환한다.
•  분배: (¬A∨¬W∨B)∧(¬A∨¬B∨W)
  • ∨  연산자를 ∧ 연산자에 대해 분배한다.

Efficient SAT Solvers

효율적인 SAT 솔버의 핵심 구성 요소와 작동 방식에 대해 설명한다.

 

DPLL(Davis-Putnam-Logemann-Loveland) 알고리즘은 현대 SAT solver의 핵심이다.

 

DPLL은 모델의 재귀적 깊이 우선 열거( Recursive depth-first enumeration )를 수행하면서 추가 기능을 제공한다.

• Early Termination
  • 모든 절이 만족되거나 어떤 절이 거짓이 되면 탐색을 중단한다.
  • 조건 1. all clauses are satisfied
  • 예시: (A∨B)∧(A∨¬C)는 {{A=true}에 의해 만족되어 탐색을 중단한다.
  • 조건 2. any clause is falsified
  • 예시: (A∨B)∧(A∨¬C)는 {A=false,B=false}에 의해 거짓이 되므로 탐색을 중단한다.
• Pure Literals
  • 아직 만족되지 않은(as-yet-unsatisfied) 절에서 기호의 모든 출현(occurrences)이 동일한 부호(sign)를 가지면, 그 기호에 그 값을 부여한다.
  • 예시: (A∨B)∧(A∨¬C)∧(C∨¬B)에서 A는 순수(pure)하고 양성(positive)이므로 참으로 설정한다.
• Unit Clauses
  • 절이 하나의 리터럴( single literal) 로 남으면, 절을 만족시키기 위해 기호(symbol)를 설정한다.
  • 예시: A=false인 경우, (A∨B)∧(A∨¬C)는 (false∨B)∧(false∨¬C), 즉 (B)∧(¬C)가 된다.
  • 유닛 절( unit clauses )을 만족시키면 종종 추가 전파( further propagation ), 새로운 유닛 절 등이 발생한다.

DPLL Algorithm

function DPLL(clauses,symbols,model) returns true or false

    if every clause in clauses is true in model then return true
    if some clause in clauses is false in model then return false
    P,value ←FIND-PURE-SYMBOL(symbols,clauses,model)
    if P is non-null then return DPLL(clauses, symbols–P, model∪{P=value})

    P,value ←FIND-UNIT-CLAUSE(clauses,model)
    if P is non-null then return DPLL(clauses, symbols–P, model∪{P=value})

    P ← First(symbols); rest ← Rest(symbols)
    return or(DPLL(clauses,rest,model∪{P=true}),

                      DPLL(clauses,rest,model∪{P=false}))

 

 

function DPLL(clauses,symbols,model) returns true or false

함수 정의: DPLL 함수는 clauses (절의 집합), symbols (기호의 목록), model (현재 모델) 세 개의 인자를 받고 참 혹은 거짓으로 반환한다 

 

    if every clause in clauses is true in model then return true

모든 절이 참인 경우, 함수는 참을 반환한다.

 

    if some clause in clauses is false in model then return false

어떤 절이 거짓인 경우, 함수는 거짓을 반환합니다.

 

    P,value ←FIND-PURE-SYMBOL(symbols,clauses,model)

 FIND-PURE-SYMBOL 함수를 사용하여 순수 기호P와 그 값value가 무엇인지 찾습니다.

 

    if P is non-null then return DPLL(clauses, symbols–P, model∪{P=value})

 순수 기호P가 있다면(non-null) , 그 기호P를 전체 기호 집합에서 제거하고, 모델에 그 기호P와 그 값value가 추가된 상태로 DPLL 함수를 재귀적으로 호출합니다.

 

    P,value ←FIND-UNIT-CLAUSE(clauses,model)

 FIND-UNIT-CLAUSE 함수를 사용하여 유닛 절(P)과 그 값(value)이 무엇인지 찾습니다.

 

    if P is non-null then return DPLL(clauses, symbols–P, model∪{P=value})

P 곧 유닛 절이 있다면, 그 기호P를 전체 기호 집합에서 제거하고, 모델에 그 기호P와 그 값이 추가된 상태로 DPLL 함수를 재귀적으로 호출합니다.

함수는 유닛 절(하나의 할당되지 않은 리터럴만 있는 절)을 찾고 그 절을 참으로 만드는 값을 할당합니다. 그런 다음 업데이트된 모델과 남은 심볼로 DPLL 함수를 재귀적으로 호출합니다.

 

    P ← First(symbols); rest ← Rest(symbols)

리스트에서 첫 번째 심볼과 나머지 심볼을 선택합니다.

 

    return or(DPLL(clauses,rest,model∪{P=true}),

                      DPLL(clauses,rest,model∪{P=false}))

선택된 심볼을 참으로 할당한 경우와 거짓으로 할당한 경우에 대해 DPLL 함수를 두 번 재귀적으로 호출합니다. 함수는 두 재귀 호출 중 하나가 참을 반환하면 참을 반환합니다.

 

Efficiency

DPLL 알고리즘의 효율성과 그 효율성을 향상시키기 위한 여러 기술을 설명합니다.

• 단순한 DPLL 알고리즘 구현 : Naïve implementation of DPLL은 대략 100개의 변수를 처리할 수 있다.
• Extras : Efficiency-Enhancing Techniques:
  • Smart variable and value ordering : 스마트한 변수 및 값 정렬 기술을 사용하여 탐색 공간을 효율적으로 탐색한다.
  • 분할 정복(Divide and conquer): 큰 문제를 작은 하위 문제로 분할하여 각 하위 문제를 독립적으로 해결한다.
  • 캐싱(Caching): 해결할 수 없는(unsolvable) 하위 케이스를 extra clause로 캐시하여 이를 재활용하고, 동일한 계산을 반복하지 않는다.
  • Cool 인덱싱(indexing) 및 증분 재계산(incremental recomputation): 이 러한 기술을 사용하여 DPLL 알고리즘의 각 단계를 효율적으로 만든다. (일반적으로 O(1) 복잡도를 가짐)
    • 각 변수가 양의(+ve) 또는 음의(-ve)로 나타나는 절의 인덱스를 유지한다.
    • 만족된 절의 수를 추적하고, 변수가 할당될 때 업데이트합니다.
    • 각 절에서 남아 있는 리터럴의 수를 추적합니다.

• 실제 DPLL 알고리즘 구현: 위의 기술들을 적용하면, 실제 DPLL implementation은 약 100,000,000개의 변수를 처리할 수 있습니다.