Optimally Solving the MCM Problem Using Pseudo-Boolean Satisfiability
本文描述了多常数乘法（MCM）问题到伪布尔可满足性（PBS）的三种编码，并介绍了一种最优求解MCM问题的算法。据我们所知，所提出的编码和优化算法是第一次正式的MCM问题在PBS的方式。该报告评估了问题大小的复杂性和几个PBS求解器在三种编码上的性能。
2011-05-17 cs.LO math.LO math.OC
diff-SAT -- A Software for Sampling and Probabilistic Reasoning for SAT and Answer Set Programming
National University of Ireland, Galway（爱尔兰国立高威大学）
本文介绍了diff-SAT，一个答案集和SAT求解器，它结合了经常使用概率条款，事实和规则的能力，解决和采样的最佳世界观（满足布尔变量分配或答案集的多集）受用户提供的概率约束。采样过程使用称为可微可满足性求解（$\partial\mathrm{SAT}$）或可微答案集编程（$\partial\mathrm{ASP}$）的基于梯度下降的优化方法来最小化用户定义的可微目标函数。用例是i.a.概率逻辑编程（以概率答案集编程的形式），概率布尔可满足性求解（PSAT）和模型多集（答案集或布尔解释）的分布感知采样。
2021-01-03 cs.AI cs.LO
A novel algorithm for solving the Decision Boolean Satisfiability Problem without algebra
本文描述了一个算法，解决决策布尔可满足性问题的一个特殊的决策可满足性问题的二进制数值性质，并行执行，面向对象，和短终止。用扩展和简化这两种操作来解释为什么使用代数增加了分辨率步骤。证明了该问题的复杂度有一个上界为$2^{n-1}$，其中$n$是给定问题的逻辑变量数.
2018-04-14 cs.CC cs.DS cs.LO
On Continuous Local BDD-Based Search for Hybrid SAT Solving
Rice University（莱斯大学）
我们探讨了连续局部搜索（CLS）在SAT求解的潜力，提出了一种新的方法来寻找一个混合系统的布尔约束的解决方案。该算法是基于CLS结合置信传播二叉决策图（BDD）。我们的框架接受所有的布尔约束，承认紧凑的BDD，包括对称布尔约束和小系数伪布尔约束作为有趣的家庭。我们提出了一种新的算法，有效地计算CLS所需的梯度。我们研究我们的多功能CLS求解器，GradSAT的能力和局限性，通过将其应用于许多基准测试实例。实验结果表明，GradSAT可以是一个有用的除了现有的SAT和MaxSAT求解器解决布尔可满足性和优化问题的投资组合。
2021-06-12 cs.AI cs.IT cs.LG
Solving Quantum-Inspired Perfect Matching Problems via Tutte's Theorem-Based Hybrid Boolean Constraints
Rice University（莱斯大学）
针对量子计算中边着色图的受约束完美匹配问题，提出基于Tutte定理与优化技术的新型混合布尔约束编码，实验证明其扩展性显著优于竞争方法，凸显了设计特定问题编码的必要性。
2023-05-18 cs.AI cs.LO math.CO
Solving Linux Upgradeability Problems Using Boolean Optimization
管理软件包系统的软件复杂性可以被视为软件体系结构的主要挑战之一。需要在短时间内进行升级，预计系统在此之后将保持可靠和一致。对于系统中的每个包，必须考虑一组依赖关系和一组冲突。虽然这个问题在计算上很难解决，但需要有效的工具。在最好的情况下，提供的解决方案也应该是最佳的，以便更好地满足用户的需求和期望。本文介绍了两种不同的工具，都基于布尔可满足性（SAT），用于解决Linux可扩展性问题。这些工具的评估中使用的问题实例主要是从真实环境中获得的，并受到两个不同的字典优化标准。开发的工具可以为许多情况提供最佳解决方案，但仍然存在一些挑战。此外，我们的理解是，这个问题与其他配置问题有许多相似之处，因此相同的技术可以用于其他领域。
2010-07-07 cs.LO
DeciLS-PBO: an Effective Local Search Method for Pseudo-Boolean Optimization
Jilin University（吉林大学）
本文针对伪布尔优化（PBO）问题，通过扩展单元传播机制构建初始赋值并引入基于子句的care启发式信息，提出了局部搜索算法DeciLS-PBO，在多项基准测试中展现出优越性能。
2023-06-29 cs.AI cs.LO
FourierSAT: A Fourier Expansion-Based Algebraic Framework for Solving Hybrid Boolean Constraints
Rice University（莱斯大学）
布尔可满足性问题（SAT）是计算机科学中的一个重要问题.虽然SAT被认为是NP完全的，但在工程方面的进展，特别是基于子句驱动的子句学习（CDCL）和局部搜索SAT求解器，已经取得了显着的进展。然而，虽然旨在以合取范式（CNF）求解工业规模基准的SAT求解器已经变得相当成熟，但是对其他类型的约束有效的SAT求解器，例如，基数约束和异或的研究较少;处理非CNF约束的一般方法仍然缺乏。此外，以前的工作表明，对于特定类别的基准测试，现有的SAT求解器的运行时间在很大程度上取决于公式的属性和编码的细节，而不是基准测试的规模，这增加了不确定性的预期运行时间。为了解决上述问题，我们设计了FourierSAT，一个不完全SAT求解器的基础上傅立叶分析的布尔函数，一种技术来表示布尔函数的多线性多项式。通过这种连续优化的减少，我们提出了一个代数框架，用于解决由不同类型的约束组成的系统。这个想法是利用梯度信息来引导搜索过程中的局部改进的方向。实证结果表明，傅立叶SAT是更强大的比其他求解器在某些类的基准。
2020-02-24 cs.IT cs.LG cs.LO
Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer
布尔毕达哥拉斯三元组问题是Ramsey理论中一个长期存在的公开问题：自然数集合N = $\{1, 2, ...\}$能否被分成两部分，使得任何部分都不包含具有$a^2 + b^2 = c^2$的三元组$(a,b,c)$？二十多年前，罗纳德·格雷厄姆为这个解决方案颁发了一个奖项。我们解决这个问题，证明事实上是不可能的，通过使用立方体和征服范式，混合SAT方法的硬问题，采用前瞻性和CDCL求解器。一个重要的作用是由专门的前瞻性算法，它确实允许解决问题的集群与800个核心在大约2天。由于这个数学问题的普遍兴趣，我们的结果需要一个形式化的证明。利用SAT求解器的不可满足性证明的最新进展，我们制作并验证了DRAT格式的证明，其大小接近200 TB。我们从中提取并提供了一个68千兆字节的压缩证书，允许任何人重建DRAT证明以供检查。
2016-05-03 cs.DM cs.LO
Expansion-Based QBF Solving Without Recursion
近年来，基于展开的方法在求解量化布尔公式（QBF）方面的理论和实践都显示出了强大的功能，QBF是布尔变量上带有存在量词和泛量词的命题公式的扩展。这种方法部分地扩展了一种类型的变量（存在的或通用的），并将所获得的公式传递给SAT求解器以决定QBF。现有的基于展开的QBF求解器对给定的公式进行分块处理，并递归地进行展开，直到找到一个解为止.本文提出了一种基于展开的QBF求解算法，该算法一次处理整个量词前缀.因此，避免了展开原理的递归应用。实验表明，我们的简单的方法的性能是与QBF解决的艺术状态，特别是在与其他解决技术相结合。
2018-10-05 cs.LO
Towards Parallel Boolean Functional Synthesis
给定一个关系规范R（X，Y），其中X和Y是输入和输出变量的序列，我们希望将每个输出合成为输入的函数，使得规范成立。这就是所谓的布尔函数综合问题，并在几个领域的应用。在本文中，我们提出了解决这个问题的第一个并行方法，使用组合和CEGAR风格的推理作为关键的构建块。我们通过大量的实验表明，我们的方法优于现有的工具上的一大类基准。
2017-03-04 cs.LO
Solving QBF by Abstraction
许多验证和综合方法依赖于量化布尔公式（QBF）的求解技术。因此，以布尔函数形式的解决方案见证变得越来越重要，因为它们代表了实现或反例。我们提出了一个递归的反例引导的抽象和细化算法（CEGAR）的解决和证明QBF，利用结构推理的公式级。该算法将给定的QBF分解为一个命题公式，用于每个量词块，该量词块从不受此量词块约束的变量的赋值中抽象出来。此外，我们展示了如何获得一个有效的认证提取方法的算法之上。我们报告在求解器QuAbS（量化抽象求解器），赢得了最近的QBF竞争（QBFEVAL'18），该算法的实验评估。此外，我们证明了认证方法的有效性，使用合成基准和案例研究，在Petri游戏中合成获胜策略。
2018-09-10 cs.LO
RustSAT: A Library For SAT Solving in Rust
为降低SAT求解技术的使用门槛，研究提出Rust语言的SAT求解库RustSAT，提供实例生成读写、多求解器统一接口及多语言高层约束编码，推动SAT技术的广泛应用。
2025-05-21 cs.LO
Structural Analysis of Boolean Equation Systems
本文提出利用结构图分析布尔方程系统，证明互模拟结构图对应相同解，并保守扩展了先前依赖图方法，通过最小化结构图简化系统。
2010-02-17 cs.LO
Analysis of Boolean Equation Systems through Structure Graphs
我们通过使用结构图来分析求解布尔方程组的问题。后者是通过一组优雅的Plotkin风格的演绎规则获得的。本文的主要贡献是证明了具有双相似结构图的方程组具有相同的解。我们表明，我们的工作保守地扩展了早期的工作，由Keiren和Willemse进行，其中依赖图被用来分析布尔方程系统的一个子类，即，标准递归形式的方程组。我们通过一个小例子来说明我们的方法，展示了通过最小化其结构图来简化方程系统的效果。
2010-02-15 cs.FL cs.LO
Improving Reasoning on DQBF
这个博士项目的目的是为依赖量化布尔公式（DQBF）开发快速和强大的推理工具。在本文中，我们概述了两个属性，自给自足和对称性，潜在的可以利用预处理和处理中的DQBF解决过程。DQBF扩展了量化布尔公式（QBF），量化变量之间具有非线性依赖关系。自动化测试和调试技术是求解器工具链的重要组成部分。对于严格的DQBF求解器开发，我们正在研究新的自动化测试和调试技术，如在SAT和QBF求解中成功建立的那样。该工具正在开发中。
2019-10-02 cs.LO
Determining the Multiplicative Complexity of Boolean Functions using SAT
我们提出了一种基于SAT的构造性算法来确定布尔函数的乘法复杂度，即，在由两输入端“与”门、两输入端“异”门和反相器组成的任何逻辑网络中，数量最少的“与”门。为了加快求解时间，我们利用几个对称性破缺的约束，这些利用XAGs的属性，可能是有用的，超出了建议的SAT为基础的算法。我们进一步提出了一个启发式的后优化算法，以减少“异”门的数量，一旦“与”门的最佳数量已经获得，这也利用SAT求解器。我们的算法是能够找到所有最佳的XAGs的所有5输入仿射等价类的代表，并为一组频繁出现的6输入功能。
2020-05-04 cs.DS cs.LO quant-ph
