DPLL算法的形式化与提取(ExtractingtheFormalizationandImplementationoftheDPLLAlgorithm)

179 浏览量更新于2023-12-12 收藏 685KB PDF 举报

身份认证购VIP最低享 7 折!

领优惠券(最高得80元）

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）243-256www.elsevier.com/locate/entcs提取DPLL算法安德鲁·劳伦斯1，2乌尔里希·伯杰3莫妮卡·塞森伯格4斯旺西大学英国斯旺西摘要我们形式化了DPLL证明系统的完备性证明，并从中提取出一个DPLL SAT求解器。当应用于合取范式中的命题公式时，程序要么产生一个令人满意的赋值，要么产生一个DPLL推导，表明它是不满意的。我们使用非计算量化器从提取的程序中删除冗余的计算内容并提高其性能。形式化是在Minlog系统中进行的保留字：程序抽取，交互式定理证明，SAT。1引言为了在工业环境中使用验证工具，它们必须高度可信，并且在许多情况下需要进行认证。我们提出了一个新的应用程序提取开发正确的可证明的决策过程。SAT求解器是试图解决布尔可满足性问题的决策过程它们是许多当代核查工具的重要组成部分。在工业环境中使用的大多数SAT解算器都基于DPLL证明系统。我们在交互式定理证明器Minlog [20，2，4]中形式化了DPLL证明系统的正确性和完整性证明。使用Minlog的程序提取设施，我们已经能够获得正式验证的SAT求解算法。当在CNF公式上运行时，该算法产生满足公式的模型或显示其不满足性的DPLL推导。然后通过将证明中的某些泛量化器标记为非计算性，1我们要感谢英维思英国铁路公司的支持。2电子邮件：csal@swansea.ac.uk3电子邮件：u. swansea.ac.uk4电子邮件：m. swansea.ac.uk1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.08.016244A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243Minlog系统中的优化。所产生的程序的性能进行了测试，与一些鸽子洞公式。程序抽取的目的是从构造性的证明中产生经过形式验证的程序。程序提取的早期工作的一个例子是在Nuprl系统中完成的[10]。Minlog中程序提取的示例可以在[5，3]中找到。其他支持程序提取的成熟的交互式定理证明器是Coq [6]，它基于归纳构造的演算，以及Isabelle [22，21]，一个扩展了许多逻辑的通用定理证明器。最近，其他基于依赖类型的交互式定理证明器[PM80]，如Agda[9]和警句[18]，已经出现了实现Curry-Howard对应[12，13]，因此也可以被视为支持程序提取。已经进行了几次尝试将自动定理证明器集成到Coq中。这项工作的大部分利用Coq的程序提取设施，以提取程序的证明决策程序。基于DPLL算法的SAT求解器已被形式化，其可靠性和完整性在Coq [15]中得到验证，并从证明中提取了代码。最后，提取的系统已被实例化的命题片段的Coq的逻辑创建一个用户友好的证明策略。二元决策图已经在Coq [26]中形式化。然后证明了它们的正确性，并在Caml中提取了经过认证的BDD算法。其形式化的主要原因是在Coq中集成了符号模型检查。Isabelle亦进行了大量工作，多项决策程序已获验证并整合至系统中。DPLL算法已在[16]中形式化自动定理证明器Metis [23]在Isabelle内部被正式验证，现在被用来从更快的外部过程（如Sledgehammer [8]中使用的过程）在Coq和Isabelle中形式化DPLL SAT求解器的方法[15，16相反，我们证明了一个定理，该定理只是指出CNF中的每个公式要么是不可满足的，要么是一个模型，并从证明中合成程序。从长远来看，我们希望将自动验证技术集成到Minlog中。在Minlog中提取SAT求解器是实现我们最终目标的一步2个房间我们从一些基本定义开始，如下[15，16]。定义2.1(i) 一个文字l要么是一个正变量+v，要么是一个负变量−v，即一个带有标签+或−的变量v(ii) 我们定义一个bar运算，它计算一个字面量的相反值，如下：+v= −v，−v=+v。(iii) 我们设置Var（+v）= Var（-v）= v，Var（L）={Var（l）|l∈L}对于一个文字集A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243245L，并且Var（Δ）={Var（L）|L∈Δ}对于一组文字集合Δ。(iv) 子句C是文字{11，.，lk}，被视为文字的析取。(v) 一个公式是合取范式（CNF），如果它是子句的有限合取。公式Δ总是指CNF中的公式，并且我们将用子句的有限集合{C1，...，Ck}，表示C i的合取。(vi) 赋值Γ是文字{l1，.，lk}被视为元素的结合。(vii) 一个值Γ是consistent（cons（Γ）），如果nl（l∈Γ→l∈/Γ）.(viii) 一个模型是一个全函数M，它将文字映射到布尔值，并满足性质l（MlParticipi<$Ml）。我们将使用缩写• M|= Γ，对于l ∈ Γ（M l）（“M是Γ的模型”），• M|= Δ，对于<$C ∈ Δ <$l ∈ C（M l）（“M是Δ的模型”）。如果存在一个模型满足这两个条件，我们称一个赋值为Γ，一个公式为Δ相容的（compatible（Γ， Δ）），即： M（M）|= r M |= Δ）;否则，Γ和Δ称为不相容（不相容（Γ，Δ））。定义2.2一个赋值Δ是由一个赋值和一个公式组成的对。r 作为一个特例，当Γ为空时，ΔΔ意味着Δ是不可满足的。在下文中，我们使用符号X，a：={x |x ∈ X<$x= a}（将a加到集合X上），X\a：={x|x∈ X<$xa}（从X中去掉a）。定义2.3[DPLL证明系统] DPLL证明系统由五条规则组成Γ，l<$Δ单位Δ，{l}Γ，lΔ，C红色Γ，l<$ Δ，（C，l）Γ，lΔElimΓ，l<$ Δ，（C，l）Γ► Δ,∅ 联系我们r，l< $Δ r，l<$ ΔSplitΓ► Δ3健全性和完整性在这一节中，我们概述了DPLL证明系统的可靠性和完整性的形式证明。我们将非常简短地介绍可靠性定理，因为它的证明没有计算内容，并进行了类似的证明在[15，16]中。另一方面，我们将详细描述完整性定理的证明，因为我们从中提取了SAT求解器我们首先将DPLL证明系统重新表述为一个可以在Minlog系统中立即形式化的归纳定义。定义中的每一条规则都有一个条款。我们符号化地用陈述“可衍生的”。246A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243定义3.1可导序列集合Γ Δ由以下（泛量化的）归纳子句归纳定义：连续性<$∈Δ→Γ <$ Δ单位{l}∈Δ→ Γ，l< $Δ\{l}→ Γ<$ ΔEliml∈Γ→l∈C→C∈Δ→ΓΔ\C→ΓΔ红l∈Γ→l∈C→C∈ Δ→Γ（Δ\C），（C\l）→ΓΔ分裂Γ，lΔ→Γ，lΔ→ΓΔ定理3.2（合理性）如果Γ Δ是可导的，则Γ和Δ是不相容的。证明过程中的结构归纳法的给定推导的r Δ。我们省略进一步的细节。现在我们将注意力转向DPLL证明系统的完备性定理。预期的完整性声明是：不相容的（Γ，Δ）→ Γ<$Δ。这个陈述的构造性证明将产生一个程序，不相容的Γ，Δ的DPLL证明我们通过用经典等价但构造性更强的析取“相容（Γ，Δ）<$Γ <$$>”替换蕴涵“不相容（Γ，Δ）→ Γ <$Δ "来重新表述该陈述通过这种方式，我们获得了一个增强的程序，该程序仍然计算不相容的Γ，Δ的DPLL证明，但如果Γ和Δ相容，则另外产生一个模型定理3.3（DPLL的完备性）相容的（Γ， Δ）<$Γ <$Δ证据我们的目标是执行这样一种方式，一个有效的程序被提取的证明。因此，我们采取以下策略：(i) 由于执行Split规则是唯一一个计算开销很大的操作(ii) 我们通过将子句划分为“干净”和“不干净”子句来在证明级别上进行优化这通过减少所需的比较次数来为此，我们证明，对于所有的估值Γ，和公式Δ，Θ，<$∈/Θ<$cons（Γ）<$Var（Γ）<$Var（Θ）=< $ →（ΓΔ θ）M（M |= r M |= Δ θ）。证明是通过主要的归纳在措施μ（r; Δ; Θ）：=|（Δ θ）\\Var（r）|+#（Δ）+#（Θ）A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243247Σ哪里|X|：=集合XΔV：={l| <$C∈Δ（l∈C<$Var（l）∈/V}#（Δ）：=C∈Δ|C|和一个侧面感应|Δ|（即Δ中的子句数）。设Γ，Δ，Θbegivensu c h，使得ε∈/Θ，cons（Γ），且Var（Γ）∈Var（θ）=ε.情况1 Δ = Δ。情况1.1 Θ = θ。我们定义了一个模型M：M（l）= TrueParticel∈ Γ。则M| = rM| = holds。情况1.2 Θ f = θ f。设C是一个在Θ中的函数，且l∈C（C/=l，通过对Θ的假设）。则μ（（1，r）;Θ;θ）<μ（r;θ;Θ）since|Θ||Var（1，r）|<|Θ||Var（r）|. 因此，对于值（l，Γ），Θ，定理的假设显然是满足的。因此，这些值的归纳假设产生（r，lθ）π πM（M| = r，lM |= 0）（1）类似地，我们可以将归纳假设应用于（l，r），θ和θ，（r，l θ）π πM（M |= r，l M |= 0）（2）析取（1）和（2）导致4种情况：在Γ，lθ Θ和Γ，lθ Θ成立的情况下，应用分裂规则，我们得到ΓθΘ。在所有其他情况下，我们使用从归纳假设获得的模型之情形2 Δ = Δ J，C.我们对赋值Γ是否有共字面量进行了格区分梭情形2.1 Γ C =。我们对子句C的基数作了进一步的区分。情况2.1.1 C = C。它的表面是显示wr（ΔJ，λ）<$Θ。这是根据冲突规则得出的。情况2.1.2 C ={1}。如果l∈Γ，则可以通过应用（以向后的方式）红色规则遵循冲突规则。如果l∈/Γ，则我们使用归纳法，用（r，l），ΔJ∈Θ，θ. 这是因为，μ（（r，1）;Δlist cla=>valu=>(listcla=>listcla=>valu=>algsuccess）=>algsuccess）cs3 cbase cstep）A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243251► ∅我们在提取的程序中看到的第一件事是一个常数cgRec，它表示受保护的递归。后者对应于以下定义：（GRecGuardρ1ρ2ρ3τ）μ z1z2z3Gt=fz1z2z3t其中f：ρ1<$ρ2<$ρ3<$Boole<$τfx1x2x3True =G x1x2x3（[y1，y2，y3].f y1y2y3（μ y1y2y3<μx1x2x3））fx1x2x3假= Inhab5类似地，可以使用函数来编写操作Reclist ρρτf：列出ρττ，它给出了其行为的更直观的视图(Rec列表ρ（τ）ys z G=fys其中fNil =zf（x：：xs）=Gx xs（f xs）6提取程序的执行我们已经提取了两个程序，一个来自上面的证明（求解器），另一个来自涉及nc量化器的证明（求解器）。 nc-量化器被插入到主证明中的关键位置，即归纳定义和主证明之外的引理中。接下来，我们将看到，当它们被应用于许多SAT问题时，可编程和可编程求解器的提取的决策过程在鸽子洞原理的几个实例上运行[11]。鸽子洞原理指出，不存在映射{1，2...，n}到{1，2，...，n− 1}。定义6.1【鸽子洞公式】PHP（n，m）：={{li，1，.，li，m}| 1 ≤ i ≤ n}{{li，k，lj，k}|1 ≤ i list cla=>valu=>（list cla=>listcla=>valu=>algsuccess）=>algsuccess）cs3 cbase cstep）cgRec =[（listcla=>list cla=>valu=>（list cla=>listcla=>valu=>algsuccess）=>algsuccess）_0，cs1，cs2，val3](list cla=>list cla=>valu=>（list cla=>list cla=>valu=>algsuccess）=>algsuccess）_0cs102 - 03- 02[cs4、cs5、val6]（GRecGuardlist cla list cla valuealgsuccess）（[cs7、cs8、val9]Lh（toLit cs7）+Lh（toLit cs8）+Lh（setminus（varSetClaList（cs7++cs8））（varv val9）））cs4cs5val6(listcla=>list cla=>valu=>（list cla=>list cla=>valu=>algsuccess）=>algsuccess）_0（Lh（toLit cs4）+Lh（toLit cs5）+Lh（setminus（varSetClaList（cs4++cs5））（varvval6））Lh（toLit cs1）+Lh（toLitcs2）+Lh（setminus（varSetClaList（cs1++cs2））（varv val3））cbase =[cs0，val1，（list cla=>listcla=>valu=>algsuccess）_2][if cs0（cModelCaseval1）（[c3，cs4]cSplitCase cs0 val1 c3 cs4（list cla=>list cla=>valu=>algsuccess）_2）]cstep =[c0，cs1，（list cla=>valu=>（list cla=>list cla=>valu=>algsuccess）=>algsuccess）_2，cs3，val4，（list cla=>list cla=>valu=>algsuccess）_5][if（vcIntersection val4 c0=（Nillit））[ifc0（[ls6][如果ls6（cancel case cs1 cs3val4）[l7，ls8][如果ls8[if（memlv（相反l7）val4）（清楚地说明情况l7 cs1 cs3 val4）（cUnitCase l7 c0 ls6 ls8 cs1 cs3 val4（list cla=>listcla=>valu=>algsuccess）_5）]（[l9，ls10][if（cindmemlem（l7：：l9：：ls10）val4）（cReduceCase cs1 c0 cs3 val4 ls6 l7 ls8 l9 ls10（listcla=>list cla=>valu=>algsuccess）_5）（cCleanCase cs1 c0 cs3 val4 ls6 l7 ls8 l9 ls10（listcla=>valu=>（list cla=>listcla=>valu=>algsuccess）=>algsuccess）_2（list cla=>listcla=>valu=>algsuccess）_5）]）]）]）]（cElimCase c0 cs1 cs3 val4（list cla=>list cla=>valu=>algsuccess）_5）]csuccessCase = [cs0，cs1，val2]csuccessZero cderivableZero256A. Lawrence等人/Electronic Notes in Theoretical Computer Science 286（2012）243cElimentary案例=[l0，cs1，cs2，val3]csuccessZero（cderivableThree（CC l0：）（相反l0）cderivableZero单位箱=[l0，c1，ls2，ls3，cs4，cs5，val6，（list cla=>list cla=>valu=>algsuccess）_7][if（（listcla=>list cla=>valu=>algsuccess）_7（remccl（CC 10：）cs4++remccl（CC 10：）cs5）（Nil cla）（conclv 10 val6））（[algderivable8]csuccessZero（cderivableTwo l0algderivable8））csuccessOne]cReduceCase =[cs0，c1，cs2，val3，ls4，l5，ls6，l7，ls8，（list cla=>listcla=>valu=>algsuccess）_9，l10][if（（list cla=>listcla=>valu=>algsuccess）_9([if（l10=l5）（CC（l7：：ls8））（结论l5[if（l10=l7）(CCls8）（结论17（结论110（结论18）]）]：：remccl（CC（l5：：l7：：ls8））cs0）CS2Val3）（[algderivable11]csuccessZero（cderivableThree（CC（l5：：l7：：ls8））（相反l10）algderivable11））csuccessOne]cCleanCase =[cs0，c1，cs2，val3，ls4，l5，ls6，l7，ls8，（list cla=>valu=>（listcla=>listcla=>valu=>algsuccess）=>algsuccess）_9，（list cla=>listcla=>valu=>algsuccess）_10][if（（list cla =>valu=>（listcla=>listcla=>valu=>algsuccess）=>algsuccess）_9（CC（l5：：l7：：ls8）：：cs2）val3（list cla=>list cla=>valu=>algsuccess）_10）（[algderivable11]csuccessZero（cderivableLemma（CF（cs0++（CC（l5：：l7：：ls8）：：cs2）algderivable11））csuccessOne]cElimCase =[c0，cs1，cs2，val3，（list cla=>list cla=>valu=>algsuccess）_4][if（（listcla=>list cl

下载后可阅读完整内容，剩余1页未读，立即下载