• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Theory and applications of satisfiability testing - SAT 2009 >Relaxed DPLL Search for MaxSAT
【24h】

Relaxed DPLL Search for MaxSAT

机译：轻松的DPLL搜索MaxSAT

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We propose a new incomplete algorithm for the Maximum Satisfiability (MaxSAT) problem on unweighted Boolean formulas, focused specifically on instances for which proving unsatisfiability is already computationally difficult. For such instances, our approach is often able to identify a small number of what we call "bottleneck" constraints, in time comparable to the time it takes to prove unsatisfiability. These bottleneck constraints can have useful semantic content. Our algorithm uses a relaxation of the standard backtrack search for satisfiability testing (SAT) as a guiding heuristic, followed by a low-noise local search when needed. This allows us to heuristically exploit the power of unit propagation and clause learning. On a test suite consisting of all unsatisfiable industrial instances from SAT Race 2008, our solver, RelaxedMinisat, is the only (MaxSAT) solver capable of identifying a single bottleneck constraint in all but one instance.
机译：针对非加权布尔公式，我们针对最大满意度（MaxSAT）问题提出了一种新的不完全算法，特别针对那些证明不满足已经很难计算的实例。在这种情况下，我们的方法通常能够识别少量的所谓的“瓶颈”约束，时间与证明不满意所花费的时间相当。这些瓶颈约束可以具有有用的语义内容。我们的算法使用标准回溯搜索的放宽来进行可满足性测试（SAT）作为指导启发法，然后在需要时进行低噪声本地搜索。这使我们能够启发式地利用单元传播和从句学习的力量。在包含SAT Race 2008中所有无法满足的工业实例的测试套件中，我们的求解器RelaxedMinisat是唯一能够识别除一个实例之外的所有瓶颈约束的（MaxSAT）求解器。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号