Extending SMT Solving with Non-Ground Clause Learning

• URL: http://arxiv.org/abs/2609.11509v1
• Date: Thu, 10 Sep 2026 13:17:14 GMT
• Title: Extending SMT Solving with Non-Ground Clause Learning
• Abstract summary: We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis.<n>Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Quantifier instantiation is currently the main approach to non-ground SMT solving: solvers generate ground instances and solve the resulting ground SMT problems with CDCL(T)-style reasoning. When a conflict is found, conflict analysis learns only a ground clause, even though the conflict comes from instances of non-ground clauses. Yet non-ground reasoning can give exponentially shorter proofs than purely ground reasoning. We propose a calculus that consists of ground instantiations, CDCL(T)-style rules, and non-ground conflict analysis. The solver reasons on ground instances, but the resolution steps of conflict analysis are performed on their original non-ground clauses. This produces learned clauses that are typically more general than the ground conflict. With a suitable strategy, the learned clauses are even non-redundant. We also show how chronological backtracking can be included in SMT solving. Our calculus gives a common setting for CDCL(T)-style SMT solving, a range of instantiation-based procedures, and non-ground clause learning, and we prove that it simulates CDCL, SCL(FOL), SCL(T), and even Resolution.

Related papers

• SALA: Semantic-Aware Logical Alignment for Complex Reasoning in In-Context Learning [61.13104919370034]
  We propose SALA, a Semantic-Aware Logical Alignment framework.<n>Instead of relying on a fixed inventory, SALA automatically learns task-specific reasoning operations.<n>It then embeds these operations into a continuous semantic space and uses dynamic time warping to align the reasoning sequences.
  arXiv  Detail & Related papers  (2026-09-02T09:12:03Z)
• Training LLMs for Divide-and-Conquer Reasoning Elevates Test-Time Scalability [129.1296673737603]
  Large language models (LLMs) have demonstrated strong reasoning capabilities through step-by-step chain-of-thought (CoT) reasoning.<n>A potential alternative is divide-and-conquer (DAC) reasoning, which decomposes a complex problem into subproblems to facilitate more effective exploration of the solution.<n>We propose an end-to-end reinforcement learning (RL) framework to enhance their DAC-style reasoning capacity.
  arXiv  Detail & Related papers  (2026-02-02T18:54:54Z)
• Reason-KE++: Aligning the Process, Not Just the Outcome, for Faithful LLM Knowledge Editing [63.96040994220329]
  We find that SFT-based methods, e.g., Reason-KE, suffer from a "faithfulness gap"<n>This gap enables the LLM's powerful parametric priors to override new contextual facts.<n>We propose Reason-KE++, an SFT+RL framework that instills process-level faithfulness.
  arXiv  Detail & Related papers  (2025-11-16T15:49:01Z)
• Thinking Before You Speak: A Proactive Test-time Scaling Approach [54.8205006555199]
  We implement our idea as a reasoning framework, named emphThinking Before You Speak (TBYS)<n>We design a pipeline for automatically collecting and filtering in-context examples for the generation of emphinsights.<n>Experiments on challenging mathematical datasets verify the effectiveness of TBYS.
  arXiv  Detail & Related papers  (2025-08-26T03:43:32Z)
• Grounding Rule-Based Argumentation Using Datalog [3.1457219084519004]
  ASPIC+ is one of the main general frameworks for rule-based argumentation for AI.<n>We propose an intelligent grounding procedure that keeps the size of the grounding manageable while preserving the correctness of the reasoning process.<n>We also propose simplifications specific to the ASPIC+ formalism to avoid grounding of rules that have no influence on the reasoning process.
  arXiv  Detail & Related papers  (2025-08-14T17:57:32Z)
• Syzygy of Thoughts: Improving LLM CoT with the Minimal Free Resolution [59.39066657300045]
  Chain-of-Thought (CoT) prompting enhances the reasoning of large language models (LLMs) by decomposing problems into sequential steps.<n>We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths.<n>SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• Large Language Models as an Indirect Reasoner: Contrapositive and Contradiction for Automated Reasoning [74.90592233107712]
  We propose a Direct-Indirect Reasoning (DIR) method, which considers Direct Reasoning (DR) and Indirect Reasoning (IR) as multiple parallel reasoning paths that are merged to derive the final answer.<n>Our DIR method is simple yet effective and can be straightforwardly integrated with existing variants of CoT methods.
  arXiv  Detail & Related papers  (2024-02-06T03:41:12Z)
• DCR: Divide-and-Conquer Reasoning for Multi-choice Question Answering with LLMs [9.561022942046279]
  We propose Divide and Conquer Reasoning (DCR) to enhance the reasoning capability of large language models (LLMs) We first categorize questions into two subsets based on confidence score ($mathcalCS$), which is estimated by statistical frequency of generated answers. In particular, we first categorize questions into two subsets based on confidence score ($mathcalCS$), which is estimated by statistical frequency of generated answers.
  arXiv  Detail & Related papers  (2024-01-10T14:38:46Z)
• SCL(FOL) Can Simulate Non-Redundant Superposition Clause Learning [0.3867363075280543]
  We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering.
  arXiv  Detail & Related papers  (2023-05-22T11:12:39Z)
• Too much information: CDCL solvers need to forget and perform restarts [0.0]
  Conflict-driven clause learning (CDCL) is a remarkably successful paradigm for solving the satisfiability problem of propositional logic. This paper will demonstrate, quite surprisingly, that clause learning can not only improve the runtime but can oftentimes deteriorate it dramatically.
  arXiv  Detail & Related papers  (2022-02-01T10:16:04Z)
• A Deep Dive into Conflict Generating Decisions [3.222802562733787]
  We use Conflict Driven Clause Learning to solve Satisfiability (SAT) problems. We show that CDCL learns clauses from conflicts, a technique that allows a solver to prune its search space. We develop Common Reason Variable Reduction (CRVR) as a new decision strategy that reduces the selection priority of some variables from the learned clauses of mc decisions.
  arXiv  Detail & Related papers  (2021-05-10T18:17:52Z)
• On the Effect of Learned Clauses on Stochastic Local Search [0.0]
  Conflict-driven clause learning (CDCL) and local search (SLS) are used in SAT solvers. We experimentally demonstrate that clauses with a large number of correct literals are beneficial to the runtime of SLS. We deduce the most beneficial strategies to add high-quality clauses as a preprocessing step.
  arXiv  Detail & Related papers  (2020-05-07T13:33:16Z)

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.