Canonical Decision Diagrams Modulo Theories

• URL: http://arxiv.org/abs/2404.16455v3
• Date: Fri, 2 Aug 2024 13:27:16 GMT
• Title: Canonical Decision Diagrams Modulo Theories
• Authors: Massimo Michelutti, Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani,
• Abstract summary: Decision diagrams are powerful tools to represent propositional formulas. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. We present a novel technique to leverage DDs to SMT level, which has several advantages.
• Score: 0.19285000127136376
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Decision diagrams (DDs) are powerful tools to represent effectively propositional formulas, which are largely used in many domains, in particular in formal verification and in knowledge compilation. Some forms of DDs (e.g., OBDDs, SDDs) are canonical, that is, (under given conditions on the atom list) they univocally represent equivalence classes of formulas. Given the limited expressiveness of propositional logic, a few attempts to leverage DDs to SMT level have been presented in the literature. Unfortunately, these techniques still suffer from some limitations: most procedures are theory-specific; some produce theory DDs (T-DDs) which do not univocally represent T-valid formulas or T-inconsistent formulas; none of these techniques provably produces theory-canonical T-DDs, which (under given conditions on the T-atom list) univocally represent T-equivalence classes of formulas. Also, these procedures are not easy to implement, and very few implementations are actually available. In this paper, we present a novel very-general technique to leverage DDs to SMT level, which has several advantages: it is very easy to implement on top of an AllSMT solver and a DD package, which are used as blackboxes; it works for every form of DDs and every theory, or combination thereof, supported by the AllSMT solver; it produces theory-canonical T-DDs if the propositional DD is canonical. We have implemented a prototype tool for both T-OBDDs and T-SDDs on top of OBDD and SDD packages and the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

Related papers

• 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. We propose Syzygy of Thoughts (SoT)-a novel framework that extends CoT by introducing auxiliary, interrelated reasoning paths. SoT captures deeper logical dependencies, enabling more robust and structured problem-solving.
  arXiv  Detail & Related papers  (2025-04-13T13:35:41Z)
• The role of slicing in test-driven development [39.01665062857323]
  Test-driven development (TDD) is a widely used agile practice. We propose a theoretical framework for TDD, with the following characteristics. We have checked the connections among TDD, contracts, and slices using a controlled experiment conducted in the industry.
  arXiv  Detail & Related papers  (2024-07-18T08:10:38Z)
• Partial-differential-algebraic equations of nonlinear dynamics by Physics-Informed Neural-Network: (I) Operator splitting and framework assessment [51.3422222472898]
  Several forms for constructing novel physics-informed-networks (PINN) for the solution of partial-differential-algebraic equations are proposed. Among these novel methods are the PDE forms, which evolve from the lower-level form with fewer unknown dependent variables to higher-level form with more dependent variables.
  arXiv  Detail & Related papers  (2024-07-13T22:48:17Z)
• A Formal Analysis of Iterated TDD [0.0]
  We formally analyze the software methodology called (iterated) Test Driven Development (TDD) We find a context in which iterated TDD provably produce'' provably correct code'' while being stable in terms of iterated code churns. We argue that the research finding of ineffective'' iterated TDD found by earlier researches are due to missing this context, while the findings of effective'' iterated TDD is due to accidentally falling into the context or simply placebo.
  arXiv  Detail & Related papers  (2024-07-04T08:07:35Z)
• Disperse-Then-Merge: Pushing the Limits of Instruction Tuning via Alignment Tax Reduction [75.25114727856861]
  Large language models (LLMs) tend to suffer from deterioration at the latter stage ofSupervised fine-tuning process. We introduce a simple disperse-then-merge framework to address the issue. Our framework outperforms various sophisticated methods such as data curation and training regularization on a series of standard knowledge and reasoning benchmarks.
  arXiv  Detail & Related papers  (2024-05-22T08:18:19Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARD is a framework that masters uniform synthesis of theorem and proof data of high quality and diversity. We present a theorem-and-proof benchmark MUSTARDSAUCE with 5,866 valid data points. We perform extensive analysis and demonstrate that MUSTARD generates validated high-quality step-by-step data.
  arXiv  Detail & Related papers  (2024-02-14T05:57:58Z)
• MDD-UNet: Domain Adaptation for Medical Image Segmentation with Theoretical Guarantees, a Proof of Concept [3.376269351435396]
  We propose an unsupervised domain adaptation framework for U-Nets with theoretical guarantees. We find that the MDD-UNet is able to learn features which are domain-invariant with no knowledge about the labels in the target domain. This work serves as a proof of concept by demonstrating an improvement on the U-Net in it's standard form without modern enhancements.
  arXiv  Detail & Related papers  (2023-12-19T15:30:10Z)
• 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)
• AdaNPC: Exploring Non-Parametric Classifier for Test-Time Adaptation [64.9230895853942]
  Domain generalization can be arbitrarily hard without exploiting target domain information. Test-time adaptive (TTA) methods are proposed to address this issue. In this work, we adopt Non-Parametric to perform the test-time Adaptation (AdaNPC)
  arXiv  Detail & Related papers  (2023-04-25T04:23:13Z)
• 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)
• Belief Revision in Sentential Decision Diagrams [126.94029917018733]
  We develop a general revision algorithm for SDDs based on a syntactic characterisation of Dalal revision. Preliminary experiments performed with randomly generated knowledge bases show the advantages of directly perform revision within SDD formalism.
  arXiv  Detail & Related papers  (2022-01-20T11:01:41Z)
• Variable Shift SDD: A More Succinct Sentential Decision Diagram [10.91026094237478]
  Sentential Decision Diagram (SDD) is a tractable representation of Boolean functions. We propose a more succinct variant of SDD named Variable Shift SDD (VS-SDD) We show that VS-SDDs are never larger than SDDs and there are cases in which the size of a VS-SDD is exponentially smaller than that of an SDD.
  arXiv  Detail & Related papers  (2020-04-06T09:18:19Z)

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.