Answer 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 end, we propose two kinds of graph representations of programs to exploit their treewidth as a parameter. Treewidth roughly measures to which extent the internal structure of a program resembles a tree. Our main contribution is the design of parameterized dynamic programming algorithms, which run in linear time if the treewidth and weights of the given program are bounded. Compared to previous work, our algorithms handle the full syntax of ASP. Finally, we report on an empirical evaluation that shows good runtime behaviour for benchmark instances of low treewidth, especially for counting answer sets.
Code (1)
Similar Papers 제목 키워드 기반
Structural Decompositions of Epistemic Logic Programs
Epistemic logic programs (ELPs) are a popular generalization of standard Answer Set Programming (ASP) providing means for reasoning over answer sets within the language. This richer formalism comes at the price of higher…
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 formul…
Tractable Weighted First-Order Model Counting with Bounded Treewidth Binary Evidence
The Weighted First-Order Model Counting Problem (WFOMC) asks to compute the weighted sum of models of a given first-order logic sentence over a given domain. Conditioning WFOMC on evidence -- fixing the truth values of a…
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…
BenchmarkingManagementSteepest ascent can be exponential in bounded treewidth problems
We investigate the complexity of local search based on steepest ascent. We show that even when all variables have domains of size two and the underlying constraint graph of variable interactions has bounded treewidth (in…