This paper investigates novel techniques to solve prime factorization by quantum annealing (QA). First, we present a very-compact modular encoding of a multiplier circuit into the 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 using 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 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 the experiments we introduced different approaches to initialize the multiplier qubits and adopted several performance enhancement techniques. Overall, 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; also, this is the largest number which was ever factorized by means of any quantum device without relying on external search or preprocessing procedures run on classical computers.
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, 749 × 251 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.
Optimization Modulo Theories (
OMT
) is an extension of SMT which allows for finding models that optimize given objectives.
OptiMathSAT
is an OMT solver which allows for solving a list of ...optimization problems on SMT formulas with linear objective functions—on the Boolean, the rational and the integer domains, and on their combination thereof—including (partial weighted)
MaxSMT
. Multiple and heterogeneous objective functions can be combined together and handled either independently, or lexicographically, or in linear or min–max /max–min combinations.
OptiMathSAT
provides an incremental interface, it supports both an extended version of the
SMT-LIBv2
language and a subset of the
FlatZinc
language, and can be interfaced via an API. In this paper we describe
OptiMathSAT
and its usage in full detail.
Weighted model integration (WMI) is a recent formalism generalizing weighted model counting (WMC) to run probabilistic inference over hybrid domains, characterized by both discrete and continuous ...variables and relationships between them. WMI is computationally very demanding as it requires to explicitly enumerate all possible truth assignments to be integrated over. Component caching strategies which proved extremely effective for WMC are difficult to apply in this formalism because of the tight coupling induced by the arithmetic constraints. In this paper we present a novel formulation of WMI, which allows to exploit the power of SMT-based predicate abstraction techniques in designing efficient inference procedures. A novel algorithm combines a strong reduction in the number of models to be integrated over with their efficient enumeration. Experimental results on synthetic and real-world data show drastic computational improvements over the original WMI formulation as well as existing alternatives for hybrid inference.
In the contexts of automated reasoning (AR) and formal verification (FV), important
decision
problems are effectively encoded into Satisfiability Modulo Theories (SMT). In the last decade, efficient ...SMT solvers have been developed for several theories of practical interest (e.g., linear arithmetic, arrays, and bit vectors). Surprisingly, little work has been done to extend SMT to deal with
optimization
problems; in particular, we are not aware of any previous work on SMT solvers able to produce solutions that minimize cost functions over
arithmetical
variables. This is unfortunate, since some problems of interest require this functionality.
In the work described in this article we start filling this gap. We present and discuss two general procedures for leveraging SMT to handle the minimization of linear rational cost functions, combining SMT with standard minimization techniques. We have implemented the procedures within the MathSAT SMT solver. Due to the absence of competitors in the AR, FV, and SMT domains, we have experimentally evaluated our implementation against state-of-the-art tools for the domain of
Linear Generalized Disjunctive Programming (LGDP)
, which is closest in spirit to our domain, on sets of problems that have been previously proposed as benchmarks for the latter tools. The results show that our tool is very competitive with, and often outperforms, these tools on these problems, clearly demonstrating the potential of the approach.
Optimization modulo theories (OMT) is an important extension of SMT which allows for finding models that optimize given objective functions, typically consisting in linear-arithmetic or ...Pseudo-Boolean terms. However, many SMT and OMT applications, in particular from SW and HW verification, require handling
bit-precise
representations of numbers, which in SMT are handled by means of the theory of bit-vectors (
B
V
) for the integers and that of floating-point numbers (
FP
) for the reals respectively. Whereas an approach for OMT with (unsigned)
B
V
objectives has been proposed by Nadel & Ryvchin, unfortunately we are not aware of any existing approach for OMT with
FP
objectives. In this paper we fill this gap, and we address for the first time
OMT
with
FP
objectives. We present a novel OMT approach, based on the novel concept of
attractor
and
dynamic attractor
, which extends the work of Nadel and Ryvchin to work with signed-
B
V
objectives and, most importantly, with
FP
objectives. We have implemented some novel
OMT
procedures on top of
OptiMathSAT
and tested them on modified problems from the SMT-LIB repository. The empirical results support the validity and feasibility of our novel approach.
Structured learning modulo theories Teso, Stefano; Sebastiani, Roberto; Passerini, Andrea
Artificial intelligence,
March 2017, 2017-03-00, 20170301, Volume:
244
Journal Article
Peer reviewed
Open access
Modeling problems containing a mixture of Boolean and numerical variables is a long-standing interest of Artificial Intelligence. However, performing inference and learning in hybrid domains is a ...particularly daunting task. The ability to model these kinds of domains is crucial in “learning to design” tasks, that is, learning applications where the goal is to learn from examples how to perform automatic de novo design of novel objects. In this paper we present Structured Learning Modulo Theories, a max-margin approach for learning in hybrid domains based on Satisfiability Modulo Theories, which allows to combine Boolean reasoning and optimization over continuous linear arithmetical constraints. The main idea is to leverage a state-of-the-art generalized Satisfiability Modulo Theory solver for implementing the inference and separation oracles of Structured Output SVMs. We validate our method on artificial and real world scenarios.
This book constitutes the refereed proceedings of the 15th International Conference on Theory and Applications of Satisfiability Testing, SAT 2012, held in Trento, Italy, in June 2012. The 29 revised ...full papers, 7 tool papers, and 16 poster papers presented together with 2 invited talks were carefully reviewed and selected from 112 submissions (88 full, 10 tool and 14 poster papers). The papers are organized in topical sections on stochastic local search, theory, quantified Boolean formulae, applications, parallel and portfolio approaches, CDCL SAT solving, MAX-SAT, cores interpolants, complexity analysis, and circuits and encodings.
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, characterized 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.
Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some theory or combination of theories; Verification Modulo Theories (VMT) ...is the problem of analyzing the reachability for transition systems represented in terms of SMT formulae. In this article, we tackle the problems of SMT and VMT over the theories of nonlinear arithmetic over the reals (NRA) and of NRA augmented with transcendental (exponential and trigonometric) functions (NTA).
We propose a new abstraction-refinement approach for SMT and VMT on NRA or NTA, called
Incremental Linearization
. The idea is to abstract nonlinear multiplication and transcendental functions as uninterpreted functions in an abstract space limited to linear arithmetic on the rationals with uninterpreted functions. The uninterpreted functions are incrementally axiomatized by means of upper- and lower-bounding piecewise-linear constraints. In the case of transcendental functions, particular care is required to ensure the soundness of the abstraction.
The method has been implemented in the M
ath
SAT SMT solver and in the
nu
X
mv
model checker. An extensive experimental evaluation on a wide set of benchmarks from verification and mathematics demonstrates the generality and the effectiveness of our approach.
PDF
