Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?

• URL: http://arxiv.org/abs/2210.03553v1
• Date: Fri, 7 Oct 2022 13:40:07 GMT
• Title: Treewidth-aware Reductions of Normal ASP to SAT -- Is Normal ASP Harder than SAT after All?
• Authors: Markus Hecher
• Abstract summary: We show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT. We present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decompositions.
• Score: 9.480212602202517
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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 studies resulted in characterizations in terms of computational complexity as well as in fine-grained insights presented in form of dichotomy-style results, lower bounds when translating to other formalisms like propositional satisfiability (SAT), and even detailed parameterized complexity landscapes. A generic parameter in parameterized complexity originating from graph theory is the so-called treewidth, which in a sense captures structural density of a program. Recently, there was an increase in the number of treewidth-based solvers related to SAT. While there are translations from (normal) ASP to SAT, no reduction that preserves treewidth or at least keeps track of the treewidth increase is known. In this paper we propose a novel reduction from normal ASP to SAT that is aware of the treewidth, and guarantees that a slight increase of treewidth is indeed sufficient. Further, we show a new result establishing that, when considering treewidth, already the fragment of normal ASP is slightly harder than SAT (under reasonable assumptions in computational complexity). This also confirms that our reduction probably cannot be significantly improved and that the slight increase of treewidth is unavoidable. Finally, we present an empirical study of our novel reduction from normal ASP to SAT, where we compare treewidth upper bounds that are obtained via known decomposition heuristics. Overall, our reduction works better with these heuristics than existing translations.

Related papers

• Self-Satisfied: An end-to-end framework for SAT generation and prediction [0.7340017786387768]
  We introduce hardware accelerated algorithms for fast SAT problem generation and a geometric SAT encoding. These advances allow us to scale our approach to SAT problems with thousands of variables and tens of thousands of clauses. A fundamental aspect of our work concerns the very nature of SAT data and its suitability for training machine learning models.
  arXiv  Detail & Related papers  (2024-10-18T22:25:54Z)
• LiteSearch: Efficacious Tree Search for LLM [70.29796112457662]
  This study introduces a novel guided tree search algorithm with dynamic node selection and node-level exploration budget. Experiments conducted on the GSM8K and TabMWP datasets demonstrate that our approach enjoys significantly lower computational costs compared to baseline methods.
  arXiv  Detail & Related papers  (2024-06-29T05:14:04Z)
• Extended Version of: On the Structural Hardness of Answer Set Programming: Can Structure Efficiently Confine the Power of Disjunctions? [21.10339925217772]
  We deal with the classification of structural parameters for disjunctive ASP on the program's rule structure. We provide double-exponential lower bounds for the most prominent parameters in that range. Our results provide an in-depth hardness study, relying on a novel reduction from normal to disjunctive programs.
  arXiv  Detail & Related papers  (2024-02-05T21:51:36Z)
• Tree Prompting: Efficient Task Adaptation without Fine-Tuning [112.71020326388029]
  Tree Prompting builds a decision tree of prompts, linking multiple LM calls together to solve a task. Experiments on classification datasets show that Tree Prompting improves accuracy over competing methods and is competitive with fine-tuning.
  arXiv  Detail & Related papers  (2023-10-21T15:18:22Z)
• W2SAT: Learning to generate SAT instances from Weighted Literal Incidence Graphs [11.139131079925113]
  W2SAT is a framework to generate SAT formulas by learning intrinsic structures and properties from given real-world/industrial instances. We introduce a novel SAT representation called Weighted Literal Incidence Graph (WLIG), which exhibits strong representation ability and generalizability. Decoding from WLIG into SAT problems is then modeled as finding overlapping cliques with a novel hill-climbing optimization method.
  arXiv  Detail & Related papers  (2023-02-01T06:30:41Z)
• Characterizing Structural Hardness of Logic Programs: What makes Cycles and Reachability Hard for Treewidth? [9.480212602202517]
  This paper deals with a novel reduction from SAT to normal ASP that goes beyond well-known encodings. This characterizes hardness in a fine-grained way by establishing the required functional dependency of the dependency graph's cycle length.
  arXiv  Detail & Related papers  (2023-01-18T12:29:45Z)
• Estimating the hardness of SAT encodings for Logical Equivalence Checking of Boolean circuits [58.83758257568434]
  We show that the hardness of SAT encodings for LEC instances can be estimated textitw.r.t some SAT partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy.
  arXiv  Detail & Related papers  (2022-10-04T09:19:13Z)
• Lassoed Tree Boosting [53.56229983630983]
  We prove that a gradient boosted tree algorithm with early stopping faster than $n-1/4$ L2 convergence in the large nonparametric space of cadlag functions of bounded sectional variation. Our convergence proofs are based on a novel, general theorem on early stopping with empirical loss minimizers of nested Donsker classes.
  arXiv  Detail & Related papers  (2022-05-22T00:34:41Z)
• Transformer-based Machine Learning for Fast SAT Solvers and Logic Synthesis [63.53283025435107]
  CNF-based SAT and MaxSAT solvers are central to logic synthesis and verification systems. In this work, we propose a one-shot model derived from the Transformer architecture to solve the MaxSAT problem.
  arXiv  Detail & Related papers  (2021-07-15T04:47:35Z)
• Treewidth-Aware Complexity in ASP: Not all Positive Cycles are Equally Hard [15.5385123560379]
  It is known that deciding consistency for normal answer set programs (ASP) is NP-complete, as hard as the satisfaction problem for classical propositional logic (SAT) We show that the consistency problem for ASP can be solved in exponential time in k cdot log(lambda) where lambda is the minimum between the treewidth and the size of the largest strongly-connected component in the positive dependency graph of the program.
  arXiv  Detail & Related papers  (2020-07-09T08:09:41Z)
• From Checking to Inference: Actual Causality Computations as Optimization Problems [79.87179017975235]
  We present a novel approach to formulate different notions of causal reasoning, over binary acyclic models, as optimization problems. We show that both notions are efficiently automated. Using models with more than $8000$ variables, checking is computed in a matter of seconds, with MaxSAT outperforming ILP in many cases.
  arXiv  Detail & Related papers  (2020-06-05T10:56:52Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.