Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Exploiting Database Management Systems and Treewidth for Counting
Bounded treewidth is one of the most cited combinatorial invariants, which was applied in the literature for solving several counting problems efficiently. A canonical counting problem is #SAT, which asks to count the sa…
BenchmarkingManagementAnswer Set Solving with Bounded Treewidth Revisited
Parameterized algorithms are a way to solve hard problems more efficiently, given that a specific parameter of the input is small. In this paper, we apply this idea to the field of answer set programming (ASP). To this e…
Structure-Aware Encodings of Argumentation Properties for Clique-width
Structural measures of graphs, such as treewidth, are central tools in computational complexity resulting in efficient algorithms when exploiting the parameter. It is even known that modern SAT solvers work efficiently o…
Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?
Answer Set Programming (ASP) is a paradigm for modeling and solving problems for knowledge representation and reasoning. There are plenty of results dedicated to studying the hardness of (fragments of) ASP. So far, these…
AllThreshold Treewidth and Hypertree Width
Treewidth and hypertree width have proven to be highly successful structural parameters in the context of the Constraint Satisfaction Problem (CSP). When either of these parameters is bounded by a constant, then CSP beco…