arXiv 1402.44652014-02-18cs.DScs.AI

并行立方体和征服

Concurrent Cube-and-Conquer

Delft University of Technology（代尔夫特理工大学）；University of Texas at Austin（德克萨斯大学奥斯汀分校）；Johannes Kepler University Linz（约翰内斯·开普勒大学林茨分校）

Peter van der Tak, Marijn J. H. Heule, Armin Biere

备注：: Third International Workshop on Pragmatics of SAT (PoS 2012)

阅读 PDF

arXiv 页面 ↗HTML 原文 ↗

摘要：

最近的工作介绍了立方体和征服的技术来解决硬SAT的情况下。它使用前瞻求解器将搜索空间划分为立方体。每个立方体处理的冲突驱动的条款学习（CDCL）解决方案。对于强大的性能至关重要的是决定何时从前瞻切换到CDCL的截止启发式。然而，这种离线启发式方法远非理想。在本文中，我们提出了一种新的混合求解器，同时适用于立方体和征服步骤。前瞻和CDCL求解器在每个立方体上一起工作，而通信仅限于同步。我们的并行立方体和征服求解器可以解决许多实例比纯前瞻，纯CDCL和离线立方体和征服，并可以提前中止有利于一个纯CDCL搜索，如果一个实例是不适合立方体和征服技术。

英文摘要：

Recent work introduced the cube-and-conquer technique to solve hard SAT instances. It partitions the search space into cubes using a lookahead solver. Each cube is tackled by a conflict-driven clause learning (CDCL) solver. Crucial for strong performance is the cutoff heuristic that decides when to switch from lookahead to CDCL. Yet, this offline heuristic is far from ideal. In this paper, we present a novel hybrid solver that applies the cube and conquer steps simultaneously. A lookahead and a CDCL solver work together on each cube, while communication is restricted to synchronization. Our concurrent cube-and-conquer solver can solve many instances faster than pure lookahead, pure CDCL and offline cube-and-conquer, and can abort early in favor of a pure CDCL search if an instance is not suitable for cube-and-conquer techniques.

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