论文标题
基于树宽的问题解决的高级工具和方法 - 扩展摘要
Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract
论文作者
论文摘要
用于解决众所周知的布尔可满足性问题（SAT）的计算机程序，所谓的求解器（SAT）已有数十年的改善。原因之一是，这些求解器如此之快的原因是在求解过程中公式的结构属性的隐含用法。这样的结构指标之一是所谓的树宽，它试图测量公式实例与变得容易的距离（类似树）。这项工作着重于基于逻辑的问题和基于树宽的方法和解决方案的工具。这些问题中的许多也与知识表示和推理（KR）以及人工智能（AI）有关。我们提出了一种新型的问题，这是由分解引导（DG）提到的。这种还原类型构成了解决自2004年以来一直开放的有界树宽的量化布尔公式（QBF）问题的基础。然后，该问题的解决方案引起了一种新方法，以证明逻辑，KR和AI的一系列进一步形式的精确下限。尽管已建立的下限，但我们通过直接使用树宽来实现一种算法来有效地求解SAT的扩展。我们的实施是基于查找实例的抽象，然后在此过程中逐步完善。因此，我们的观察结果证实，树宽是现代求解器设计中应考虑的重要措施。
Computer programs, so-called solvers, for solving the well-known Boolean satisfiability problem (Sat) have been improving for decades. Among the reasons, why these solvers are so fast, is the implicit usage of the formula's structural properties during solving. One of such structural indicators is the so-called treewidth, which tries to measure how close a formula instance is to being easy (tree-like). This work focuses on logic-based problems and treewidth-based methods and tools for solving them. Many of these problems are also relevant for knowledge representation and reasoning (KR) as well as artificial intelligence (AI) in general. We present a new type of problem reduction, which is referred to by decomposition-guided (DG). This reduction type forms the basis to solve a problem for quantified Boolean formulas (QBFs) of bounded treewidth that has been open since 2004. The solution of this problem then gives rise to a new methodology for proving precise lower bounds for a range of further formalisms in logic, KR, and AI. Despite the established lower bounds, we implement an algorithm for solving extensions of Sat efficiently, by directly using treewidth. Our implementation is based on finding abstractions of instances, which are then incrementally refined in the process. Thereby, our observations confirm that treewidth is an important measure that should be considered in the design of modern solvers.
