As quantum technology advances, the efficient design of quantum circuits has become an important area of research. This paper provides an introduction to the MCT quantum circuit design problem for reversible Boolean functions with the necessary background in quantum computing to comprehend the problem. While this is a well-studied problem, optimization models that minimize the true objective have only been explored recently. This paper introduces a new optimization model and symmetry-breaking constraints that improve solving time by up to two orders of magnitude compared to earlier work when a Constraint Programming solver is used. Experiments with up to seven qubits and using up to 15 quantum gates result in several new best-known circuits, obtained by any method, for well-known benchmarks. Several in-depth analyses are presented to validate the effectiveness of the symmetry-breaking constraints from multiple perspectives. Finally, an extensive comparison with other approaches shows that optimization models may require more time but can provide superior circuits with optimality guarantees.
Essence is a constraint language for specifying combinatorial problems. It is designed to be significantly more abstract than constraint modelling languages currently in use. The first full description of the language and its design rationale was published in Constraints in 2008. This paper, written to mark the 30th anniversary of the journal, describes the history of the development of Essence, summarises developments since publication and provides some afterthoughts.
This article is a retrospective look at practical applications of constraint programming following up on the original article published in 1996.
An a posteriori revisit of the accumulated results on the Semiring and Valued constraint satisfaction problems and related problems, showing how semi-rings and monoids (or semi-groups) are useful objects to explore the intricate interplay between expressivity and the design of efficient, correct and convergent algorithms in computer science, showing tight relationships and scientific overlaps with probabilistic reasoning over graphical structures and linear or polynomial discrete mathematical programming.
This paper revisits the paper on solving hard temporal reasoning problems, uncovers the motivations behind the paper, puts the results in perspective, and reports on rerunning some of the empirical evaluations thirty years later.
We consider decision-making problems in which there are both “hard” constraints that must be satisfied and “soft” constraints that the decision-maker would like to satisfy. When no feasible solution exists that satisfies all of the soft constraints, the decision-maker must choose which of these to enforce and which to violate while still ensuring that all of the hard constraints remain satisfied. Enumerating all minimally infeasible and maximally feasible subsets of the soft constraints can assist in making an informed decision, but generating these sets can be a time-intensive process. We propose two enhancements to a known algorithm for generating these sets and evaluate their computational impact on a collection of real-world problems from a healthcare setting.
MD5, SHA-1, and SHA-256 are fundamental cryptographic hash functions that produce a hash of fixed size given a message of arbitrary finite size. Their core components are compression functions. The MD5 compression function operates in 4 rounds of 16 steps each, while that of SHA-1 and SHA-256 operate in 80 and 64 rounds, respectively. It is computationally infeasible to invert these compression functions, i.e., to find an input given an output. In 2012, 28-step MD5, 23-round SHA-1, and 16-round SHA-256 compression functions were reduced to SAT and inverted by Conflict-Driven Clause Learning solvers, yet no progress in this area has been made since then. The present paper proposes to construct intermediate inverse problems for any pair of MD5 steps (i,i+1) such that the first problem is very close to inverting i steps, while the last one is almost inverting i+1 steps. The same idea works for a pair of sequential rounds in case of SHA-1 and SHA-256. SAT encodings of intermediate problems for MD5, SHA-1, and SHA-256 were constructed, and then a Conflict-Driven Clause Learning solver was parameterized on the simplest of them. The parameterized solver was used to design a parallel Cube-and-Conquer solver that for the first time inverted 29-step MD5, 24-round SHA-1, and 19-round SHA-256 compression functions.
We investigate using Constraint Programming (CP) and Domain-Independent Dynamic Programming (DIDP) to solve the master problem in Logic-based Benders Decomposition (LBBD) models, focusing on the challenge of feasibility cut formulation. For CP, we exploit variable assignment bounds, variable assignment counting, and global constraints to construct three combinatorial cut encodings. For the state-based DIDP model, we propose two cut encoding approaches: using additional preconditions of state transitions or adding state constraints. Each of these approaches can be modeled using integer numeric variables or set variables, resulting in four novel encodings. We apply the three CP variants and four DIDP variants to the LBBD model of the simple assembly line balancing problems with sequence-dependent setup times type-1 (SUALBP-1). Experimental results show all approaches outperform a mixed-integer programming (MIP) based master problem and the state-of-the-art monolithic MIP model, with the three CP variants being superior to all of the DIDP approaches. Though the evaluation is specific to SUALBP-1, the proposed approaches can be used for other problems where LBBD with feasibility cuts is applicable.
Object-oriented programming is the dominant paradigm for general-purpose programming languages. While several attempts have been made to introduce object models into constraint modelling languages, these often have restrictions in terms of their expressivity, are not available in mainstream modelling languages, or are incompatible with modern solving technology. To address these challenges, this paper identifies essential requirements for expressive and elegant object-oriented constraint modelling. We propose an object model that supports decision variables of object type, objects referring to other objects, and, crucially, variable sets of objects, whose cardinality is decided by the solver. The object model is presented as an extension of the MiniZinc modelling language that can be translated into standard MiniZinc. A number of examples and a case study demonstrate the viability of the approach.
We consider a product configuration problem for high-performance pumps and valves, where feasible configurations are defined by restriction tables. For this problem we propose a Constraint Programming based model to find preferred solutions and to detect conflicts. We introduce an algorithm for enumerating minimal conflicts and their resolutions. The paper highlights two primary use cases: assisting sales personnel to resolve conflicts that arise during product configuration when not all the customer requirements can be met simultaneously and aiding product modelers in structuring and validating product models by finding the source of unexpected conflicts. The study also explores model preprocessing techniques to improve the solver performance. The algorithm is shown to be well suited for both real-time decision support and in-depth product model analysis in the cases at hand; the computational results demonstrate the practical applicability of the approach.
We propose a new automata-based algorithm for solving string constraints that tightly integrates reasoning about equations and regular constraints. Exchanging information between the two allows an efficient pruning of generated combinatorial cases. The algorithm is based on a novel language-based characterization of satisfiability of word equations with regular constraints. Namely, satisfiability of an equation is implied by its stability: the concatenation of the regular languages constraining variables on the left-hand side equals the concatenation of the languages on the right-hand side. It is complete for the chain-free string constraints. We experimentally show that our prototype implementation is competitive with the best string solvers and even superior on difficult examples.
In a polydiagonal subspace of the Euclidean space, certain components of the vectors are equal (synchrony) or opposite (anti-synchrony). Polydiagonal subspaces invariant under a matrix have many applications in graph theory and dynamical systems, especially coupled cell networks. We describe invariant polydiagonal subspaces in terms of coloring vectors. This approach gives an easy formulation of a constraint satisfaction problem for finding invariant polydiagonal subspaces. Solving the resulting problem with existing state-of-the-art constraint solvers greatly outperforms the currently known algorithms.
In Mathematical Music theory, the Aperiodic Tiling Complements Problem consists in finding all the possible aperiodic complements of a given rhythm A. The complexity of this problem depends on the size of the period n of the canon and on the cardinality of the given rhythm A. The current state-of-the-art algorithms can solve instances with n smaller than 180 . In this paper, we propose an ILP formulation and a SAT Encoding to solve this mathemusical problem, and we use the Maplesat solver to enumerate all the aperiodic complements. We then enhance the SAT model in two different ways. First, we enforce the SAT model with a set of clauses that retrieves the solutions up to translation. Second, we propose a decomposition of the solution space that allows to parallelize the resolution of the problem. We validate our different models using several different periods and rhythms and we compute for the first time the complete list of aperiodic tiling complements of standard Vuza rhythms for canons with period n = { 180, 420, 900 } .
Solving constraint satisfaction problems often involves a large amount of redundant exploration stemming from the existence of subproblems whose information can be reused for other subproblems. Subproblem dominance is a general notion of reusability that arises when one subproblem imposes more constraints on the remaining part of the search than another subproblem and allows the search to reuse the solutions of the dominating subproblem for the dominated subproblem. The search can exploit subproblem dominance by storing the subproblems that have been explored in a cache and abandoning the current subproblem whenever the cache contains a subproblem that dominates it. While using caching makes it possible to solve problems where subproblem dominance arises orders of magnitude faster, storing all of these subproblems can require a substantial amount of memory, making it impractical in many cases. This paper analyses the dominance between different subproblems for various constraint problems, revealing that only a relatively small number of subproblems dominate other subproblems. Based on these findings, two types of strategies are proposed for reducing the number of subproblems stored in the cache: limiting the number of subproblems that can be stored in the cache and periodically cleaning up the cache. An experimental evaluation demonstrates that these strategies provide an effective instrument for reducing the memory consumption of caching, allowing it to be used on a larger scale. However, there is a trade-off between saving memory and reducing redundant exploration, as removing subproblems from the cache may prevent dominance from being detected for certain subproblems.
We consider the problem of perception-based constraint solving, where part of the problem specification is provided indirectly through an image provided by a user. As a pedagogical example, we use the complete image of a Sudoku grid. While the rules of the puzzle are assumed to be known, the image must be interpreted by a neural network to extract the values in the grid. In this paper, we investigate (1) a hybrid modeling approach combining machine learning and constraint solving for joint inference, knowing that blank cells need to be both predicted as being blank and filled-in to obtain a full solution; (2) the effect of classifier calibration on joint inference; and (3) how to deal with cases where the constraints of the reasoning system are not satisfied. More specifically, in the case of handwritten user errors in the image, a naive approach fails to obtain a feasible solution even if the interpretation is correct. Our framework identifies human mistakes by using a constraint solver and helps the user to correct these mistakes. We evaluate the performance of the proposed techniques on images taken through the Sudoku Assistant Android app, among other datasets. Our experiments show that (1) joint inference can correct classifier mistakes, (2) overall calibration improves the solution quality on all datasets, and (3) estimating and discriminating between user-written and original visual input while reasoning makes for a more robust system, even in the presence of user errors.
In recent years, pattern mining has evolved from a slow-moving, repetitive three-step process to a much more agile and iterative/user-centric mining model. A crucial element of this framework is the capability to rapidly provide a set of diverse patterns to the user. This paper proposes a pattern mining approach based on constraint programming that incorporates a non-redundancy/diversity constraint into closed pattern enumeration. The level of diversity is controlled through a threshold on the maximum pairwise Jaccard similarity of pattern occurrences. We show that the Jaccard measure does not have nice (anti-)monotonicity properties w.r.t. the general-to-specific enumeration. To address this limitation, we propose anti-monotonic lower and upper-bound relaxations of the Jaccard similarity with nice pruning-enabling properties, and connect the final results to the original Jaccard Index. To evaluate the effectiveness of our relaxations, we conduct a comprehensive comparison against several existing pattern mining techniques designed to control redundancy. Experimental results illustrate that our approach provides an effective solution for mining diverse itemsets, showing competitive performance in both runtime and flexibility.
We study a planning problem based on Plotting, a tile-matching puzzle video game published by Taito in 1989. The objective of this turn-based game is to remove a target number of coloured blocks from a grid by sequentially shooting blocks into the same grid. Plotting features complex transitions after every shot: various blocks are affected directly, while others can be indirectly affected by gravity. We consider modelling and solving Plotting from two perspectives. The puzzle is naturally cast as an AI Planning problem and we first discuss modelling the problem using the Planning Domain Definition Language (PDDL). We find that a model in which planning actions correspond to player actions is inefficient with a grounding-based state-of-the-art planner. However, with a more fine-grained action model, where each change of a block is a planning action, solving performance is dramatically improved. We also describe two lifted constraint models, able to capture the inherent complexities of Plotting and enabling the application of efficient solving approaches from SAT and CP. Our empirical results with these models demonstrates that they can compete with, and often exceed, the performance of the dedicated planning solvers, suggesting that the richer languages available to constraint modelling can be of benefit when considering planning problems with complex changes of state. CP and SAT solvers solved almost all of the largest and most challenging instances within 1 hour, whereas the best planning approach solved approximately 30%. Finally, the flexibility provided by the constraint models allows us to easily curate interesting levels for human players.
We lift the problem of enumerative solution counting to quantified Boolean formulas (QBFs) at the second quantifier block. In contrast to the well-explored model counting problem for SAT (#SAT), where models are simply assignments to the Boolean variables of a formula, we are now dealing with tree (counter-)models reflecting the dependencies between the variables of the first and the second quantifier block. It turns out that enumerative counting on the second level does not give the complete solution count and more fine-grained view is necessary. We present a level-2 solution counting approach that works for true and false formulas. We implemented the presented approach in a counting tool exploiting state-of-the-art QBF solving technology. We present several kinds of benchmarks for testing our implementation and show that even with this very basic approach of solution enumeration the solution counts of challenging benchmarks can be found.
We develop and deploy a set of constraints for the purpose of calculating minimal sizes of lottery designs. Specifically, we find the minimum number of tickets of size six which are needed to match at least two balls on any draw of size six, whenever there are at most 70 balls.
