Exact ASP Counting with Compact Encodings

• URL: http://arxiv.org/abs/2312.11936v1
• Date: Tue, 19 Dec 2023 08:27:29 GMT
• Title: Exact ASP Counting with Compact Encodings
• Authors: Mohimenul Kabir and Supratik Chakraborty and Kuldeep S Meel
• Abstract summary: This paper presents a new ASP counting framework, called sharpASP, which counts answer sets avoiding larger input formulas. Our empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters.
• Score: 32.300155018027624
• License: http://creativecommons.org/licenses/by-sa/4.0/
• Abstract: Answer Set Programming (ASP) has emerged as a promising paradigm in knowledge representation and automated reasoning owing to its ability to model hard combinatorial problems from diverse domains in a natural way. Building on advances in propositional SAT solving, the past two decades have witnessed the emergence of well-engineered systems for solving the answer set satisfiability problem, i.e., finding models or answer sets for a given answer set program. In recent years, there has been growing interest in problems beyond satisfiability, such as model counting, in the context of ASP. Akin to the early days of propositional model counting, state-of-the-art exact answer set counters do not scale well beyond small instances. Exact ASP counters struggle with handling larger input formulas. The primary contribution of this paper is a new ASP counting framework, called sharpASP, which counts answer sets avoiding larger input formulas. This relies on an alternative way of defining answer sets that allows for the lifting of key techniques developed in the context of propositional model counting. Our extensive empirical analysis over 1470 benchmarks demonstrates significant performance gain over current state-of-the-art exact answer set counters. Specifically, by using sharpASP, we were able to solve 1062 benchmarks with PAR2 score of 3082 whereas using prior state-of-the-art, we could only solve 895 benchmarks with a PAR2 score of 4205, all other experimental conditions being the same.

Related papers

• Answer Set Counting and its Applications [0.8158530638728501]
  We developed an exact ASP counter, sharpASP, which utilizes a compact encoding for propositional formulas. In addition, we proposed an approximate ASP counter, named ApproxASP, a hashing-based counter integrating Gauss-Jordan elimination within the ASP solver, clingo.
  arXiv  Detail & Related papers  (2025-02-13T11:52:55Z)
• Scaling up Test-Time Compute with Latent Reasoning: A Recurrent Depth Approach [70.44265766483633]
  We study a novel language model architecture that is capable of scaling test-time computation by implicitly reasoning in latent space. Our model works by iterating a recurrent block, thereby unrolling to arbitrary depth at test-time. We show that the resulting model can improve its performance on reasoning benchmarks, sometimes dramatically.
  arXiv  Detail & Related papers  (2025-02-07T18:55:02Z)
• IASCAR: Incremental Answer Set Counting by Anytime Refinement [18.761758874408557]
  This paper introduces a technique to iteratively count answer sets under assumptions on knowledge compilations of CNFs that encode supported models. In a preliminary empirical analysis, we demonstrate promising results.
  arXiv  Detail & Related papers  (2023-11-13T10:53:48Z)
• Answer-Set Programming for Lexicographical Makespan Optimisation in Parallel Machine Scheduling [18.286430978487388]
  We deal with a challenging scheduling problem on parallel machines with sequence-dependent setup times and release dates. We put the individual machine spans in non-ascending order and lexicographically minimise the resulting robustnesss. Our experimental results show that ASP is indeed a promising KRR paradigm for this problem and is competitive with state-of-the-art CP and MIP solvers.
  arXiv  Detail & Related papers  (2022-12-18T12:43:24Z)
• Successive Prompting for Decomposing Complex Questions [50.00659445976735]
  Recent works leverage the capabilities of large language models (LMs) to perform complex question answering in a few-shot setting. We introduce Successive Prompting'', where we iteratively break down a complex task into a simple task, solve it, and then repeat the process until we get the final solution. Our best model (with successive prompting) achieves an improvement of 5% absolute F1 on a few-shot version of the DROP dataset.
  arXiv  Detail & Related papers  (2022-12-08T06:03:38Z)
• Aggregate Semantics for Propositional Answer Set Programs [14.135212040150389]
  We present and compare the main aggregate semantics that have been proposed for propositional ASP programs. We highlight crucial properties such as computational complexity and expressive power, and outline the capabilities and limitations of different approaches.
  arXiv  Detail & Related papers  (2021-09-17T17:38:55Z)
• 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)
• grASP: A Graph Based ASP-Solver and Justification System [5.098678276629787]
  We propose a novel dependency graph-based approach for finding answer sets in which conjunction of goals is explicitly represented as a node. Our representation preserves causal relationships allowing for justification for each literal in the answer set to be elegantly found.
  arXiv  Detail & Related papers  (2021-04-02T18:16:20Z)
• Few-Shot Question Answering by Pretraining Span Selection [58.31911597824848]
  We explore the more realistic few-shot setting, where only a few hundred training examples are available. We show that standard span selection models perform poorly, highlighting the fact that current pretraining objective are far removed from question answering. Our findings indicate that careful design of pretraining schemes and model architecture can have a dramatic effect on performance in the few-shot settings.
  arXiv  Detail & Related papers  (2021-01-02T11:58:44Z)
• Session-Aware Query Auto-completion using Extreme Multi-label Ranking [61.753713147852125]
  We take the novel approach of modeling session-aware query auto-completion as an e Multi-Xtreme Ranking (XMR) problem. We adapt a popular XMR algorithm for this purpose by proposing several modifications to the key steps in the algorithm. Our approach meets the stringent latency requirements for auto-complete systems while leveraging session information in making suggestions.
  arXiv  Detail & Related papers  (2020-12-09T17:56:22Z)

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.