An ASP-Based Framework for MUSes

• URL: http://arxiv.org/abs/2507.03929v1
• Date: Sat, 05 Jul 2025 07:23:24 GMT
• Title: An ASP-Based Framework for MUSes
• Authors: Mohimenul Kabir, Kuldeep S Meel,
• Abstract summary: Given an unsatisfiable formula, understanding the core reason for unsatisfiability is crucial in several applications.<n>One effective way to capture this is through the minimal unsatisfiable subset (MUS), the subset-minimal set of clauses that remains unsatisfiable.<n>Current research broadly focuses on two directions: (i) enumerating as many MUSes as possible within a given time limit, and (ii) counting the total number of MUSes for a given unsatisfiable formula.<n>In this paper, we introduce an answer set programming-based framework
• Score: 31.74767457870183
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Given an unsatisfiable formula, understanding the core reason for unsatisfiability is crucial in several applications. One effective way to capture this is through the minimal unsatisfiable subset (MUS), the subset-minimal set of clauses that remains unsatisfiable. Current research broadly focuses on two directions: (i) enumerating as many MUSes as possible within a given time limit, and (ii) counting the total number of MUSes for a given unsatisfiable formula. In this paper, we introduce an answer set programming-based framework, named MUS-ASP, designed for online enumeration of MUSes. ASP is a powerful tool for its strengths in knowledge representation and is particularly suitable for specifying complex combinatorial problems. By translating MUS enumeration into answer set solving, MUS-ASP leverages the computational efficiency of state-of-the-art ASP systems. Our extensive experimental evaluation demonstrates the effectiveness of MUS-ASP and highlights the acceleration in both MUS enumeration and counting tasks, particularly when integrated within hybrid solvers, including the framework proposed in this paper.

Related papers

• EIFBENCH: Extremely Complex Instruction Following Benchmark for Large Language Models [65.48902212293903]
  We present the Extremely Complex Instruction Following Benchmark (EIFBENCH) for evaluating large language models (LLMs)<n>EIFBENCH includes multi-task scenarios that enable comprehensive assessment across diverse task types concurrently.<n>We also propose the Segment Policy Optimization (SegPO) algorithm to enhance the LLM's ability to accurately fulfill multi-task workflow.
  arXiv  Detail & Related papers  (2025-06-10T02:39:55Z)
• Symbolic Mixture-of-Experts: Adaptive Skill-based Routing for Heterogeneous Reasoning [76.10639521319382]
  We propose Symbolic-MoE, a symbolic, text-based, and gradient-free Mixture-of-Experts framework.<n>We show Symbolic-MoE beats strong LLMs like GPT4o-mini, as well as multi-agent approaches, with an absolute avg. gain of 8.15% over the best multi-agent baseline.
  arXiv  Detail & Related papers  (2025-03-07T18:03:13Z)
• Multi2: Multi-Agent Test-Time Scalable Framework for Multi-Document Processing [43.75154489681047]
  We propose a novel framework leveraging test-time scaling for Multi-Document Summarization (MDS)<n>Our approach employs prompt ensemble techniques to generate multiple candidate summaries using various prompts, then combines them with an aggregator to produce a refined summary.<n>To evaluate our method effectively, we also introduce two new LLM-based metrics: the Consistency-Aware Preference (CAP) score and LLM Atom-Content-Unit (LLM-ACU) score.
  arXiv  Detail & Related papers  (2025-02-27T23:34:47Z)
• Answer Set Counting and its Applications [0.8158530638728501]
  We developed an exact ASP counter, sharpASP, which utilizes a compact encoding for propositional formulas.<n>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)
• Sparse Mixture-of-Experts for Compositional Generalization: Empirical Evidence and Theoretical Foundations of Optimal Sparsity [89.81738321188391]
  This study investigates the relationship between task complexity and optimal sparsity in SMoE models.<n>We show that the optimal sparsity lies between minimal activation (1-2 experts) and full activation, with the exact number scaling proportionally to task complexity.
  arXiv  Detail & Related papers  (2024-10-17T18:40:48Z)
• Quantifying over Optimum Answer Sets [6.390468088226495]
  ASP(Q) lacks a method for encoding modeling in an elegant and compact way. We propose an extension of ASP(Q) in which component programs may contain weak constraints. We showcase the modeling capabilities of the new formalism through various application scenarios.
  arXiv  Detail & Related papers  (2024-08-14T17:53:13Z)
• One Prompt is not Enough: Automated Construction of a Mixture-of-Expert Prompts [110.94724216491753]
  Large Language Models (LLMs) exhibit strong generalization capabilities when prompted with language instructions and in-context demos. Various methods have been explored to automate the instruction design, but they restricted the searched prompt to one instruction. We adopt the Mixture-of-Expert paradigm and divide the problem space into a set of sub-regions. A two-phase process is developed to construct the specialized expert for each region. A region-based joint search of an instruction per expert complements the demos assigned to it, yielding a synergistic effect.
  arXiv  Detail & Related papers  (2024-06-28T23:05:08Z)
• QFMTS: Generating Query-Focused Summaries over Multi-Table Inputs [63.98556480088152]
  Table summarization is a crucial task aimed at condensing information into concise and comprehensible textual summaries. We propose a novel method to address these limitations by introducing query-focused multi-table summarization. Our approach, which comprises a table serialization module, a summarization controller, and a large language model, generates query-dependent table summaries tailored to users' information needs.
  arXiv  Detail & Related papers  (2024-05-08T15:05:55Z)
• Large Language Models to Enhance Bayesian Optimization [57.474613739645605]
  We present LLAMBO, a novel approach that integrates the capabilities of Large Language Models (LLM) within Bayesian optimization. At a high level, we frame the BO problem in natural language, enabling LLMs to iteratively propose and evaluate promising solutions conditioned on historical evaluations. Our findings illustrate that LLAMBO is effective at zero-shot warmstarting, and enhances surrogate modeling and candidate sampling, especially in the early stages of search when observations are sparse.
  arXiv  Detail & Related papers  (2024-02-06T11:44:06Z)
• Exact ASP Counting with Compact Encodings [32.300155018027624]
  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.
  arXiv  Detail & Related papers  (2023-12-19T08:27:29Z)
• 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)

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.