基于展开的QBF求解器的等价依赖集表示

理论计算机科学电子笔记251（2009）83-95www.elsevier.com/locate/entcs的等价依赖集表示基于展开的QBF求解器Florian Lonsing和Armin Biere1形式模型与验证研究所奥地利林茨摘要给定一个前束合取范式（PCNF）的量化布尔公式（QBF），考虑变量依赖的识别问题.在相关的工作中，依赖关系的正式定义已经基于quantier prefix重新排序提出：如果将两个变量在Prefix不会改变公式的可满足性。而不是一般的情况下，我们专注于依赖存在变量的所有通用变量的集合。这对于基于扩展的QBF解算器尤其相关。我们提出了一种有效地计算存在依赖集的方法，通过变量上的有向连接关系，并演示了如何使用union-find数据结构将这种关系复杂地表示为树实验结果表明了该方法的有效性关键词：量化布尔公式，QBF，扩展，依赖。1引言量化布尔公式逻辑（QBF）扩展了具有泛量化的命题逻辑（SAT）。虽然QBF并不比SAT更有表现力，但模型检查和验证的相关问题[6，8，13，19]通常可以在QBF中编码得比SAT更复杂。在SAT领域，在过去几年中，在基于DPLL框架的有效决策程序的开发方面取得了令人鼓舞的进展[12]。成功是由于先进的策略修剪搜索空间，如学习，跳回或重新启动。这些技术被成功地扩展到QBF的基于DPLL的算法[11，17，26]，但是，尽管对性能仍然很重要，但事实证明并不能保证与SAT类似的进展第1http://fmv.jku.at/1571-0661 © 2009 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.08.02984F. Lonsing，A.Biere/Electronic Notes in Theoretical Computer Science 251（2009）83¬∈¬≡有强有力的迹象[4，14，15，18]表明，前束合取范式（PCNF）中QBF的量化前缀可能是这种现象的一个原因。 在QBF中，不同类型的量化器的存在引入了变量之间的依赖关系，QBF求解器必须遵守这些依赖关系。在许多情况下，线性量化器前缀导致的依赖性过于悲观，对求解器性能有负面影响。在[23]中，已经提出了依赖关系的正式定义，并且表明识别最佳（最小）依赖集的问题与QBF的决策问题一样，是PSPACE完全的[24]。 由于这一事实，必须在效率和最优性之间找到一种折衷。已经提出了各种方法来识别依赖关系，从而克服线性量化器前缀的缺点[2，4，7，9，15，18，20，23]。据我们所知，所有这些方法都是基于分析的句法结构的QBF。除了基于搜索的QBF求解器，其在探索搜索空间的不相关部分时依赖于依赖性，处理依赖性对于基于变量消除的求解器至关重要[2，5，7，10，20]。这些求解器必须处理涉及消除的公式的依赖性相关的大小增加在本文中，我们解决了在PCNF中计算QBF的通用量化变量的依赖集的问题，这与基于扩展的QBF求解器相关[2，5，7，10，20]。我们的工作是基于[7，9]。本文简要介绍了泛展开式，并分析了文[9]中提出的计算依赖关系的算法通用变量。从我们的分析开始，我们在普适扩展的背景下开发了依赖性的正式定义。该定义基于变量的句法连接关系。我们通过定义存在变量上的等价关系来获得有向依赖关系。这种关系可以表示为一棵树，不包括传递边。作为实验结果demonstrate，这种关系允许在QBF中的所有泛变量的依赖集的高效计算。由于我们不考虑存在变量的依赖关系，因此我们的方法不能直接应用于基于搜索的求解器，但我们看到了将我们的工作扩展到存在变量的依赖集22个房间对于一组变量V，文字是变量x V或其否定x，其中v（x）=x和v（x）=x表示文字的变量。 子句是对文字的析取。一个命题公式是合取范式（CNF），如果它由子句上的合取词一个量化的布尔公式（QBF）F S1.前束合取正规形式（PCNF）中的Snφ由一组变量V上的CNF中的命题公式φ和一个量化前缀S1.组成。S n.量化器前缀是作用域Si的线性有序集合，使得S1<。. .& lt;S n，它在变量集上形成一个分区：V= S1... 当1≤i，j≤n且ij时，S n和Si <$S j= /0。[21]事实上，我们已经扩展了我们的方法。我们得到了存在变量和泛变量依赖关系的一个紧图表示。这种表示也基于语法变量连接[23]。F. Lonsing，A.Biere/Electronic Notes in Theoretical Computer Science 251（2009）8385qSqSii\||⊆ ⊆×⊆×{∈|联系我们⊆×产品名称：∀ ∃ ∨ ¬ ∧ ¬ ∨一个作用域Si是存在的，如果它与一个存在量化器相关联，写为（）=，否则是全称的，其中（ ）=的 . 存在变量和泛变量的集合分别表示为V= Si（对于q（Si）=）和V= Si（对于q（Si）=）。 F或变量x∈Si，s（x）=Si是x的scope，q（x）= q（s（x））是x的型. 对于两个相邻的作用域Si和Si+1，其中1≤i n，q（Si）q（Si+1）. 给定一个有n个作用域的QBF，有n-1个量化器交替。对于某个变量x，R（x）= yVδ（x）δ（y）。 也就是说，R（x）是所有大于x的变量的集合。对于作用域Si和文字l，δ（Si）=i和δ（l）=δ（s（v（l）分别表示Si和l的水平。 对于作用域Si，Sj和文字l，k，Sj大于Si，k大于l，分别有δ（Si）<δ（Sj）和δ（l）<δ（k）.设R V V是变量集V上的二元关系。R的自反传递闭包是最小的自反传递闭包RJVV，使得RRJ。R的自反传递约简是使R和RJ具有相同的自反传递闭包的最小RjVV在下文中，考虑PCNF中的QBF，使得对于所有子句C=（11.... . . 你 好 。 .lk），v（li）=v（lj）和δ（li）δ（lj），对于1I

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