DPLL 알고리즘

DPLL algorithm
DPLL
Dpll11.png
5번의 시도(빨간색) 후 변수 할당 a=1, b=1을 선택하면 단위 전파 후(아래쪽) 성공(녹색): 왼쪽 위 CNF 공식이 만족됩니다.
학급부울 만족도 문제
data 구조이진 트리
최악의 경우 성능
베스트 케이스 성능( ){ O (1} (상수)
최악의 경우 공간의 복잡성( ){ O ( ) （ ） （ )))알고리즘)

논리학과 컴퓨터 공학에서 데이비스는...Putnam-Logemann-Loveland(DPLL) 알고리즘은 CNF-SAT 문제를 해결하기 위해 결합 정규 형식으로 명제 논리 공식의 만족도를 결정하기 위한 완전한 역추적 기반 검색 알고리즘입니다.

1961년 마틴 데이비스, 조지 로게만, 도널드 W. 러브랜드에 의해 도입되었으며 초기 데이비스의 개량형이다.Putnam 알고리즘은 1960년 Davis와 Hilary Putnam에 의해 개발된 해상도 기반 절차입니다.특히 오래된 출판물에서 데이비스-로게만-러블랜드 알고리즘은 종종 "데이비스-"로 언급된다.Putnam 메서드" 또는 "DP 알고리즘"입니다.구별을 유지하는 다른 일반적인 이름으로는 DLL과 DPLL이 있습니다.

구현 및 응용 프로그램

SAT 문제는 이론적인 측면과 실제적인 측면 모두에서 중요하다.복잡도 이론에서 그것은 NP-완전성이 입증되는 첫 번째 문제였고, 인공지능의 모델 검사, 자동 계획 및 스케줄링, 진단과 같은 다양한 응용 프로그램에 나타날 수 있다.

이와 같이 효율적인 SAT 해결사를 쓰는 것은 오랫동안 연구 주제였다.CRAPP(1996-1999)는 DPLL을 [1]사용한 초기 구현입니다.국제 SAT 대회에서는 2004년과 [4]2005년에 zChaff[2], MiniSat[3] 등 DPLL을 기반으로 한 구현이 1위를 차지했다.

DPLL을 수반하는 또 다른 응용은 자동화된 정리 증명 또는 충족 가능성 모듈로 이론(SMT)입니다.이것은 명제 변수가 다른 수학 이론의 공식으로 대체되는 SAT 문제입니다.

알고리즘

기본 역추적 알고리즘은 리터럴을 선택하고, true 값을 할당하고, 공식을 단순화한 다음, 단순화된 공식이 만족스러운지 재귀적으로 체크함으로써 실행됩니다.이 경우 원래 공식이 만족스러운지 여부를 재귀적으로 체크합니다.그렇지 않으면 반대되는 true 값을 가정하여 동일한 재귀 검사가 수행됩니다.이것은 문제를 두 가지 간단한 하위 문제로 분할하기 때문에 분할 규칙이라고 합니다.단순화 단계는 기본적으로 할당에서 참이 되는 모든 구를 공식에서 삭제하고 거짓이 되는 모든 리터럴을 나머지 구에서 삭제합니다.

DPLL 알고리즘은 각 단계에서 다음 규칙을 적극적으로 사용함으로써 백트래킹알고리즘보다 확장됩니다.

단위 전파
절이 단위구인 경우, 즉 할당되지 않은 리터럴이 하나만 포함된 경우, 이 절은 이 리터럴을 참으로 만들기 위해 필요한 값을 할당해야만 충족될 수 있습니다.따라서 선택의 여지가 없습니다.단위 전파는 단위구의 리터럴을 포함하는 모든 절을 삭제하고 단위구의 리터럴을 포함하는 모든 절에서 단위구의 리터럴의 보완을 폐기하는 것으로 구성됩니다.실제로, 이것은 종종 결정론적 단위 계단식으로 이어지며, 따라서 순진한 검색 공간의 많은 부분을 피한다.
순수 리터럴 소거
만약 명제 변수가 공식에서 하나의 극성만을 가지고 일어난다면, 그것은 순수라고 불립니다.순수 리터럴은 이를 포함하는 모든 구를 참으로 만드는 방식으로 항상 할당할 수 있습니다.따라서 이러한 방법으로 할당되면 이러한 절은 검색을 더 이상 제한하지 않으며 삭제할 수 있습니다.

한 절이 비어 있는 경우, 즉 모든 변수가 대응하는 리터럴을 거짓으로 할당되어 있는 경우, 주어진 부분 할당의 불만족성이 검출된다.공식의 만족도는 빈 구를 생성하지 않고 모든 변수가 할당되었을 때 또는 최신 구현에서 모든 구가 충족되었을 때 검출됩니다.완전한 공식에 대한 불만족 여부는 철저한 검색 후에만 확인할 수 있습니다.

DPLL 알고리즘은 다음의 의사 코드로 집약할 수 있습니다.여기서 δ는 CNF 공식입니다.

알고리즘 DPLL 입력: 구 δ 세트.출력: δ가 충족 가능한지 여부를 나타내는 True 값. 
dp do ← unit-lict(l, φ)에 단위구 {l}이(가) 있는 동안 함수 DPLL(L) ← - do ← pure-lict-lict(l, φ)에 순수하게 발생하는 리터럴 l이 있는 반면 φ do ← pure-lictictract(l, φ)에 빈 경우 true를 반환한다.)});
  • "←"는 할당을 나타냅니다.예를 들어 "가장 큰 ← 항목"은 가장 큰 값의 값이 항목 값으로 변경됨을 의미합니다.
  • "return"은 알고리즘을 종료하고 다음 값을 출력합니다.

이 의사 코드에서는unit-propagate(l, Φ)그리고.pure-literal-assign(l, Φ)단위 전파와 순수 리터럴 규칙을 각각 리터럴에 적용한 결과를 반환하는 함수입니다.l그리고 공식은Φ다시 말해, 모든 발생을 치환합니다.l'진실'과 같은 일이 있을 때마다not l식중에 "false"가 포함되어 있다Φ및 결과 수식을 간략화합니다.그or에서returnstatement는 단축 연산자입니다. Φ ∧ {l}를 "참"으로 치환한 단순화된 결과를 나타냅니다.l에Φ.

알고리즘은 두 가지 경우 중 하나로 종료됩니다.CNF 공식 중 하나Φ비어 있습니다. 즉, 절이 없습니다.그러면 모든 절이 공허하게 참이기 때문에 어떤 할당에서도 충족됩니다.그렇지 않은 경우, 공식에 빈 구가 포함되어 있는 경우 전체 집합에 대해 true인 멤버가 적어도1개 필요하기 때문에 해당 구가 완전히 false가 됩니다.이 경우, 이러한 절의 존재는 공식(모든 절의 결합으로 평가됨)이 참으로 평가될 수 없으며 만족스럽지 않아야 한다는 것을 의미한다.

의사코드 DPLL 함수는 최종 할당이 수식을 충족하는지 여부만 반환합니다.실제 구현에서는 일반적으로 부분 만족 할당도 성공 시 반환됩니다.이는 분기 리터럴 및 단위 전파 및 순수 리터럴 제거 중에 이루어진 리터럴 할당을 추적함으로써 도출할 수 있습니다.

Davis-Logemann-Loveland 알고리즘은 역추적 단계에서 고려된 문자인 분기 리터럴의 선택에 따라 달라집니다.그 결과, 이것은 엄밀하게는 알고리즘이 아니라 알고리즘의 패밀리로, 분기 리터럴을 선택하는 각각의 가능한 방법에 대해 1개씩이 됩니다.효율은 분기 리터럴 선택에 의해 크게 영향을 받습니다.브런치 리터럴 선택에 따라 실행 시간이 일정하거나 지수적으로 변화하는 경우가 있습니다.이러한 선택 함수를 휴리스틱 함수 또는 분기 [5]휴리스틱이라고도 합니다.

시각화

데이비스, 로게만, 러브랜드(1961)가 이 알고리즘을 개발했다.이 원래 알고리즘의 속성은 다음과 같습니다.

  • 검색을 기반으로 합니다.
  • 그것은 거의 모든 현대 SAT 해결사의 기초가 된다.
  • 학습 또는 비연대적 역추적(1996년 도입)을 사용하지 않는다.

시간순으로 역추적하는 DPLL 알고리즘을 시각화한 예:

  • All clauses making a CNF formula

    CNF 수식을 만드는 모든 구

  • Pick a variable

    변수 선택

  • Make a decision, variable a = False (0), thus green clauses becomes True

    결정을 내립니다. 변수 a = False(0). 따라서 녹색 절이 True가 됩니다.

  • After making several decisions, we find an implication graph that leads to a conflict.

    몇 가지 결정을 내린 후 충돌로 이어지는 시사 그래프를 찾습니다.

  • Now backtrack to immediate level and by force assign opposite value to that variable

    이제 즉시 수준으로 역추적하여 해당 변수에 반대 값을 강제로 할당합니다.

  • But a forced decision still leads to another conflict

    하지만 강요된 결정은 또 다른 갈등으로 이어집니다.

  • Backtrack to previous level and make a forced decision

    이전 수준으로 되돌아가서 강제적인 결정을 내리다

  • Make a new decision, but it leads to a conflict

    새로운 결정을 내리지만 충돌로 이어집니다.

  • Make a forced decision, but again it leads to a conflict

    강요된 결정을 내리지만, 다시 갈등으로 이어집니다.

  • Backtrack to previous level

    이전 수준으로 역추적

  • Continue in this way and the final implication graph

    이 방법으로 계속하여 최종 시사 그래프

관련 알고리즘

1986년 이후, (축소 순서) 바이너리 결정 다이어그램도 SAT 문제 해결에 사용되고 있습니다.

1989~1990년에 스톨마르크의 공식 검증 방법이 발표되어 특허를 받았다.그것은 공업용도에 [6]어느 정도 쓰이고 있다.

DPLL은 DPLL([1]T) 알고리즘을 통해 1차 로직의 fragment를 증명하는 자동 정리를 위해 확장되었습니다.

2010-2019년 10년 동안 알고리즘 개선 작업은 알고리즘을 더 빠르게 만들기 위해 분기 리터럴과 새로운 데이터 구조를 선택하기 위한 더 나은 정책을 찾아냈다. 특히 단위 전파에 관한 부분은 그렇다.단, 주요 개선사항은 보다 강력한 알고리즘인 CDCL(Conflict-Driven Clause Learning)으로, DPLL과 유사하지만 충돌에 도달한 후 충돌의 근본 원인(변수에 대한 할당)을 학습하고 이 정보를 사용하여 sa에 도달하지 않도록 비연대적 역추적(백점핑)을 수행합니다.나는 또 갈등을 겪는다.대부분의 최첨단 SAT 해결사는 2019년 [7]현재 CDCL 프레임워크를 기반으로 한다.

다른 개념과의 관계

불만족스러운 인스턴스에서의 DPLL 기반 알고리즘 실행은 트리 해상도 [8]반박 증명에 해당합니다.

「 」를 참조해 주세요.

레퍼런스

Wikimedia Commons에는 Davis-Putnam-Logemann-Loveland 알고리즘과 관련된 미디어가 있습니다.

일반

  • Davis, Martin; Putnam, Hilary (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376.
  • Davis, Martin; Logemann, George; Loveland, Donald (1961). "A Machine Program for Theorem Proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
  • Ouyang, Ming (1998). "How Good Are Branching Rules in DPLL?". Discrete Applied Mathematics. 89 (1–3): 281–286. doi:10.1016/S0166-218X(98)00045-6.
  • John Harrison (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. pp. 79–90. ISBN 978-0-521-89957-4.

특정한

  1. ^ a b Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesar (2004), "Abstract DPLL and Abstract DPLL Modulo Theories" (PDF), Proceedings Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, pp. 36–50
  2. ^ zChaff website
  3. ^ "Minisat website".
  4. ^ The international SAT Competitions web page, sat! live
  5. ^ Marques-Silva, João P. (1999). "The Impact of Branching Heuristics in Propositional Satisfiability Algorithms". In Barahona, Pedro; Alferes, José J. (eds.). Progress in Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Évora, Portugal, September 21–24, 1999 Proceedings. LNCS. Vol. 1695. pp. 62–63. doi:10.1007/3-540-48159-1_5. ISBN 978-3-540-66548-9.
  6. ^ Stålmarck, G.; Säflund, M. (October 1990). "Modeling and Verifying Systems and Software in Propositional Logic". IFAC Proceedings Volumes. 23 (6): 31–36. doi:10.1016/S1474-6670(17)52173-4.
  7. ^ Möhle, Sibylle; Biere, Armin (2019). "Backing Backtracking" (PDF). Theory and Applications of Satisfiability Testing – SAT 2019. 11628: 250–266. doi:10.1007/978-3-030-24258-9_18.
  8. ^ Van Beek, Peter (2006). "Backtracking search algorithms". In Rossi, Francesca; Van Beek, Peter; Walsh, Toby (eds.). Handbook of constraint programming. Elsevier. p. 122. ISBN 978-0-444-52726-4.

추가 정보

  • Malay Ganai; Aarti Gupta; Dr. Aarti Gupta (2007). SAT-based scalable formal verification solutions. Springer. pp. 23–32. ISBN 978-0-387-69166-4.
  • Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Satisfiability Solvers". In Van Harmelen, Frank; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. Vol. 3. Elsevier. pp. 89–134. doi:10.1016/S1574-6526(07)03002-7. ISBN 978-0-444-52211-5.