DPLL 일관된 리터럴 집합이란 무엇입니까?

Question

SAT 솔버를 작성 중이며 DPLL 알고리즘을 구현하기 시작했습니다. 나는 알고리즘을 이해하고 그것이 어떻게 작동하는지, 나는 또한 그것의 변형을 구현했다. 그러나 나를 귀찮게하는 것은 다음 것이다.

function DPLL(Φ) 
    if Φ is a consistent set of literals 
     then return true; 
    if Φ contains an empty clause 
     then return false; 
    for every unit clause l in Φ 
     Φ ← unit-propagate(l, Φ); 
    for every literal l that occurs pure in Φ 
     Φ ← pure-literal-assign(l, Φ); 
    l ← choose-literal(Φ); 
    return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l)); 

은 무엇을 의미 하는가, Φ 리터럴의 일관된이라고? 나는 이 일치하지 않는 것은을 의미하며, 은 일관성이 없음을 의미합니다.. 왜 현재 할당이 문제를 위조하지 않는다면 true을 반환 할 수 있습니까?

내 SAT 해결사를 구현 한 방법은 모든 절을 사실로 만든 할당이 올 때마다 해당 할당을 반환하고 알고리즘이 완료되었음을 의미합니다. 하지만 주어진 할당 때문에, 문제에 대한 해결책이되기 위해서는 모든 절이 참이어야합니다. 이해가 안됩니다. 이 단지의 문제를 해결할 경우에 true을 반환 할 수있는 방법은 무엇입니까? 여기서 무엇인가 잘못되었지만, Φ이 일관성이 있다면 거짓이 아니라는 것을 의미합니다. 그러나 여전히 결정할 수 없습니다.).

Answer 1

Φ는 리터럴과 리터럴 만 포함하고 Φ에는 부정이없는 경우 일관된 리터럴 집합입니다. 순수하고 단위 규칙을 통해 DPLL 알고리즘은 점차적으로 모든 절을 만족하는 리터럴 목록으로 절 목록을 변환합니다. 알고리즘이 발생하면 (Φ는 일관된 리터럴 집합입니다.) 시도하거나 리터럴 할당이 부족하여 최상위 DPLL 호출이 false를 반환하면 알고리즘이 완료됩니다.