DPLL(T)

コンピュータサイエンスにおいて、DPLL(T)はSMT問題の充足可能性を判定するためのフレームワークである。このアルゴリズムは、元のSAT解決DPLLアルゴリズムを拡張し、任意の理論Tについて推論する機能を備えている。^{[ 1 ]}^{[ 2 ]}^{[ 3 ]}大まかに言うと、このアルゴリズムはSMT問題を、原子をブール変数に置き換えたSAT式に変換することで機能する。アルゴリズムはSAT問題に対する充足評価を繰り返し見つけ、理論ソルバーを参照してドメイン固有の理論の下での一貫性をチェックし、その後（矛盾が見つかった場合）この情報を使用してSAT式を改良する。^{[ 4 ]}

MicrosoftのZ3 Theorem ProverやCVC4など、多くの最新の SMT ソルバーは、コアとなるソルビング機能を実現するために DPLL(T) を使用しています。^{[ 5 ]}^{[ 6 ]}^{[ 7 ]}

参考文献

↑ Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). "DPLL(T): 高速決定手順". In Alur, Rajeev; Peled, Doron A. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 3114. Springer Berlin Heidelberg. pp. 175–188 . doi : 10.1007/978-3-540-27813-9_14 . ISBN 9783540278139。
↑ Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). "SAT および SAT Modulo Theories の解法: 抽象的な Davis–Putnam–Logemann–Loveland 手順から DPLL(T) へ". J. ACM . 53 (6): 937– 977. doi : 10.1145/1217856.1217859 . ISSN 0004-5411 . S2CID 14058631 .
↑ Nieuwenhuis, Robert; Oliveras, Albert (2005). "DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic". In Etessami, Kousha; Rajamani, Sriram K. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 3576. Springer Berlin Heidelberg. pp. 321–334 . doi : 10.1007/11513988_33 . ISBN 9783540316862。
↑ Reynolds, Andrew (2015). "充足可能性モジュロ理論とDPLL(T)" (PDF) .アイオワ大学. 2019年4月8日取得.
↑ de Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: 効率的なSMTソルバー". Ramakrishnan, CR; Rehof, Jakob (編). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Vol. 4963. Springer Berlin Heidelberg. pp. 337–340 . doi : 10.1007/978-3-540-78800-3_24 . ISBN 9783540788003。
↑ Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "文字列と正規表現の理論のためのDPLL(T)理論ソルバー". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 646–662 . doi : 10.1007 /978-3-319-08867-9_43 . ISBN 978-3-319-08867-9。
↑ブルットメッソ、ロベルト。チマッティ、アレッサンドロ。フランゼン、アンダース。グリッジョ、アルベルト。セバスティアーニ、ロベルト (2008)。「MathSAT 4 SMT ソルバー」。 Gupta , アールティ;マリク、シャラド (編)。コンピュータ支援による検証。コンピューターサイエンスの講義ノート。 Vol. 5123. シュプリンガーベルリンハイデルベルク。 pp. 299–303。土井: 10.1007/978-3-540-70545-1_28。ISBN 9783540705451。

[1] Ganzinger, Harald; Hagen, George; Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2004). "DPLL(T): 高速決定手順". In Alur, Rajeev; Peled, Doron A. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 3114. Springer Berlin Heidelberg. pp. 175–188 . doi : 10.1007/978-3-540-27813-9_14 . ISBN 9783540278139。

[2] Nieuwenhuis, Robert; Oliveras, Albert; Tinelli, Cesare (2006). "SAT および SAT Modulo Theories の解法: 抽象的な Davis–Putnam–Logemann–Loveland 手順から DPLL(T) へ". J. ACM . 53 (6): 937– 977. doi : 10.1145/1217856.1217859 . ISSN 0004-5411 . S2CID 14058631 .

[3] Nieuwenhuis, Robert; Oliveras, Albert (2005). "DPLL(T) with Exhaustive Theory Propagation and Its Application to Difference Logic". In Etessami, Kousha; Rajamani, Sriram K. (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Vol. 3576. Springer Berlin Heidelberg. pp. 321–334 . doi : 10.1007/11513988_33 . ISBN 9783540316862。

[4] Reynolds, Andrew (2015). "充足可能性モジュロ理論とDPLL(T)" (PDF) .アイオワ大学. 2019年4月8日取得.

[5] Moura, Leonardo; Bjørner, Nikolaj (2008). "Z3: 効率的なSMTソルバー". Ramakrishnan, CR; Rehof, Jakob (編). Tools and Algorithms for the Construction and Analysis of Systems . Lecture Notes in Computer Science. Vol. 4963. Springer Berlin Heidelberg. pp. 337–340 . doi : 10.1007/978-3-540-78800-3_24 . ISBN 9783540788003。

[6] Liang, Tianyi; Reynolds, Andrew; Tinelli, Cesare; Barrett, Clark; Deters, Morgan (2014). "文字列と正規表現の理論のためのDPLL(T)理論ソルバー". In Biere, Armin; Bloem, Roderick (eds.). Computer Aided Verification . Lecture Notes in Computer Science. Cham: Springer International Publishing. pp. 646–662 . doi : 10.1007 /978-3-319-08867-9_43 . ISBN 978-3-319-08867-9。

[7] ブルットメッソ、ロベルト。チマッティ、アレッサンドロ。フランゼン、アンダース。グリッジョ、アルベルト。セバスティアーニ、ロベルト (2008)。「MathSAT 4 SMT ソルバー」。 Gupta , アールティ;マリク、シャラド (編)。コンピュータ支援による検証。コンピューターサイエンスの講義ノート。 Vol. 5123. シュプリンガーベルリンハイデルベルク。 pp. 299–303。土井: 10.1007/978-3-540-70545-1_28。ISBN 9783540705451。

[ 1 ]

[ 2 ]

[ 3 ]

[ 4 ]

[ 5 ]

[ 6 ]

[ 7 ]

参考文献

関連するトピック

SMT

SAT

DPLLアルゴリズムを拡張し、任意の

理論