Advanced Tools and Methods for Treewidth-Based Problem Solving -- Extended Abstract

TL;DR

This paper introduces new treewidth-based methods and tools for solving logic problems, including a novel problem reduction and an efficient SAT extension solver, highlighting the importance of treewidth in modern solver design.

Contribution

It presents a decomposition-guided reduction for bounded treewidth QBFs and a new methodology for establishing lower bounds across various logical formalisms.

Findings

Successfully solved a long-standing QBF problem using treewidth-based reduction.

Implemented an efficient SAT extension solver leveraging instance abstractions.

Confirmed the significance of treewidth in the design of modern problem solvers.

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.