Top-Down Knowledge Compilation for Counting Modulo Theories
- URL: http://arxiv.org/abs/2306.04541v2
- Date: Thu, 30 Nov 2023 16:21:18 GMT
- Title: Top-Down Knowledge Compilation for Counting Modulo Theories
- Authors: Vincent Derkinderen, Pedro Zuidberg Dos Martires, Samuel Kolb, Paolo
Morettin
- Abstract summary: Propositional model counting can be solved efficiently when the input formula is in deterministic decomposable negation normal form (d-DNNF)
Top-down knowledge compilation is a state-of-the-art technique for solving #SAT problems.
We advocate for a top-down compiler based on the traces of exhaustive DPLL(T) search.
- Score: 11.086759883832505
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Propositional model counting (#SAT) can be solved efficiently when the input
formula is in deterministic decomposable negation normal form (d-DNNF).
Translating an arbitrary formula into a representation that allows inference
tasks, such as counting, to be performed efficiently, is called knowledge
compilation. Top-down knowledge compilation is a state-of-the-art technique for
solving #SAT problems that leverages the traces of exhaustive DPLL search to
obtain d-DNNF representations. While knowledge compilation is well studied for
propositional approaches, knowledge compilation for the (quantifier free)
counting modulo theory setting (#SMT) has been studied to a much lesser degree.
In this paper, we discuss compilation strategies for #SMT. We specifically
advocate for a top-down compiler based on the traces of exhaustive DPLL(T)
search.
Related papers
- Bisimulation Learning [55.859538562698496]
We compute finite bisimulations of state transition systems with large, possibly infinite state space.
Our technique yields faster verification results than alternative state-of-the-art tools in practice.
arXiv Detail & Related papers (2024-05-24T17:11:27Z) - Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming [8.34623776815378]
We curate a dataset of 600K lines of open-source F* programs and proofs.
Our dataset includes around 32K top-level F* definitions, each representing a type-directed program and proof synthesis problem.
We investigate the use of AI to synthesize programs and their proofs in F*, with promising results.
arXiv Detail & Related papers (2024-05-03T00:14:33Z) - 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) - An Eager Satisfiability Modulo Theories Solver for Algebraic Datatypes [4.393684402895834]
Algebraic data types (ADTs) are a construct classically found in functional programming languages.
We present an SMT solver that takes a fundamentally different approach, an empheager approach.
arXiv Detail & Related papers (2023-10-18T18:14:18Z) - TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative
Language Models [68.65075559137608]
We propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas.
We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system.
We develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability.
arXiv Detail & Related papers (2023-10-16T08:42:39Z) - When Do Program-of-Thoughts Work for Reasoning? [51.2699797837818]
We propose complexity-impacted reasoning score (CIRS) to measure correlation between code and reasoning abilities.
Specifically, we use the abstract syntax tree to encode the structural information and calculate logical complexity.
Code will be integrated into the EasyInstruct framework at https://github.com/zjunlp/EasyInstruct.
arXiv Detail & Related papers (2023-08-29T17:22:39Z) - Evaluating and Improving Tool-Augmented Computation-Intensive Math
Reasoning [75.74103236299477]
Chain-of-thought prompting(CoT) and tool augmentation have been validated as effective practices for improving large language models.
We propose a new approach that can deliberate the reasoning steps with tool interfaces, namely textbfDELI.
Experimental results on CARP and six other datasets show that the proposed DELI mostly outperforms competitive baselines.
arXiv Detail & Related papers (2023-06-04T17:02:59Z) - Explaining Patterns in Data with Language Models via Interpretable
Autoprompting [143.4162028260874]
We introduce interpretable autoprompting (iPrompt), an algorithm that generates a natural-language string explaining the data.
iPrompt can yield meaningful insights by accurately finding groundtruth dataset descriptions.
Experiments with an fMRI dataset show the potential for iPrompt to aid in scientific discovery.
arXiv Detail & Related papers (2022-10-04T18:32:14Z) - Linear Temporal Logic Modulo Theories over Finite Traces (Extended
Version) [72.38188258853155]
This paper studies Linear Temporal Logic over Finite Traces (LTLf)
proposition letters are replaced with first-order formulas interpreted over arbitrary theories.
The resulting logic, called Satisfiability Modulo Theories (LTLfMT), is semi-decidable.
arXiv Detail & Related papers (2022-04-28T17:57:33Z) - Refinement Type Directed Search for Meta-Interpretive-Learning of
Higher-Order Logic Programs [2.28438857884398]
We show that type checking is able to prune large parts of the hypothesis space of programs.
We are able to infer polymorphic types of synthesized clauses and of entire programs.
arXiv Detail & Related papers (2021-02-18T13:40: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.