arXiv subjects

Giuseppe Spallitta

Publications and source records attributed to Giuseppe Spallitta.

12 recordsLinked to original sources

arXiv2026

Beyond Eager Encodings: A Theory-Agnostic Approach to Theory-Lemma Enumeration in SMT

Lifting Boolean-reasoning techniques to the SMT level most often requires producing theory lemmas that rule out theory-inconsistent truth assignments. With standard SMT solving, it is common to "lazily" generate such lemmas on demand during the search; with some harder SMT-level tasks -- such as unsat-core extraction, MaxSMT, T-OBDD or T-SDD compilation -- it may be beneficial or even necessary to "eagerly" pre-compute all the needed theory lemmas upfront. Whereas in principle "classic" eager SMT encodings could do the job, they are specific for very few and easy theories, they do not comply with theory combination, and may produce lots of unnecessary lemmas. In this paper, we present theory-agnostic methods for enumerating complete sets of theory lemmas tailored to a given formula. Starting from AllSMT as a baseline approach, we propose improved lemma-enumeration techniques, including divide&conquer, projected enumeration, and theory-driven partitioning, which are highly parallelizable and which may drastically improve scalability. An experimental evaluation demonstrates that these techniques significantly enhance efficiency and enable the method to scale to substantially more complex instances.

cs.LO↗

arXiv2026

Extending CDCL-based Model Enumeration with Weights

In this work we investigate Weighted Model Enumeration (WME): given a Boolean formula and a weight function over its satisfying assignments, enumerate models while accounting for their weights. This setting supports weight-driven queries, such as producing the top-k models or all models above a threshold. While related to AllSAT, Weighted Model Counting, and MaxSAT, these paradigms do not treat selective enumeration under weights as a native solver task. We present CDCL-based algorithms for WME that integrate weight propagation, weight-based pruning, and weight-aware conflict analysis into both chronological and non-chronological backtracking frameworks. Chronological backtracking exploits implicit blocking and keeps the clause database compact, thereby reducing memory footprint and enabling efficient propagation. In contrast, non-chronological backtracking with clause learning supports explicit blocking and restarts. We show that both approaches are feasible and complementary, highlighting trade-offs in pruning effectiveness with weights and clarifying when each performs best.

cs.LO↗

arXiv2026

Computing Short SAT Implicants via Ising/QUBO Encodings

Many reasoning tasks require short partial satisfying assignments (implicants), sometimes focusing on a set of important variables. SAT-to-Ising-QUBO formulations are implicitly designed so that ground states correspond to total assignments, since the Ising/QUBO model assigns a value to every spin and has no native representation of unassigned variables. We introduce an Ising/QUBO framework that incorporates "don't-care" semantics into the quadratic model via a dual-polarity representation, enabling the retrieval of short implicants. The encoding supports implicant shrinking and projection through minor objective modifications. We provide parameter regimes under which ground states correspond to short partial satisfying assignments, achieving minimality and, when the quadratic penalty function permits, minimum-cardinality. We empirically evaluate the encoding with simulated annealing on random 3-SAT enumeration benchmarks and non-CNF formulas, showing that it leaves about one-third of variables unassigned on random 3-SAT formulas while preserving satisfiability, and that consecutive polarity-freezing rounds achieve minimality (and minimum-cardinality) with high probability.

cs.LO↗

arXiv2026

d-DNNF Modulo Theories: A General Framework for Polytime SMT Queries

In Knowledge Compilation (KC) a propositional knowledge base is compiled off-line into some target form, typically into deterministic decomposable negation normal form (d-DNNF) or one of its subcases, which is then used on-line to answer a large number of queries in polytime, such as clausal entailment, model counting, and others. The general idea is to push as much of the computational effort into the off-line compilation phase, which is amortized over all on-line polytime queries. In this paper, we present for the first time a novel and general technique to leverage d-DNNF compilation and querying to SMT level. Intuitively, before d-DNNF compilation, the input SMT formula is combined with a list of pre-computed ad-hoc theory lemmas, so that the queries at SMT level reduce to those at propositional level. This approach has several features: (i) it works for every theory, or theory combination thereof; (ii) it works for all forms of d-DNNF; (iii) it is easy to implement on top of any d-DNNF compiler and any theory-lemma enumerator, which are used as black boxes; (iv) most importantly, these compiled SMT d-DNNFs can be queried in polytime by means of a standard propositional d-DNNF reasoner. As proof of concept, we have implemented a tool on top of state-of-the-art d-DNNF packages and of the MathSAT SMT solver. Some preliminary empirical evaluation supports the effectiveness of the approach.

cs.LO↗

arXiv2025

On CNF Conversion for SAT and SMT Enumeration

Modern SAT and SMT solvers are designed to handle problems expressed in Conjunctive Normal Form (CNF) so that non-CNF problems must be CNF-ized upfront, typically by using variants of either Tseitin or Plaisted and Greenbaum transformations. When passing from plain solving to enumeration, however, the capability of producing partial satisfying assignments that are as small as possible becomes crucial, which raises the question of whether such CNF encodings are also effective for enumeration. In this paper, we investigate both theoretically and empirically the effectiveness of CNF conversions for SAT and SMT enumeration. On the negative side, we show that: (i) Tseitin transformation prevents the solver from producing short partial assignments, thus seriously affecting the effectiveness of enumeration; (ii) Plaisted and Greenbaum transformation overcomes this problem only in part. On the positive side, we prove theoretically and we show empirically that combining Plaisted and Greenbaum transformation with NNF preprocessing upfront -- which is typically not used in solving -- can fully overcome the problem and can drastically reduce both the number of partial assignments and the execution time.

cs.LO↗

arXiv2024

Disjoint Projected Enumeration for SAT and SMT without Blocking Clauses

All-Solution Satisfiability (AllSAT) and its extension, All-Solution Satisfiability Modulo Theories (AllSMT), have become more relevant in recent years, mainly in formal verification and artificial intelligence applications. The goal of these problems is the enumeration of all satisfying assignments of a formula (for SAT and SMT problems, respectively), making them useful for test generation, model checking, and probabilistic inference. Nevertheless, traditional AllSAT algorithms face significant computational challenges due to the exponential growth of the search space and inefficiencies caused by blocking clauses, which cause memory blowups and degrade unit propagation performances in the long term. This paper presents two novel solvers: tabularAllSAT, a projected AllSAT solver, and tabularAllSMT, a projected AllSMT solver. Both solvers combine Conflict-Driven Clause Learning (CDCL) with chronological backtracking to improve efficiency while ensuring disjoint enumeration. To retrieve compact partial assignments we propose a novel aggressive implicant shrinking algorithm, compatible with chronological backtracking, to minimize the number of partial assignments, reducing overall search complexity. Furthermore, we extend the solver framework to handle projected enumeration and SMT formulas effectively and efficiently, adapting the baseline framework to integrate theory reasoning and the distinction between important and non-important variables. An extensive experimental evaluation demonstrates the superiority of our approach compared to state-of-the-art solvers, particularly in scenarios requiring projection and SMT-based reasoning.

cs.LO↗

arXiv2024

Canonical Decision Diagrams Modulo Theories

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.

cs.LO↗

arXiv2024

Experimenting with D-Wave Quantum Annealers on Prime Factorization problems

This paper builds on top of a paper we have published very recently, in which we have proposed a novel approach to prime factorization (PF) by quantum annealing, where 8,219,999=32,749x251 was the highest prime product we were able to factorize -- which, to the best of our knowledge is the largest number which was ever factorized by means of a quantum device. The series of annealing experiments which led us to these results, however, did not follow a straight-line path; rather, they involved a convoluted trial-and-error process, full of failed or partially-failed attempts and backtracks, which only in the end drove us to find the successful annealing strategies. In this paper, we delve into the reasoning behind our experimental decisions and provide an account of some of the attempts we have taken before conceiving the final strategies that allowed us to achieve the results. This involves also a bunch of ideas, techniques, and strategies we investigated which, although turned out to be inferior wrt. those we adopted in the end, may instead provide insights to a more-specialized audience of D-Wave users and practitioners. In particular, we show the following insights: ($i$) different initialization techniques affect performances, among which flux biases are effective when targeting locally-structured embeddings; ($ii$) chain strengths have a lower impact in locally-structured embeddings compared to problem relying on global embeddings; ($iii$) there is a trade-off between broken chain and excited CFAs, suggesting an incremental annealing offset remedy approach based on the modules instead of single qubits. Thus, by sharing the details of our experiences, we aim to provide insights into the evolving landscape of quantum annealing, and help people access and effectively use D-Wave quantum annealers.

quant-ph↗

arXiv2024

Enhancing SMT-based Weighted Model Integration by Structure Awareness

The development of efficient exact and approximate algorithms for probabilistic inference is a long-standing goal of artificial intelligence research. Whereas substantial progress has been made in dealing with purely discrete or purely continuous domains, adapting the developed solutions to tackle hybrid domains, characterised by discrete and continuous variables and their relationships, is highly non-trivial. Weighted Model Integration (WMI) recently emerged as a unifying formalism for probabilistic inference in hybrid domains. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in drastic computational savings. Additionally, we show how SMT-based approaches can seamlessly deal with different integration techniques, both exact and approximate, significantly expanding the set of problems that can be tackled by WMI technology. An extensive experimental evaluation on both synthetic and real-world datasets confirms the substantial advantage of the proposed solution over existing alternatives. The application potential of this technology is further showcased on a prototypical task aimed at verifying the fairness of probabilistic programs.

cs.AI↗

arXiv2024

Disjoint Partial Enumeration without Blocking Clauses

A basic algorithm for enumerating disjoint propositional models (disjoint AllSAT) is based on adding blocking clauses incrementally, ruling out previously found models. On the one hand, blocking clauses have the potential to reduce the number of generated models exponentially, as they can handle partial models. On the other hand, the introduction of a large number of blocking clauses affects memory consumption and drastically slows down unit propagation. We propose a new approach that allows for enumerating disjoint partial models with no need for blocking clauses by integrating: Conflict-Driven Clause-Learning (CDCL), Chronological Backtracking (CB), and methods for shrinking models (Implicant Shrinking). Experiments clearly show the benefits of our novel approach.

cs.LO↗

arXiv2023

Effective Prime Factorization via Quantum Annealing by Modular Locally-structured Embedding

This paper investigates novel techniques to solve prime factorization by quantum annealing (QA). Our contribution is twofold. First, we present a novel and very compact modular encoding of a binary multiplier circuit into the Pegasus architecture of current D-Wave QA devices. The key contribution is a compact encoding of a controlled full-adder into an 8-qubit module in the Pegasus topology, which we synthesized offline by means of Optimization Modulo Theories. This allows us to encode up to a 21*12-bit multiplier (and a 22*8-bit one) into the Pegasus 5760-qubit topology of current annealers. To the best of our knowledge, these are the largest factorization problems ever encoded into a quantum annealer. Second, we have investigated the problem of actually solving encoded PF problems by running an extensive experimental evaluation on a D-Wave Advantage 4.1 quantum annealer. In order to help the annealer in reaching the global minimum, in the experiments we introduced different approaches to initialize the multiplier qubits and adopted several performance enhancement techniques. Overall, exploiting all the encoding and solving techniques described in this paper, 8, 219, 999 = 32, 749 * 251 was the highest prime product we were able to factorize within the limits of our QPU resources. To the best of our knowledge, this is the largest number which was ever factorized by means of a quantum annealer, and, more generally, by a quantum device.

quant-ph↗

arXiv2022

SMT-based Weighted Model Integration with Structure Awareness

Weighted Model Integration (WMI) is a popular formalism aimed at unifying approaches for probabilistic inference in hybrid domains, involving logical and algebraic constraints. Despite a considerable amount of recent work, allowing WMI algorithms to scale with the complexity of the hybrid problem is still a challenge. In this paper we highlight some substantial limitations of existing state-of-the-art solutions, and develop an algorithm that combines SMT-based enumeration, an efficient technique in formal verification, with an effective encoding of the problem structure. This allows our algorithm to avoid generating redundant models, resulting in substantial computational savings. An extensive experimental evaluation on both synthetic and real-world datasets confirms the advantage of the proposed solution over existing alternatives.

cs.AI↗