首页/论文/1502.02484

arXiv 1502.024842015-02cs.LO

基于子句组求解器API的QBF最小不可满足核的增量计算

Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API

Florian Lonsing, Uwe Egly

备注：: (fixed typo), camera-ready version, 6-page tool paper, to appear in proceedings of SAT 2015, LNCS, Springer
DOI：: 10.1007/978-3-319-24318-4_14

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

我们考虑QBF的最小不可满足核（MUC）的增量计算。为此，我们为增量QBF求解器DepQBF配备了一个新的API，以允许基于子句组的增量求解。子句组是一组子句，这些子句被递增地添加到先前求解的QBF中或从先前求解的QBF中移除。我们的新API的实现与基于选择器变量和假设的增量SAT求解有关。然而，API完全隐藏了用户的选择器变量和假设，这有利于DepQBF在其他工具中的集成。我们目前的实施细节，并首次报告相关的实验使用DepQBF的新条款组API的QBF的MUCs的计算。

英文摘要：

We consider the incremental computation of minimal unsatisfiable cores (MUCs) of QBFs. To this end, we equipped our incremental QBF solver DepQBF with a novel API to allow for incremental solving based on clause groups. A clause group is a set of clauses which is incrementally added to or removed from a previously solved QBF. Our implementation of the novel API is related to incremental SAT solving based on selector variables and assumptions. However, the API entirely hides selector variables and assumptions from the user, which facilitates the integration of DepQBF in other tools. We present implementation details and, for the first time, report on experiments related to the computation of MUCs of QBFs using DepQBF's novel clause group API.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

子句比变量多三个的不可满足击中子句集

Unsatisfiable hitting clause-sets with three more clauses than variables

本文的主题是最小不可满足子句集（MU）的一致性猜想，指出对于每个固定的缺陷（子句数减去变量数），只有1000个模式，给出了一定的基本约简（广义单位子句传播）。我们把注意力集中在击中子句集（每两个子句至少有一个冲突），其中的猜想说，只有100多个同构类型。这里，已知连续性猜想对于至多亏数2成立，现在我们证明它对于亏数3成立。一个重要的工具是“（不可）约子句集”的概念：我们展示了如何减少一般问题的不可约的情况下，然后解决这种情况下（不足3）。这个概念来自数论（Korec 1984，Berger et al 1990），我们在研究中重新发现了它。

2016-04-05cs.DMcs.LOmath.CO

存在不可满足的线性k-CNFs，对于每个k

Unsatisfiable Linear k-CNFs Exist, for every k

我们称CNF公式为线性的，如果任何两个子句最多有一个公共变量。设线性k-SAT是判定给定的线性k-CNF公式是否可满足的问题。这里，k-CNF公式是每个子句的大小正好为k的CNF公式。已知当k >= 3时，线性k-SAT是NP-完全的当且仅当存在一个不可满足的线性k-CNF公式，并且当k >= 4时它们确实存在。我们证明了对每个k都存在不可满足的线性k-CNF公式。设f（k）是不可满足的线性k-CNF公式的最小子句数。我们证明了f（k）是Omega（k2^k）和O（4^k*k^4），即，最小尺寸不可满足线性k-CNF公式显著大于最小尺寸不可满足k-CNF公式。最后，我们证明，令人惊讶的是，线性k-CNF公式不允许一个更大的分数的条款得到满足比一般k-CNF公式。

2007-08-17cs.CCcs.DMcs.LO

一致性规划作为增量式QBF求解的实例研究

Conformant Planning as a Case Study of Incremental QBF Solving

Vienna University of Technology（维也纳工业大学）；University of Siegen（锡根大学）

我们考虑规划与初始状态的不确定性作为增量量化布尔公式（QBF）求解的案例研究。我们报告的实验工作流程，逐步编码规划实例到一个序列的QBF。为了解决这个增量构造的QBF序列，我们使用我们的通用增量QBF求解器DepQBF。由于生成的QBF有许多共同的条款和变量，我们的方法避免了冗余的编码阶段和求解阶段。实验结果表明，增量QBF求解优于非增量QBF求解。我们的研究结果是增量QBF解决规划的背景下，并激励其在其他应用领域的第一次实证研究。

2016-04-04cs.AIcs.LO

约束规划的不可满足核

Unsatisfiable Cores for Constraint Programming

National ICT Australia（澳大利亚国家信息与通信技术研究院）；University of Melbourne（墨尔本大学）

约束编程（CP）求解器通常通过反复寻找问题的解决方案来解决优化问题，同时对解决方案的成本设置越来越严格的界限。这种方法有些幼稚，特别是对于软约束优化问题，其中软约束大多得到满足。在布尔可满足性中解决软约束问题的不可满足核方法（例如MAXSAT）强制所有软约束保持初始状态。当求解失败时，它们返回一个不可满足的核心，作为一组不能同时保持的软约束。使用该信息，问题被放松以允许违反某些软约束，并且求解继续。由于懒惰子句生成（LCG）求解器也可以返回不可满足的核心，我们可以将MAXSAT不可满足的核心方法应用于CP。我们实现了原来的MAXSAT不可满足的核心求解算法WPM1，MSU3在一个国家的最先进的LCG求解器，并表明存在的问题，受益于这种混合的方法。

2013-05-08cs.AIcs.LO

最小不可满足性的参数：Smarandache本原数和全子句

Parameters for minimal unsatisfiability: Smarandache primitive numbers and full clauses

我们在命题逻辑和初等数论之间建立了一座新的桥梁。主要对象是“最小不可满足子句集”、短“MU”、通过消除任何子句而变得可满足的不可满足合取范式。换句话说，布尔超立方体的子立方体的无冗余覆盖。MU的主要参数是“亏数”k，即子句数与变量数之差（覆盖中元素数与超立方体维数之差），基本事实是k >= 1成立。MU中的“完整子句”包含所有变量（对应于覆盖中的单例）。我们证明了下界S_2（k）<= FCM（k），其中FCM（k）是亏数为k的MU中的最大满子句数，而S_2（k）是使得2^k整除n！的最小n。证明依赖于两种方法：在逻辑组合方面，应用包容解决方案及其逆，一个基本的方法，因为布尔在1854年介绍了“扩展方法”。在算术方面，分析某些递归，将特定于应用的递归与来自元斐波那契序列的递归（实际上S_2等于Conolly序列的两倍）相结合。另一个工具是考虑不可满足的“命中子句集”（UHIT），MU的特殊情况，对应于布尔超立方体的子立方体分区;它们也被称为正交或不相交的DNF重言式。我们实际上证明了更清晰的下界S_2（k）<= FCH（k），其中FCH（k）是亏数为k的UHIT中满子句的最大数目。我们猜想对所有k成立S_2（k）= FCH（k），这将在（不）可满足的极值组合学和初等数论之间建立一种令人惊讶的联系。我们应用该下界来分析MU和UHIT的结构。

2015-07-08cs.DMcs.LOmath.CO

约束规划的不可满足核与下界

Unsatisfiable Cores and Lower Bounding for Constraint Programming

National ICT Australia（澳大利亚国家信息与通信技术研究院）；University of Melbourne（墨尔本大学）

约束编程（CP）求解器通常通过反复寻找问题的解决方案来解决优化问题，同时对解决方案的成本设置越来越严格的界限。这种方法有些幼稚，特别是对于软约束优化问题，其中软约束大多得到满足。在SAT中解决软约束问题的不可满足核方法（例如MAXSAT）强制所有软约束最初都是硬约束。当求解失败时，它们返回一个不可满足的核心，作为一组不能同时保持的软约束。这些将恢复为软，求解将继续。由于惰性子句生成求解器也可以返回不可满足的核心，我们可以将这种方法应用于约束编程。我们适应原来的MAXSAT不可满足的核心求解方法，可用于约束编程和定义了一些扩展。实验结果表明，我们的方法是有益的CP优化基准涉及软约束，基数或偏好的广泛类。

2015-08-25cs.AIcs.LO

更多相关论文收起更多论文

基于子句证明优化的图裁剪

Trimming Graphs Using Clausal Proof Optimization

我们提出了一种方法，逐步计算一个越来越小的命题公式的不可满足的核心，最小化证明的不可满足性。目标是计算一个最小不可满足核，该核与相同公式的其他最小不可满足核相比相对较小。我们试图实现这一目标，推迟删除任意条款的公式，只要有可能-在现有的最小不可满足的核心算法。我们应用这种方法将色数为5的已知最小单位距离图从553个顶点和2720条边减少到529个顶点和2670条边。

2019-07-15cs.LOmath.CO

命题归结的完备性：一个简单的构造性命题<br>证明

The Completeness of Propositional Resolution: A Simple and Constructive<br> Proof

众所周知，归结方法（对于命题逻辑）是完备的。然而，在文献中发现的完备性证明使用了一个矛盾论证，表明如果一组子句是不可满足的，那么它必须有一个归结反驳。因此，这些证明实际上都没有给出一个从一组不可满足的子句中产生一个归结反驳的算法。本文给出了命题归结的完备性的一个简单的构造性证明，它包括一个算法和一个正确性证明。

2006-11-07cs.AIcs.LO

具有广义公理的Q-归结

Q-Resolution with Generalized Axioms

Q-resolution是一个基于前向合取范式（PCNF）的量化布尔公式（QBF）的证明系统，它是基于搜索的QBF求解器与子句和立方体学习（QCDCL）的基础。为了在搜索的早期获得和学习更强的子句和立方体，我们推广了Q-分辨率演算的公理，从而产生了一个指数级更强大的证明系统。广义公理将Q-解析引入到任何其他QBF证明系统的接口，允许直接组合正交求解技术。我们在QBF求解器DepQBF中实现了具有广义公理的Q-分辨率演算的变体。作为两个案例研究，我们在搜索过程中应用集成的SAT求解和资源受限的QBF预处理来精确地检测潜在的公理应用。应用程序基准测试的实验表明，显着的性能改善。

2016-04-22cs.LO

基于极小模型和不可满足核的ASP中的谨慎推理

Cautious reasoning in ASP via minimal models and unsatisfiable cores

回答集编程（ASP）是一个基于逻辑的知识表示框架，支持-在其他推理模式中-查询回答的中心任务。在命题的情况下，查询回答相当于在给定的候选集合中的原子之间计算输入程序的谨慎后果，其中谨慎后果是属于所有稳定模型的原子。目前，最有效的算法要么迭代地验证一个候选人的补充扩展的输入程序的稳定模型的存在，其中候选人被选择，或引入一个子句强制执行至少一个候选人的虚假性，使得求解器可以自由选择在稳定模型的计算期间的任何时间伪造哪个候选人。本文介绍了计算谨慎后果的新算法，目的是驱动求解器搜索稳定的模型，放弃更多的候选人。具体来说，这样的算法之一强制极小的集合上的真实的候选人，其中可以使用不同的概念的极小，和另一个利用不可满足的核心计算。该算法在WASP中实现，并在最新的ASP竞赛的基准测试上进行实验，结果表明新算法的性能优于现有技术。（正在考虑接受TPLP）。

2018-04-23cs.LO

SATformer: 基于Transformer的UNSAT核心学习

SATformer: Transformer-Based UNSAT Core Learning

The Chinese University of Hong Kong（香港中文大学）

本研究提出基于Transformer的SATformer方法，通过建模子句交互识别不可满足子问题，结合多任务学习训练，性能显著优于NeuroSAT，还能将现有SAT求解器运行时间平均缩短21.33%。

2024-03-12cs.AIcs.LGcs.LO

DepQBF 6.0：超越传统QCDCL的基于搜索的QBF求解器

DepQBF 6.0: A Search-Based QBF Solver Beyond Traditional QCDCL

我们提出了基于QCDCL的量化布尔公式（QBF）求解器DepQBF的最新主要发布版本6.0。QCDCL是冲突驱动子句学习（CDCL）范式的扩展，在最先进的命题可满足性（SAT）求解器中实现。Q-resolution演算（QRES）是QCDCL的一个QBF证明系统。QCDCL求解器可以产生QBFs的QRES证明在前束合取范式（PCNF）作为求解过程的副产品。与基于QRES的传统QCDCL相比，DepQBF 6.0实现了基于QRES概括的QCDCL变体。这种推广是由于一组额外的公理，并保持原来的Q-归结规则不变。QRES的推广使QCDCL可能产生比传统变体更短的指数证明。我们提出了一个概述DepQBF中实现的功能和报告的实验结果表明，广义QRES在QCDCL的有效性。

2017-05-30cs.LO