MMJun, 2013

Proteus: 分层求解器和转换组合

PDF
TL;DR该论文提出了一种名为 Proteus 的分层组合策略解决 CSP 问题的方法，该方法能够将 CSP 实例编码为 SAT 形式，并选择合适的编码和相应的 SAT 求解器进行求解，实验结果表明 Proteus 能够显著提高组合问题求解性能。
portfolio approachescsp solvingsat instanceshierarchical portfolio-based approachproteus
发现论文，激发创造
  • HordeSat：一个高并行的 SAT 求解器组合器

    本研究探讨了在大规模并行 SAT 问题求解中应用基于投资组合的分布式 SAT 求解方法，并实现了一个名为 HordeSat 的可扩展的并行 SAT 求解器，其使用分层并行和分布式设计，实现了数百到数千个处理器的可观加速效果。

    May, 2015

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

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

    Feb, 2015

  • 一种增强特征提取器，用于约束求解器的组合

    本文介绍了一种取自不同建模语言（MiniZinc、FlatZinc 或 XCSP）的限制编程（CSP）问题的特征集，用于求解器选择，实验结果显示使用这些特征可与最先进的 CSP 投资组合技术相竞争

    Aug, 2013

  • SUNNY: 一种针对约束求解的惰性组合投资策略

    本文提出了一种名为 SUNNY 的算法，利用约束求解器的组合来求解 Constraint Satisfaction Problem，通过实验表明 SUNNY 算法效果优于其他现有算法，并提出了一个基于 SUNNY 的 portfolio solver -- sunny-csp，同时探讨了该算法用于 Answer Set Programming 和 Constraint Logic Programming 的可能性。

    Nov, 2013

  • 解决四类 SAT 问题的通用方法

    该研究提出了一种基于整数规划和强化学习算法的统一框架 DCSAT，用于解决不同类型的布尔可满足性问题，包括 MaxSAT、Weighted MaxSAT、PMS 和 WPMS 等。通过调整目标函数系数，构建了统一的整数规划表示方法，并基于 0-1 整数规划构建了适当的强化学习模型。基于二叉树搜索结构，在 SAT 问题上应用了蒙特卡罗树搜索（MCTS）方法，证明了该方法能够基于维纳 - 欣钦大数定律找到所有最优的布尔赋值。实验证明，该方法能够剪枝不必要的搜索空间，找到问题的最优布尔赋值，同时为 SAT 问题的监督学习方法提供多样的标签。

    Dec, 2023

  • 约束答案集编程：集成与转化（或基于 SMT 的）方法

    本文提出了 Constraint answer set programming 技术的概述，重点介绍了整合法和翻译法两种设计 Constraint answer set 求解器的方法，并提供了一个基于该技术的 Traveling Salesman Problem 的编码实例。

    Jul, 2021

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

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

    Dec, 2007

  • 约束求解器 EZCSP 及其集成架构的重要性

    本研究提出了约束应答集编程 Constraint Answer Set Programming （CASP）新研究领域，开发相应的 EZCSP 语言及其解释器并对其进行了系统性的研究，其设计和算法细节清晰地证明了这种混合系统的发展具有挑战性。在此基础上，展开了基于 EZCSP 的案例研究，重点关注其提供的各种集成方式。

    Feb, 2017

  • 基于答案集规划的求解器调度

    本研究提出了一种使用 Answer Set Programming 自动确定精细的、非均匀且有序的求解器调度方案的方法，并且可以定制化地生成并行调度方案。

    Jan, 2014

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

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

    Oct, 2011