DPLL(T)

DPLL(T)

컴퓨터 과학에서 DPLL(T)은 SMT 문제의 충족 가능성을 결정하기 위한 프레임워크입니다.이 알고리즘은 원래의 SAT 해결 DPLL 알고리즘을 임의의 이론 [1][2][3]T에 대해 추론할 수 있는 능력으로 확장합니다.높은 수준에서 알고리즘은 SMT 문제를 원자가 부울 변수로 대체되는 SAT 공식으로 변환하여 작동합니다.이 알고리즘은 반복적으로 SAT 문제에 대한 만족스러운 평가를 찾고, 이론 해결사와 상의하여 영역별 이론에서 일관성을 확인한 다음, (부정성이 발견될 경우) [4]이 정보로 SAT 공식을 수정한다.

Microsoft의 Z3 Oremy Prover와 같은 많은 최신 SMT 솔버는 핵심 해결 [5][6]능력을 강화하기 위해 DPLL(T)을 사용합니다.

레퍼런스

  1. ^ Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). Alur, Rajeev; Peled, Doron A. (eds.). "DPLL(T): Fast Decision Procedures". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 3114: 175–188. doi:10.1007/978-3-540-27813-9_14. ISBN 9783540278139.
  2. ^ Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). "Solving SAT and SAT Modulo Theories: From an Abstract Davis–Putnam–Logemann–Loveland Procedure to DPLL(T)". J. ACM. 53 (6): 937–977. doi:10.1145/1217856.1217859. ISSN 0004-5411.
  3. ^ Nieuwenhuis, Robert; Oliveras, Albert (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 3576: 321–334. doi:10.1007/11513988_33. ISBN 9783540316862.
  4. ^ Reynolds, Andrew (2015). "Satisfiability Modulo Theories and DPLL(T)" (PDF). The University of Iowa. Retrieved 2019-04-08.
  5. ^ de Moura, Leonardo; Bjørner, Nikolaj (2008). Ramakrishnan, C. R.; Rehof, Jakob (eds.). "Z3: An Efficient SMT Solver". Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 4963: 337–340. doi:10.1007/978-3-540-78800-3_24. ISBN 9783540788003.
  6. ^ Bruttomesso, Roberto; Cimatti, Alessandro; Franzén, Anders; Griggio, Alberto; Sebastiani, Roberto (2008). Gupta, Aarti; Malik, Sharad (eds.). "The MathSAT 4 SMT Solver". Computer Aided Verification. Lecture Notes in Computer Science. Springer Berlin Heidelberg. 5123: 299–303. doi:10.1007/978-3-540-70545-1_28. ISBN 9783540705451.
P np NP

이 이론적인 컴퓨터 공학 관련 기사는 짧은 글이다.위키피디아를 확장함으로써 위키피디아를 도울 수 있습니다.