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

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsFormal Methods in Verification · Logic, programming, and type systems · Constraint Satisfaction and Optimization
