May, 2015

HordeSat：一个高并行的 SAT 求解器组合器

PDF
TL;DR本研究探讨了在大规模并行 SAT 问题求解中应用基于投资组合的分布式 SAT 求解方法，并实现了一个名为 HordeSat 的可扩展的并行 SAT 求解器，其使用分层并行和分布式设计，实现了数百到数千个处理器的可观加速效果。
parallel satisfiability solvingportfolio-based sat solvermassively parallel solvingdecentralized designhierarchical parallelism
发现论文，激发创造
  • Proteus: 分层求解器和转换组合

    该论文提出了一种名为 Proteus 的分层组合策略解决 CSP 问题的方法，该方法能够将 CSP 实例编码为 SAT 形式，并选择合适的编码和相应的 SAT 求解器进行求解，实验结果表明 Proteus 能够显著提高组合问题求解性能。

    Jun, 2013

  • 基于 GPU 的混合 SAT 求解的大规模并行连续局部搜索

    提出了基于梯度驱动连续局部搜索（CLS）的高度并行混合 SAT 求解器 FastFourierSAT，该算法利用图形处理单元（GPU）的并行性能加速计算，可以比之前的方法快 100 + 倍，并在更大规模的案例上表现出良好的性能。

    Aug, 2023

  • SATzilla: 基于投资组合的 SAT 算法选择

    SATzilla 是一种使用经验难度模型来构建每个实例算法组合的自动化方法，用于选择 SAT 问题的求解器，并在实验中得到了卓越的表现。

    Oct, 2011

  • 使用连续运行分布预测 SAT 局部搜索的并行加速

    本文通过分析顺序版本算法的运行时行为，提出了一种评估给定算法并行性能的框架，并将此方法应用于研究两种 SAT 局部搜索求解器的并行性能，结果表明模型能够准确预测性能并展示了不同情况下局部搜索求解器的运行时分布。

    Jan, 2024

  • 一个用于约束求解的多核工具

    介绍了 sunny-cp2：第一个在多核设置下实现并行 CP 投资组合求解器，它可以动态、协同和同时执行其求解器。它包含最先进的求解器，并提供可用的和可配置的框架，实证结果非常有前途。

    Feb, 2015

  • FourierSAT: 一个基于傅里叶展开的代数框架求解混合布尔约束问题

    FourierSAT 是一种基于布尔函数的傅里叶分析的不完全的 SAT 求解器，其提出一种用于解决具有不同类型限制的系统的代数框架，并通过实验证明在某些基准测试上，它比其他解算器更具鲁棒性。

    Dec, 2019

  • AutoSAT: 通过大型语言模型自动优化 SAT 求解器

    AutoSAT 是一种自动优化 SAT 解算器中启发式算法的新框架，基于大型模型（LLMs），它能够自主生成代码、进行评估，并利用反馈进一步优化启发式算法，从而减少人工干预并增强解算器的能力。AutoSAT 在插拔式基础上操作，不需要广泛的预备设置和模型训练，促进了具有容错性的思维链的合作过程，确保了强大的启发式优化。对 Conflict-Driven Clause Learning (CDCL) 解算器进行的大量实验证明了 AutoSAT 的整体优异性能，特别是在解决一些特定的 SAT 问题实例中。

    Feb, 2024

  • 实现高效的全解 SAT 求解器

    本文介绍 AllSAT 问题及其重要意义，探讨解决方案，实施大量实验并公开开发的求解器以及该问题的特征。

    Oct, 2015

  • 分而治之：约束满足问题的通用方法

    介绍一种用几何模型来解决多约束条件优化问题的方法，并在布尔可满足性问题和球体堆积问题两个基准测试中说明了其有效性和竞争性。

    Dec, 2007

  • 可配置的 SAT 求解器挑战 (CSSC)

    Configurable SAT Solver Competition (CSSC) compares solvers by the performance they achieved after a fully automated configuration step to solve combinatorial problems, particularly propositional satisfiability problem (SAT), by tuning solver parameters, with CSSC 2013 and 2014 being reported.

    May, 2015