广义概率满足性问题的理论计算及在线获取解决方法

可在www.sciencedirect.com在线获取理论计算机科学电子笔记332（2017）39-56www.elsevier.com/locate/entcs广义概率满足性1卡洛斯·卡尔德龙a菲利普·卡萨尔b安德烈亚·莫尔迪多aaSQIG-InstitutodeTelecomunicaQuarterooesDEP. 葡萄牙Lisboa大学数学研究所b伙伴关系、应用和技术合作中心（CMAF-CIO）DEP. 葡萄牙Lisboa大学数学研究所摘要我们分析了一个广义概率满足性问题（GenPSAT），该问题包括确定涉及经典命题公式概率的线性不等式的满足性。证明了GenPSAT是NP-完全的，并给出了混合规划的多项式约简。 利用这种翻译，我们实现和测试的GenPSAT问题的求解器。正如以前观察到的许多其他NP完全问题，我们能够检测到GenPSAT的相变行为。关键词：概率满足性，GenPSAT，混合规划，相变1介绍多年来，命题逻辑（SAT）的可满足性问题已经被广泛地研究，无论是出于理论目的，如复杂性理论，还是出于实践目的。尽管它的NP-完全性[9]，解决SAT的现代工具能够以非常有效的方式处理非常大的问题，应用于许多不同的领域和行业[2]。自然地，人们开始将这个问题扩展到更有表现力的框架：例如，在可满足性模理论[10]中，人们可以尝试决定一个公式在某些特定的一阶理论中是否有效，而不是在命题逻辑中工作。另一个方向是用概率扩展命题逻辑。概率满足问题（PSAT）最初是由乔治·1在研发部门50008的范围内完成的工作，由适用的财务框架资助（FCT/MEC通过国家基金，适用时由FEDER-PT 2020共同资助由FundaundaAM得 到了 FCT在 SFRH/BD/77648/2011 号 赠款 下的 支 持， 并 得到 了Calouste Gulbenkian 基 金会 在2011 年ProgramadeEst'ımulo`aInvestigacaBundo 下 的 支 持 。FC 感 谢 DP-PMI 和 FCT （ 葡 萄 牙 ） 通 过 奖 学 金SRFH/BD/52243/2013提供的支持。CC感谢欧盟FP 7 Marie Curie PIRSES-GA-2012-318986项目GeTFun的支持：概括真理功能。http://dx.doi.org/10.1016/j.entcs.2017.04.0041571-0661/© 2017作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。40C. Calcium et al./理论计算机科学电子笔记332（2017）39[18][19]这个问题在于决定命题公式的一组概率赋值的可满足性。在分析概率满足性问题和开发自动处理这一问题的有效工具方面，已经有了很大的成就[11，14，6，1，12]。在本文中，我们研究了广义概率可满足性问题（GenPSAT），通过允许值的概率分配到命题公式的线性组合来扩展PSAT的范围，并且在分析密码协议的安全性和估计攻击存在的概率方面有应用[17]。直观地说，GenPSAT包括决定存在的概率分布满足一组经典的命题公式与概率1，和一组线性不等式涉及概率的命题公式。GenPSAT问题先前在[13]中的概率逻辑的可满足性的背景下被识别，其中还显示是NP完全的。在这里，我们探索了这个问题的计算行为，并提出了一个多项式减少从GenPSAT混合编程，遵循[6，1]的线路。混合规划（MIP）[19]是一个框架，用于在实数上为一组线性约束的线性目标函数找到最优解。整型变量 我们将利用SAT和MIP之间的密切关系[4]，以便将GenPSAT问题简化为合适的MIP问题。正如在许多NP完全问题[7]中所观察到的，GenPSAT也呈现出相变行为。通过求解一批参数化的随机GenPSAT问题，我们观察到存在一个阈值，该阈值将几乎每个GenPSAT问题都满意的阶段和几乎每个GenPSAT问题都不满意的阶段分开在这种转变中，问题变得更加难以解决[7]。作为这项工作的主要贡献，我们开发的理论框架，允许GenPSAT和MIP问题之间的翻译，然后允许GenPSAT的可证明正确的求解器的实施。这种翻译能够将严格的不等式和不等式编码到MIP上下文中。有了GenPSAT解算器，我们就能够检测和研究相变行为。本文概述如下：在第2节中，我们简要回顾了PSAT问题;在第3节中，我们仔细定义了GenPSAT问题，并建立了一些关于其复杂性的结果;第4节致力于找到从GenPSAT到MIP的多项式约简，并提供了一个自动分析问题的原型工具;在第5节中，我们分析了相变的存在;最后，在第6节中，我们评估了我们的贡献并讨论了未来的工作。C. Calcium et al./理论计算机科学电子笔记332（2017）3941P ={}常规公式。 我们说一组赋值V满足一个命题PV满足公式Pr（c）∞p，如果a子句，p∈Q，0≤p≤ 1且∞ ∈ {=，≤，≥}。 我们说概率分布π∑（（） ）∞iiV{（）∞ ≤联系我们在简单的概率公式中，证明了概率Satis-ii={Pr（c）∞p<$1≤i≤k}P⎨⎪∑i=在所有的∞i。对mula_（？），如果，对ea_c_h_v∈V，v（？）=1. 这一概念被扩展到集合的proposi-满足第i个子句，p=[pi]是所有pi的k向量，∞=[∞i]是k向量π∞p2预赛让我们首先固定一组命题变量x1，...，x n. 字面量是命题变量或其否定。子句是一个或多个文字的非空析取。命题公式是命题变量的任何布尔组合。命题赋值是映射v∶ P → {0， 1}，本文将它推广到命题赋值.像往常一样，为穆拉斯。设V={v1， . ，v2n}是定义的所有值的集合的变量。我们将π上的概率分布定义为向量大小2n.一个简单的概率公式是Pr（c）∞p形式的表达式，其中c是2Nv c π p。i=1概率分布π满足一组简单的概率公式，如果它满足其中的每一个。我们现在回顾PSAT问题[18，14，11]。定义2.1[PSAT问题]给定一组命题变量和一组稳定性问题（PSAT）在于确定是否存在满足π的概率分布πPrcipi1i k的 PSAT问题可以用代数公式表示为寻找不等式组的解π的问题π1，⎪⎩π≥0其中V是k × 2 n矩阵，使得V ij= v j（c i），即， V ij= 1 i第j次估值SAT问题可以被建模为PSAT实例，其中概率向量的条目pi都等于1。PSAT问题被证明是NP完全的[14，13]，即使子句仅由两个文字2-PSAT的析取组成。42C. Calcium et al./理论计算机科学电子笔记332（2017）39∈Pii=1在rel=1，a=1的情形下，得到了一个简单的概率公式. An1我关系符号为≤、>、=的公式可以通过缩写得到。（）≤（）（）下一页V（）（）下一页联系我们（）={（）=∈}（）下一页i=1j=13GenPSAT问题现在我们将简单概率公式的概念推广到处理涉及命题公式概率的线性不等式概率公式是以下形式的表达式：∑（aiPr（ci））∞p，其中c i是命题分句，∞ ∈ {≥，<}，l∈N和a1，.，al，p∈Q. 观察原子概率公式是这样的概率公式，其中每个C i是一个命题变量，即，c 对于每个i。我们知道，概率分布π满足对于a∑l=1（aiPr（ci））∞p，如果l 2∑∞p.概率分布π满足一组概率公式，如果它满足其中的每一个GenPSAT的一个实例是一对Γ， Γ，其中Γ是一组命题子句（也称为硬约束），并且Γ是一组概率公式（软约束）。我们说概率分布π满足GenPSAT实例Γ，如果它满足概率公式r，（一）定义3.1 [GenPSAT问题]给定一个GenPSAT实例Γ，π，广义概率可满足性问题（GenPSAT）在于确定是否存在满足Γ，π的概率分布π。GenPSAT提出了一个方便的框架，用于指定涉及不同概率公式的约束。例如，人们可能希望强加2 PrAPrB两个命题分句A，B这些要求可能是在指定感兴趣的系统的属性时非常有用，但它们不能在PSAT框架中容易地我们现在通过编码Monty Hall问题来展示GenPSAT例3.2蒙提·霍尔问题是一个难题，我们面临着从三扇门中选择一扇门，知道奖品在其中一扇门后面。在我们最初的选择之后，游戏主持人打开剩下的一扇门，前提是奖品不在它后面，并让我们选择切换或保持最初的猜测。问题是：哪种选择更有利？为了将这个问题建模为GenPSAT实例，让我们定义以下比例变量：如果奖品在门i后面，则Pi成立;如果我们的初始选择是门i，则Xi成立;如果主机在我们的初始选择之后显示门i，则Hi成立，对于i1， 2， 3。由于只有一个门与奖品，一个初步的选择，和一个门透露LC. Calcium et al./理论计算机科学电子笔记332（2017）3943→ <$→ <$∈{}19981998（）≥（）通过切换获胜是通过检查实例（Γ，Pr（WbS）））是正如预期的那样，该实例是不满意的，并且实例（Γ，Pr（WbS）≥◊（）（）下一页3（+）× =[]∈{+33使用我们实现的工具检查实例[8]。改变我们最初的选择由主办方，我们施加以下限制：r=（Pi<$Pj<$Pk），（Xi<$Xj<$Xk），（Hi<$Hj<$Hk）。i，j，k∈{1，2，3}i，j，k∈{1，2，3}i，j，k∈{1，2，3}⎩伊什吉·克鲁吉伊什吉·克鲁吉我的朋友此外，主人既不能打开所选的门，也不能打开有奖品的门，因此我们在Γ中包括以下约束P iH i和X iH i，对于每个i 1，2，3。我们进一步假设奖品在每扇门后面的概率是一致的，并且最初的选择与奖品在哪里无关n=n{Pr（P）=1，Pr（P我（X）=1Pr（X）}i，j∈{1，2，3}3i j3j关于切换和保持我们最初的选择哪个更有利的问题，我们将切换获胜编码为WbS：并通过保持3Pi=1-（<$XiHi）），WbK：3Pi=1-X i）。我们想决定是否总是Pr WbS Pr WbK的情况，这可以通过测试GenPSAT实例（r，n ={Pr（WbS） 0。设W是从V通过选择前k行（cor-k）构造的矩阵。响应于表1中的概率公式）和最后一行（要求lution. 再次利用引理3.3，我们得到存在一个（k+1）×k矩阵W，其中k≤k+1，n是有正解ρ的方程组. 解π（5）反过来，假设存在一个秩为kk1的k1k矩阵W满足（i），（ii），（iii），并设π表示（5）的解 我们在寻找概率分布π满足Γ，为此，设0vj1，.， v jk表示根据条件（ii）的W的估值集合，并定义π=[πi]，其中π=ππi 如果i∈{j1， . ，jk′}。我也不知道π满足GenPSAT实例的验证现在是即时的：● 给定γ∈Γ，我们通过观察最后一个等式，证明π∈V使P′r（γ）=2nk′∑vj（γ） <$πj= ∑πj=∑πjs=1。j=1{j<$vj（γ）=1}s=1● 给出一个关于∑l=1aiPr（yi）∞p的概率分布，我们回忆一下定义：π是（5）的解，从而得出结论：l2nlk ′k′ l∗∑ai<$∑vj（yi） <$πj<$$>=∑ai<$∑vjs（yi） <$π js <$$>=∑（∑ai<$vjs（yi））πjs∞p，C. Calcium et al./理论计算机科学电子笔记332（2017）3947也就是说， π满足π中◻48C. Calcium et al./理论计算机科学电子笔记332（2017）39和m，我们的目标是现在描述一个编码问题的过程，（） =VcP列表示V0中的值，该值根据以下比例变量进行评估：=（ ）≤=[]×∑h∑=j=1=-当h=1时，即，IJ≤ ≤ − + ≤≤克r′=1Iss=1W我我×′或者是关系符号≥，或者是，我们可以很容易地编码第一种<∑（）∞∞∑≥ii≥∑πj=1。（总数1）∞<对于每个赋值1≤j≤k，我们生成一个线性不等式，r=1s=1∑h ir，j）+ ≥ 1。（伽玛）约束，即当verhij为0时，迫使bij为零，并确保bijπj4.2翻译成MIP关于引理4.1，给定标准形式的GenPSAT实例r，在条件（i），（ii），（iii）中找到一组估值0和概率分布π，作为MIP问题。我们称之为GenToMIP。让我们用Hhij表示大小为n k′的（仍然未知的）矩阵，，也就是， hijv jx i对于每个1 in和1 jk。设α1，...，α n表示命题变量x1，.的概率，x n，且在[6，1]的推理中，我们建立了非线性约束不等式k′k′j=1ijπj=αi 为线性bijαi，（val1）通过引入受到适当约束额外变量bij，0bijhij和hij1πjbijπj。（val2）我们通过施加以下条件来确保π表示概率分布：尽管如此，由于V0j=1satisfiesΓ，givenaclause（southxir） n （w′<$x′）of（中文）注意，如果我们在Γ中总共有m个子句，我们生成m k个这样的不等式。为了验证MIP帧- w中概率公式的满足性，考虑在MIP中对于mulal=1aiPryip的一个随机概率。既然能不等式作为MIP线性约束，但在处理其余关系符号时应小心。对于形式为∑l=1aiPr（yi）≥p的模型的概率问题，我们给出了线性不等式La α p。 （概率）i=1C. Calcium et al./理论计算机科学电子笔记332（2017）3949在严格不等式的情况下，我们使用一个特定的变量引入MIP问题，比如ε，将目标函数固定为ε的最大化，maximizeε（obj）50C. Calcium et al./理论计算机科学电子笔记332（2017）39Li=1我∑（）− ii=∑（） −ii∑（） −>ii当n=1时，不等式y（6）成立，若i=1，则y（6）成立● n约束（val1），● 1个约束（sums1），到目前为止，我们已经介绍了：● k≥约束（概率），≥×≠≠′≥V（）（）∑（ai <$α i）− p≤′≤≤ ≤（）下一页bij=hijρj，{v， . ，v′}和ρ=[ρ]表示一个值集和一个概率分布（）V =minΔ，通过GenToMIP获得的MIP问题的可行性与最优值ε0（如适用）。算法1给出了一个GenPSAT实例，将其转换为MIP问题，然后适当地解决后者。为此，让我们假设我们初始化一个空的MIP问题，并考虑以下辅助过程：add const将线性约束引入MIP问题，set obj定义了目标函数（作为最大化或最小化），而之前没有定义，fresh在MIP问题中声明了一个新的二进制变量mip sat根据问题是否可行（并获得最优解）返回True或False，● mipobjvalue返回目标函数设置时的目标值。命题4.3一个标准形式的GenPSAT实例，如果RtA 1-租m 1返回Sat，则它是满足的。证据 设Γ， Γ是标准形式的满足的GenPSAT实例，并且0由引理4.1给出，满足条件（i）-（iii）。然后，考虑以下值，然后让我们检查它们是否构成在算法1处构造的MIP问题的最优解：对于每个1 i n和1jk，令hij=vj（xi），πj=ρj，αi={∑ρj，=j<$vj（xi）=1}●●●●ε∗C. Calcium et al./理论计算机科学电子笔记332（2017）3953我ij1，...，n，j1，...，K8：对于i=1到n，[]∈{}∈{}5：对于j=′1至k，6：对于在rdorsrs中的each（nx） n（nx）30：如果 mip sat（）然后13：辅助←0=（）>19：辅助←123：辅助←116：情况25：C←1+q+∑ai21：add const（∑a<$α+ε≤q）<$（prob）ii<29：add const（∑π=1）<$（sums1）i15：开关（∞）18：case<11：add const（0≤b≤h）<$（val2）ijij27：add const（∑a<$α−C<$z−ε≥q−C）<$$>（prob）ii<$2：声明：二元变量：hfori∈{}∈{}9：add const（∑j′bij=αi）<$（val1）其中Δ={q−∑l=1（ai<$αi<$）<$（∑l=1aiPr（xi）q）∈<$}<$<<${C<$z<$$>+q−∑l=1（ai<$αi<$）<$$>∈<$具有形式∑l=1aiPr（xi）<$q}<$我我并且，对于形式为∑l=1aiPr（xi）<$q的mu∈M的e个半概率，我我我我我算法1基于MIP的GenPSAT1：proCUBERGENPSAT（props{xi}n=1，formr，probformr）′3：0，1-变量：αi，πj，bij，i1， . ，n， j1，. ， K4：实变量：ε7：add const（∑rhrj+∑s（1−hsj）≥1）<$（gamma）10：对于j=1至k，12：addconst（hij−1+πj≤bij≤πj）<$（val2）14：对于每个∑ai<$Pr（xi）∞q，17：add const（∑ai<$αi≥q）<$（prob≥）20：设置obj（maxε）（obj）22：情况24：z←fresh（）z是一个新鲜的二进制变量26：设置obj（maxε）（obj）28：add const（∑ai<$αi−C<$z+ε≤q）<$$>（prob<$）31：if（aux0）or（aux1 andmip objvalue0）then32：返回Sat33：返回Unsat<${C−C<$z<$$> −q+∑l=1（ai<$αi<$）<$$> ∈<$具有形式∑l=1aiPr（xi）<$q}，如果∑l=1ai<$αi<$q，ϕ我′54C. Calcium et al./理论计算机科学电子笔记332（2017）39我如果∑l=1ai<$αi<$>q，则为1z.C. Calcium et al./理论计算机科学电子笔记332（2017）3955{}∈如果h = 0，则b因为π≤ 1，所以π− 1 ≤b≤π，即，ijij我（（）∞ ）∈我（2）（ ）≥ ）∈≥=对前一个，我们可以得出结论：∑la<$α<$（val 1）通过{bij}和{hij}的定义，我们实际上已经（val2）Si nce 0 ≤vj（xi）≤1 and0 ≤ρj≤1 w e i mm e d i atelyhave 0≤bij≤hij.● 如果hij=1 th e nbij=πj，因此πj≤bij≤πj，即，h<$ij−1+πj<$$> ≤b<$ij≤πj<$i=1i=1{j≠vj（xi）=1}i=1j=1I1我J1J我JI1我我∑（ai<$αi<$） +ε<$≤∑（ai<$αi<$） +q−∑（ai<$αi<$）=q。我我对f的模，我们有∑l=1（ai<$αi<$）<$q，在其它情况下，q−∑l=1（ai<$αi<$）>0我z的定义，并注意到L∗我LL我我我现在让我们检查一下，在算法1中引入MIP问题的每个线性约束都得到了满足。（γ）hij满足模型的约束条件，因为ea chvV0满足Γ。k′k′k′∑bij=∑hij<$ρj=∑vj（xi） <$ρj=∑ρj=αi .j=1j=1j=1{j<$vj（xi）=1}●对于另一个不等于y的情况，回想hij=vj（xi）处的h和htπj=ρj，并注意：h<$ij−1+πj<$$> ≤b<$ij≤πj<$（sums1）Si nc e π=ρ，我们立即得出∑k′π=1.Jjj=1 J为了检查概率公式是否满足，只需注意，给定一个对于mula∑l=1aiPrxiqi，∗⎛ ⎞l⎛2n⎞∑ai=∑ai。（prob）设l1aiPrxi q，注意，由于ρ满足条件（i），（ii），（iii），特别是它满足所有的概率公式，因此∑l=a（∑2=n v（x） <$ρ）≥q，则∑l=a<$α<$≥q.（prob<）Now，let（∑l=1aiPr（xi）q）∈N，注意，在一个推理中，0。（七）但我们也应该注意到，由于ε=minΔ，则ε≤q−∑l=1（ai<$αi<$），并且我们得到l l li=1i=1i=1最后，让我们考虑以下形式的或q−∑l=1（ai<$αi<$）<<$0。回想一下常数C定义为sC=1+q+∑l=1ai，和C<$z<$$>+q−∑（ai<$αi<$）>0（ 8）L56C. Calcium et al./理论计算机科学电子笔记332（2017）39C C z q a α 0（9）i=1C. Calcium et al./理论计算机科学电子笔记332（2017）3957ε≤C<$z<$+q−∑l （a<$α<$）且ε<$≤C−C<$z<$−q+∑l （aα）。因此，我们现在没有了11岁的孩子>（）=我=我=1≤i≤n，1≤j≤k考虑va表示的集合V0={v1， . ，vk′}，其中，对于每个ch，=[ ]= ≤ ≤′=-C =0（）=的∑（ai<$αi<$ ） −C<$z<$$> −ε<$≥∑（ai<$αi<$） −C+C<$z<$$>+q−∑（ai<$αi<$）=q−C，∑（ai<$αi<$） −C<$z<$$>+ε<$≤∑（ai<$αi<$） +C<$z<$$>+q−∑（ai<$αi<$）=q。∑（ai<$αi<$ ） −C<$z<$$> −ε<$≥∑（ai<$αi<$ ） −C−（C−C<$z<$$> −q+∑（ai<$αi<$））=q−C，∑（ai<$αi<$） −C<$z<$$>+ε<$≤∑（ai<$αi<$） −C+C<$z<$$>+q−∑（ai<$αi<$）=q。反过来，假设算法1返回Sat，让我们用hij表示，在2n向量πρj上，其中ρj πj 对于1 jk线性约束（prob≥）、（prob<）、（prob）和（sums1），通过定义矩阵引理4.1中描述的第三个条件是通过简单检查在上述任何一种情况下都是可以验证的 还应注意，通过定义ε，我我分析之前的每一个案例：● 如果q∑l=1aiαi ，然后，l l lI1而且，Li=1Li=1Li=1i=1i=1● 如果q∑l=1（aiαi），则nz∑l=1，且l l lI1而且，Li=1Li=1Li=1i=1i=1为了完成直接含义，请注意ε>0作为（7）、（8）和（9）的结果，（9），它取最大可能值，因为否则，让ΔΔ是公式在Δ中具有最小值的单位为Δ。 那么，如果有一个解决方案，如果是客观值，则它将违反对ΔΔ的约束（概率）。∗αi，ε和πjthe′（最优）解分别为变量h i j，α i，ε和π j，for e a c h.变量xi，vj xi hij。由于限制（伽马），可以立即得出结论，每个估值满足Γ。然后，让概率分布π定义为当k j ≤ 2 n时，ρj=0<。 注意that（sums1）意味着π是一个概率向量。并且回想最优值ε使得ε>0。◻作为前面命题的推论，我们得到下列结果。定理4.4GenToMIP算法是GenPSAT到GenToMIP算法的正确翻译多项式大小的MIP问题。5相变相变是一种现象，标志着在解决问题的实例中的硬度变化。这种行为在许多NP完全问题中观察到[7]，其中我们强调3-SAT[16]和PSAT[11，12]。在本节中，我们通过算法1的实现和由随机实例电池组成的测试来研究GenPSAT为58C. Calcium et al./理论计算机科学电子笔记332（2017）39//=-/=-我们衡量满意实例的比例以及求解器解决它们所花费的平均时间。该软件是用Java编写的，我们使用Guidance[15]，版本6.5.0来解决MIP问题。用于测试的机器是一台Mac Pro，3，33 GHz 6核Intel Xeon，6 GB内存。我们的实现在[8]中可用。有人指出，在随机3-SAT实例中[16]，有一个明确的阶段，其中实例几乎肯定是满意的，而另一个阶段则几乎肯定是不满意的。这种现象的特征在于比率m n存在一个阈值，其中m是子句的数量，n是变量的数量，对于其中：对于较小的比率值，SAT实例几乎肯定是令人满意的，并且很容易解决，而具有较大比率值的实例几乎肯定是不令人满意的，并且也很容易解决。然而，由于比率的值非常接近这个阈值，平均而言，这些实例非常难以解决，并且无法确定问题是否令人满意。正如我们已经注意到的，任何3-SAT问题都可以被视为GenPSAT实例。我们测试了我们的GenPSAT求解器与3- SAT的随机实例，并观察到，相变发生时的比率m n约为4。[16]见图1。图1被视为GenPSAT实例的SAT的相变，其中n= 20。对概率满足性问题PSAT[11，12]的更深入分析表明，对于比率m n，PSAT存在相变行为，其中m是子句的数量，n是变量的数量。我们测试了随机PSAT实例的概率公式k2，n15和m的数量从1到105的步骤2。对于每个m值，我们生成100个PSAT实例。所得结果见图2。我们强调，分析k上变化（而不是m上变化）的相变的存在性对于深入理解概率满足性问题的相变（而不是概率公式存在时命题公式的满足性问题的相变）是必不可少的。为此，我们测试了随机PSAT实例，其中n为30，m为40，k为1至25，并且还观察到相变