Don’t care in SMT: building flexible yet efficient abstraction/refinement solvers

This paper describes a method for combining “off-the-shelf” SAT and constraint solvers for building an efficient Satisfiability Modulo Theories (SMT) solver for a wide range of theories. Our method follows the abstraction/refinement approach to simplify the implementation of custom SMT solvers. The expected performance penalty by not using an interweaved combination of SAT and theory solvers is reduced by generalising a Boolean solution of an SMT problem first via assigning don’t care to as many variables as possible. We then use the generalised solution to determine a thereby smaller constraint set to be handed over to the constraint solver for a background theory. We show that for many benchmarks and real-world problems, this optimisation results in considerably smaller and less complex constraint problems. The presented approach is particularly useful for assembling a practically viable SMT solver quickly, when neither a suitable SMT solver nor a corresponding incremental theory solver is available. We have implemented our approach in the ABsolver framework and applied the resulting solver successfully to an industrial case-study: the verification problems arising in verifying an electronic car steering control system impose non-linear arithmetic constraints, which do not fall into the domain of any other available solver.     

Evaluating ASP and Commercial Solvers on the CSPLib

This paper deals with four solvers for combinatorial problems: the commercial state-of-the-art solver ILOG oplstudio, and the research answer set programming (ASP) systems dlv, smodels and cmodels. The first goal of this research is to evaluate the relative performance of such systems when used in a purely declarative way, using a reproducible and extensible experimental methodology. In particular, we consider a third-party problem library, i.e., the CSPLib, and uniform rules for modelling and instance selection. The second goal is to analyze the marginal effects of popular reformulation techniques on the various solving technologies. In particular, we consider structural symmetry breaking, the adoption of global constraints, and the addition of auxiliary predicates. Finally, we evaluate, on a subset of the problems, the impact of numbers and arithmetic constraints on the different solving technologies. Results show that there is not a single solver winning on all problems, and that reformulation is almost always beneficial: symmetry-breaking may be a good choice, but its complexity has to be carefully chosen, by taking into account also the particular solver used. Global constraints often, but not always, help opl, and the addition of auxiliary predicates is usually worth, especially when dealing with ASP solvers. Moreover, interesting synergies among the various modelling techniques exist.     

Interval propagation to reason about sets: Definition and implementation of a practical language

Local consistency techniques have been introduced in logic programming in order to extend the application domain of logic programming languages. The existing languages based on these techniques consider arithmetic constraints applied to variables ranging over finite integer domains. This makes difficult a natural and concise modelling as well as an efficient solving of a class of NP-complete combinatorial search problems dealing with sets. To overcome these problems, we propose a solution which consists in extending the notion of integer domains to that of set domains (sets of sets). We specify a set domain by an interval whose lower and upper bounds are known sets, ordered by set inclusion. We define the formal and practical framework of a new constraint logic programming language over set domains, called Conjunto. Conjunto comprises the usual set operation symbols (, , \), and the set inclusion relation (% MathType!MTEF!2!1!+-% feaafiart1ev1aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn% hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr% 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9% vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x% fr-xb9adbaqaaeaacaGaaiaabeqaamaabaabaaGcbaGaeyOHI0maaa!37EA!\[ \subseteq \]). Set expressions built using the operation symbols are interpreted as relations (s s ₁ = s ₂, ...). In addition, Conjunto provides us with a set of constraints called graduated constraints (e.g. the set cardinality) which map sets onto arithmetic terms. This allows us to handle optimization problems by applying a cost function to the quantifiable, i.e., arithmetic, terms which are associated to set terms. The constraint solving in Conjunto is based on local consistency techniques using interval reasoning which are extended to handle set constraints. The main contribution of this paper concerns the formal definition of the language and its design and implementation as a practical language.     

Solving finite domain constraint hierarchies by local consistency and tree search

We provide a reformulation of the constraint hierarchies (CHs) framework based on the notion of error indicators. Adapting the generalised view of local consistency in semiring-based constraint satisfaction problems, we define constraint hierarchy k-consistency (CH-k-C) and give a CH-2-C enforcement algorithm. We demonstrate how the CH-2-C algorithm can be seamlessly integrated into the ordinary branch-and-bound algorithm to make it a finite domain (FD) CH solver. Experimentation confirms the efficiency and robustness of our proposed solver prototype. Unlike other FD CH solvers, our proposed method works for both local and global comparators. In addition, our solver can support arbitrary error functions.     

Compile-time analysis of nonlinear constraints in CLPR

Solving nonlinear constraints over real numbers is a complex problem. Hence constraint logic programming languages like CLPR or Prolog III solve only linear constraints and delay nonlinear constraints until they become linear. This efficient implementation method has the disadvantage that sometimes computed answers are unsatisfiable or infinite loops occur due to the unsatisfiability of delayed nonlinear constraint These problems could be solved by using a more powerful constraint solver which can deal with nonlinear constraints like in RISC-CLP(Real). Since such powerful constraint solvers are not very efficient, we propose a compromise between these two extremes. We characterize a class of CLPR programs for which all delayed nonlinear constraints become linear at run time. Programs belonging to this class can be safely executed with the efficient CLPR method while the remaining programs need a more powerful constraint solver. This paper is an extended and revised version of Ref. 12). The research described in this paper was made during the author’s stay at the Max-planck-Institut für Informatik in Saarbrücken, Germany. It was supported in part by the German Ministry for Research and Technology (BMFT) under grant ITS 9103 and by the ESPRIT Basic Research Working Group 6028 (Construction of Computational Logics). The responsibility for the contents of this publication lies with the author.     

Extending SMT solvers with support for finite domain <Literal>alldifferent</Literal> constraint

In this paper we consider integration of SMT solvers with the filtering algorithms for the finite domain alldifferent constraint. Such integration makes SMT solvers suitable for solving constraint satisfaction problems with the alldifferent constraint involved. First, we present a novel algorithm for explaining inconsistencies and propagations in the alldifferent constraint. We compare it to Katsirelos’ algorithm and flow-based algorithms that are commonly used for that purpose. Then we describe our DPLL(T)-compliant SMT theory solver for constraint satisfaction problems that include alldifferent constraints. We also provide an experimental evaluation of our approach.     

Weight constraint programs with evaluable functions

In the current practice of Answer Set Programming (ASP), evaluable functions are represented as special kinds of relations. This often makes the resulting program unnecessarily large when instantiated over a large domain. The extra constraints needed to enforce the relation as a function also make the logic program less transparent. In this paper, we consider adding evaluable functions to answer set logic programs. The class of logic programs that we consider here is that of weight constraint programs, which are widely used in ASP. We propose an answer set semantics to these extended weight constraint programs and define loop completion to characterize the semantics. Computationally, we provide a translation from loop completions of these programs to instances of the Constraint Satisfaction Problem (CSP) and use the off-the-shelf CSP solvers to compute the answer sets of these programs. A main advantage of this approach is that global constraints implemented in such CSP solvers become available to ASP. The approach also provides a new encoding for CSP problems in the style of weight constraint programs. We have implemented a prototype system based on these results, and our experiments show that this prototype system competes well with the state-of-the-art ASP solvers. In addition, we illustrate the utilities of global constraints in the ASP context.     

Automated String Constraints Solving for Programs Containing String Manipulation Functions

The ability to solve various constraints is a principal factor of automatic constraint solvers. Most object-oriented languages treat a character string as a primitive data type which is manipulated by string library functions. Most constraint solvers have limitations on their input constraints, such as strong restrictions on the expressiveness of constraints or lack of the ability to solve hybrid constraints. These limitations hinder applying automated constraint solvers on program analysis techniques for programs containing strings and string manipulation functions. We propose an approach to automatically solve program constraints involving strings and string manipulation functions. Based on the character array model, we design a constraint language which contains primitive operations to precisely describe the constraints of commonly used string manipulation functions. The translated string constraints together with numeric constraints are then solved by a two-phase test generation procedure: firstly, a partial solution is obtained to satisfy the arithmetic constraints of the position variables, and the solution is utilized to simplify the string constraints into pure character array constraints; secondly, the pure array constraints are solved by an off-the-shelf array-specific theory based constraint solver. We integrate the approach into an automated testing tool to support the generation of string test cases, and then perform experiments. The results of the experiments prove that the integration of the proposed approach promotes the testing coverage of the existing testing tool, and the integrated tool has an advantage of handling specific string manipulation functions compared with an existing string solver.     

Reasoning on constraints in CLP(FD)

Constraint Logic Programming solvers on finite domains (CLP(FD) solvers) use constraints to prune those combinations of assignments which cannot appear in any consistent solution. There are applications, such as temporal reasoning or scheduling, requiring some form of qualitative reasoning where constraints can be changed (restricted) during the computation or even chosen when disjunction occurs. We embed in a (CLP(FD) solver the concept of constraints as first class objects. In the extended language, variables range over finite domains of objects (e.g., integers) and relation variables range over finite domains of relation symbols. We define operations and constraints on the two sorts of variables and one constraint linking the two. We first present the extension as a general framework, then we propose two specializations on finite domains of integers and of sets. Programming examples are given, showing the advantages of the extension proposed from both a knowledge representation and an operational viewpoint.     

Acquiring Both Constraint and Solution Preferences in Interactive Constraint Systems

Constraints are useful to model many real-life problems. Soft constraints are even more useful, since they allow for the use of preferences, which are very convenient in many real-life problems. In fact, most problems cannot be precisely defined by using hard constraints only.However, soft constraint solvers usually can only take as input preferences over constraints, or variables, or tuples of domain values. On the other hand, it is sometimes easier for a user to state preferences over entire solutions of the problem.In this paper, we define an interactive framework where it is possible to state preferences both over constraints and over solutions, and we propose a way to build a system with such features by pairing a soft constraint solver and a learning module, which learns preferences over constraints from preferences over solutions. We also describe a working system which fits our framework, and uses a fuzzy constraint solver and a suitable learning module to search a catalog for the best products that match the user's requirements.     

Implementing logical connectives in constraint programming

Combining constraints using logical connectives such as disjunction is ubiquitous in constraint programming, because it adds considerable expressive power to a constraint language. We explore the solver architecture needed to propagate such combinations of constraints efficiently. In particular we describe two new features named satisfying sets and constraint trees. We also make use of movable triggers (Gent et al., 2006) [1], and with these three complementary features we are able to make considerable efficiency gains.A key reason for the success of Boolean Satisfiability (SAT) solvers is their ability to propagate Or constraints efficiently, making use of movable triggers. We successfully generalise this approach to an Or of an arbitrary set of constraints, maintaining the crucial property that at most two constraints are active at any time, and no computation at all is done on the others. We also give an And propagator within our framework, which may be embedded within the Or. Using this approach, we demonstrate speedups of over 10,000 times in some cases, compared to traditional constraint programming approaches. We also prove that the Or algorithm enforces generalised arc consistency (GAC) when all its child constraints have a GAC propagator, and no variables are shared between children. By extending the Or propagator, we present a propagator for AtLeastK, which expresses that at least k of its child constraints are satisfied in any solution.Some logical expressions (e.g. exclusive-or) cannot be compactly expressed using And, Or and AtLeastK. Therefore we investigate reification of constraints. We present a fast generic algorithm for reification using satisfying sets and movable triggers.     

An Environment for Designing/Executing Constraint Solver Collaborations

Abstract

Constraint programming is a paradigm based on the notion of constraints and mechanisms for their resolution. Thus, the key point of this class of languages is not only to offer a wide class of constraints for declarativity reasons, but also to treat them efficiently. For this purpose, the need for collaboration i.e., combination and cooperation of solvers is widely recognized. This new concept enables to solve problems that cannot be tackled or efficiently solved with a single solver. Furthermore, the demand for integrating symbolic mathematical tools into automated deduction system has significantly increased.In order to meet these motivations we propose BALI, an environment for designing/executing solver collaborations. BALI is a heterogeneous distributed collaborative problem solving system. It consists of a solver collaboration language and a host language. By providing several construction primitives (as concurrency, parallelism and sequentiality) and several combinators for their composition (as iterator or guarded control), the solver collaboration language enables to build complex solvers from elementary heterogeneous ones. The solvers are encapsulated in order to federate their different knowledge representations. We thus obtain agents that communicate and collaborate with each other. The host language, which is a constraint programming language, furnishes several strategies for manipulating constraints and executing solver collaborations i.e., agent collaborations.     

An enhanced bitstring encoding for exact maximum clique search in sparse graphs

This paper describes BBMCW, a new efficient exact maximum clique algorithm tailored for large sparse graphs which can be bit-encoded directly into memory without a heavy performance penalty. These graphs occur in real-life problems when some form of locality may be exploited to reduce their scale. One such example is correspondence graphs derived from data association problems. The new algorithm is based on the bit-parallel kernel used by the BBMC family of published exact algorithms. BBMCW employs a new bitstring encoding that we denote ‘watched’, because it is reminiscent of the ‘watched literal’ technique used in satisfiability and other constraint problems. The new encoding reduces the number of spurious operations computed by the BBMC bit-parallel kernel in large sparse graphs. Moreover, BBMCW also improves on bound computation proposed in the literature for bit-parallel solvers. Experimental results show that the new algorithm performs better than prior algorithms over data sets of both real and synthetic sparse graphs. In the real data sets, the improvement in performance averages more than two orders of magnitude with respect to the state-of-the-art exact solver IncMaxCLQ.     

On the implication problem for cardinality constraints and functional dependencies

In database design, integrity constraints are used to express database semantics. They specify the way by that the elements of a database are associated to each other. The implication problem asks whether a given set of constraints entails further constraints. In this paper, we study the finite implication problem for cardinality constraints. Our main result is a complete characterization of closed sets of cardinality constraints. Similar results are obtained for constraint sets containing cardinality constraints, but also key and functional dependencies. Moreover, we construct Armstrong databases for these constraint sets, which are of special interest for example-based deduction in database design.     

Contractor programming

This paper describes a solver programming method, called contractor programming, that copes with two issues related to constraint processing over the reals. First, continuous constraints involve an inevitable step of solver design. Existing softwares provide an insufficient answer by restricting users to choose among a list of fixed strategies. Our first contribution is to give more freedom in solver design by introducing programming concepts where only configuration parameters were previously available. Programming consists in applying operators (intersection, composition, etc.) on algorithms called contractors that are somehow similar to propagators.Second, many problems with real variables cannot be cast as the search for vectors simultaneously satisfying the set of constraints, but a large variety of different outputs may be demanded from a set of constraints (e.g., a paving with boxes inside and outside of the solution set). These outputs can actually be viewed as the result of different contractors working concurrently on the same search space, with a bisection procedure intervening in case of deadlock. Such algorithms (which are not strictly speaking solvers) will be made easy to build thanks to a new branch & prune system, called paver.Thus, this paper gives a way to deal harmoniously with a larger set of problems while giving a fine control on the solving mechanisms. The contractor formalism and the paver system are the two contributions. The approach is motivated and justified through different cases of study. An implementation of this framework named Quimper is also presented.     

Deductive Generation of Constraint Propagation Rules

Constraint propagation can often be conveniently expressed by rules. In recent years, a number of techniques for automatic generation of rule-based constraint solvers have been developed, most of them using a generate-and-test approach. We examine a generation method that is based on deduction. A solver (i.e. a set of rules) for a complex constraint is obtained from one or several weaker solvers for simple constraints. We describe incremental solver constructions for several types of constraint modifications, including conjunction, existential and universal quantification.     

Logic-based solution methods for optimal control of hybrid systems

Combinatorial optimization over continuous and integer variables is a useful tool for solving complex optimal control problems of hybrid dynamical systems formulated in discrete-time. Current approaches are based on mixed-integer linear (or quadratic) programming (MIP), which provides the solution after solving a sequence of relaxed linear (or quadratic) programs. MIP formulations require the translation of the discrete/logic part of the hybrid problem into mixed-integer inequalities. Although this operation can be done automatically, most of the original symbolic structure of the problem (e.g., transition functions of finite state machines, logic constraints, symbolic variables, etc.) is lost during the conversion, with a consequent loss of computational performance. In this paper, we attempt to overcome such a difficulty by combining numerical techniques for solving convex programming problems with symbolic techniques for solving constraint satisfaction problems (CSP). The resulting "hybrid" solver proposed here takes advantage of CSP solvers for dealing with satisfiability of logic constraints very efficiently. We propose a suitable model of the hybrid dynamics and a class of optimal control problems that embrace both symbolic and continuous variables/functions, and that are tailored to the use of the new hybrid solver. The superiority in terms of computational performance with respect to commercial MIP solvers is shown on a centralized supply chain management problem with uncertain forecast demand.     

Improving Linear Constraint Propagation by Changing Constraint Representation

Propagation based finite domain solvers provide a general mechanism for solving combinatorial problems. Different propagation methods can be used in conjunction by communicating through the domains of shared variables. The flexibility that this entails has been an important factor in the success of propagation based solving for solving hard combinatorial problems. In this paper we investigate how linear integer constraints should be represented in order that propagation can determine strong domain information. We identify two kinds of substitution which can improve propagation solvers, and can never weaken the domain information. This leads us to an alternate approach to propagation based solving where the form of constraints is modified by substitution as computation progresses. We compare and contrast a solver using substitution against an indexical based solver, the current method of choice for implementing propagation based constraint solvers, identifying the relative advantages and disadvantages of the two approaches. In doing so, we investigate a number of choices in propagation solvers and their effects on a suite of benchmarks.     

Efficient Interval Linear Equality Solving in Constraint Logic Programming

Existing interval constraint logic programming languages, such as BNR Prolog, work under the framework of interval narrowing and are deficient in solving systems of linear constraints over real numbers, which constitute an important class of problems in engineering and other applications. In this paper, we suggest to separate linear equality constraint solving from inequality and non-linear constraint solving. The implementation of an efficient interval linear constraint solver, which is based on the preconditioned interval Gauss-Seidel method, is proposed. We show how the solver can be adapted to incremental execution and incorporated into a constraint logic programming language already equipped with a non-linear solver based on interval narrowing. The two solvers share common interval variables, interact and cooperate in a round-robin fashion during computation, resulting in an efficient interval constraint arithmetic language CIAL. The CIAL prototypes, based on CLP(R), are constructed and compared favorably against several major interval constraint logic programming languages.     

A full first-order constraint solver for decomposable theories

Over the last decade, first-order constraints have been efficiently used in the artificial intelligence world to model many kinds of complex problems such as: scheduling, resource allocation, computer graphics and bio-informatics. Recently, a new property called decomposability has been introduced and many first-order theories have been proved to be decomposable: finite or infinite trees, rational and real numbers, linear dense order,...etc. A decision procedure in the form of five rewriting rules has also been developed. This latter can decide if a first-order formula without free variables is true or not in any decomposable theory. Unfortunately, this decision procedure is not enough when we want to express the solutions of a first-order constraint having free variables. These kind of problems are generally known as first-order constraint satisfaction problems. We present in this paper, not only a decision procedure but a full first-order constraint solver for decomposable theories. Our solver is given in the form of nine rewriting rules which transform any first-order constraint ϕ (which can possibly contain free variables) into an equivalent formula φ which is either the formula true, or the formula false or a simple solved formula having at least one free variable and being equivalent neither to true nor to false. We show the efficiency of our solver by solving complex first-order constraints over finite or infinite trees containing a huge number of imbricated quantifiers and negations and compare the performances with those obtained using the most recent and efficient dedicated solver for finite or infinite trees. This is the first full first-order constraint solver for any decomposable theory.