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

• Assisting Mathematical Formalization with A Learning-based Premise Retriever [29.06255449960557]
  We introduce an innovative method for training a premise retriever to support the formalization of mathematics. Our approach employs a BERT model to embed proof states and premises into a shared latent space. To streamline the formalization process, we will release a search engine that enables users to query Mathlib theorems directly using proof states.
  arXiv  Detail & Related papers  (2025-01-21T06:32:25Z)
• Training Neural Networks as Recognizers of Formal Languages [87.06906286950438]
  Formal language theory pertains specifically to recognizers. It is common to instead use proxy tasks that are similar in only an informal sense. We correct this mismatch by training and evaluating neural networks directly as binary classifiers of strings.
  arXiv  Detail & Related papers  (2024-11-11T16:33:25Z)
• CASET: Complexity Analysis using Simple Execution Traces for CS* submissions [0.0]
  The most common method to auto-grade a student's submission in a CS1 or a CS2 course is to run it against a pre-defined test suite and compare the results against reference results. This technique cannot be used if the correctness of the solution goes beyond simple output, such as the algorithm used to obtain the result. We propose CASET, a novel tool to analyze the time complexity of algorithms using dynamic traces and unsupervised machine learning.
  arXiv  Detail & Related papers  (2024-10-20T15:29:50Z)
• 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)
• 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)
• 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)

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.