Presolving is a preprocessing step performed by optimisation solvers to improve performance. However, these solvers cannot easily exploit high-level model structure as available in modelling languages such as MiniZinc or Essence. We present an integrated approach that performs presolving as a separate pass during the compilation from high-level optimisation models to solver-level programs. The compiler produces a representation of the model that is suitable for presolving by retaining some of the high-level structure. It then uses information learned during presolving to generate the final solver-level representation. Our approach introduces the novel concept of variable paths that identify variables which are common across multiple compilation passes, increasing the amount of shared information. We show that this approach can lead to both faster compilation and more efficient solver-level programs.

The generation and GAC enforcement of a large number of weak nogoods in Symmetry Breaking During Search (SBDS) is costly and often not worthwhile in terms of prunings. In this paper, we propose weak-nogood consistency (WNC) for nogoods and a lazy propagator for SBDS (and its variants) using watched literal technology. We give formal results on the strength and relatively low space and time complexities of the lazy propagator. Nogoods collected for each symmetry are increasing. We further define generalized weak-incNGs consistency (GWIC) for a conjunction of increasing nogoods, and give a lazy propagator for the incNGs global constraint. We prove GWIC on a conjunction is equivalent to WNC on individual nogoods, and give the space and time complexities. Various lazy versions of SBDS and its variants are implemented. We give experimentation to demonstrate the efficiency of the lazy versions as compared to state of the art symmetry breaking methods.

Specifically, we present a top-down algorithm cn2mddg for compiling finite-domain CNs into multivalued decomposable We present and evaluate a top-down algorithm for decision graphs. The input of cn2mddg is a CN compiling finite-domain constraint networks (CNs) represented in the XCSP 2.1 format [Roussel and Lecoutre, into the language MDDG of multivalued decomposable 2009]. The output of our compilation algorithm is a representation decision graphs. Though it includes Decision-of the solutions of the CN in the language MDDG DNNF as a proper subset, MDDG offers the same key of multivalued decomposable decision graphs. MDDG is precisely tractable queries and transformations as Decision-the extension to non-Boolean domains of the language DNNF, which makes it useful for many applications. DDG [Fargier and Marquis, 2006] also known as Decision-Intensive experiments showed that our compiler DNNF [Oztok and Darwiche, 2014]: it is based on decomposable cn2mddg succeeds in compiling CNs which -nodes and (multivalued) decision nodes. Similarly are out of the reach of standard approaches based to Decision-DNNF, the MDDG language offers a number of on a translation of the input network to CNF, followed tractable queries, including (possibly weighted) solution finding by a compilation to Decision-DNNF. Furthermore, and counting, solution enumeration (solutions can be enumerated the sizes of the resulting compiled representations with polynomial delay), and optimization w.r.t. a linear turn out to be much smaller (sometimes by objective function. It also offers tractable transformations, several orders of magnitude).

The last decade has seen a growing interest in solver portfolios, automated solver configuration, and runtime prediction methods. At their core, these methods rely on a deterministic, consistent behaviour from the underlying algorithms and solvers. However, modern state-of-the-art solvers have elementsof stochasticity built in such as randomised variable and value selection, tie-breaking, and randomised restarting. Such features can elicit dramatic variations in the overall performance between repeated runs of the solver,often by several orders of magnitude. Despite the success of the aforementioned fields, such performance variations in the underlying solvers have largely been ignored. Supported by a large-scale empirical study employing many years of industrial SAT Competition instances including repeated runs, we present statistical and empirical evidence that such a performance variation phenomenon necessitates a change in the evaluation of portfolio, runtime prediction, and automated configuration methods. In addition, we demonstrate that this phenomenon can have a significant impact on empirical solver competitions. Specifically, we show that the top three solvers from the 2014 SAT Competition could have been ranked in any permutation. These findings demonstrate the need for more statistically well-founded regimes in empirical evaluations.

Adaptive constraint propagation has recently received a great attention. It allows a constraint solver to exploit various levels of propagation during search, and in many cases it shows better performance than static/predefined. The crucial point is to make adaptive constraint propagation automatic, so that no expert knowledge or parameter specification is required. In this work, we propose a simple learning technique, based on multi-armed bandits, that allows to automatically select among several levels of propagation during search. Our technique enables the combination of any number of levels of propagation whereas existing techniques are only defined for pairs. An experimental evaluation demonstrates that the proposed technique results in a more efficient and stable solver.

A number of effective techniques for constraint-based optimization can be used to generate either diverse or high-quality solutions independently, but no framework is devoted to accomplish both simultaneously. In this paper, we tackle this issue with a generic paradigm that can be implemented in most existing solvers. We show that our technique can be specialized to produce diverse solutions of high quality in the context of over-constrained problems. Furthermore, our paradigm allows us to consider diversity from a different point of view, based on generic concepts expressed by global constraints.

Core-guided MAXSAT algorithms dominate other methods in solving industrial MAXSAT problems. In this work, we propose a new efficient algorithm that is guided by correction sets and cores. At every iteration, the algorithm obtains a correction set or a core, which is then used to rewrite the formula using incremental and succinct transformations. We theoretically show that correction sets and cores have complementary strengths and empirically demonstrate that their combination leads to an efficient MAXSAT solver that outperforms state-of-the-art WPMS solvers on the 2014 Evaluation on industrial instances.

In Constraint Programming (CP), a portfolio solver uses a variety of different solvers for solving a given Constraint Satisfaction / Optimization Problem. In this paper we introduce sunny-cp2: the first parallel CP portfolio solver that enables a dynamic, cooperative, and simultaneous execution of its solvers in a multicore setting. It incorporates state-of-the-art solvers, providing also a usable and configurable framework. Empirical results are very promising. sunny-cp2 can even outperform the performance of the oracle solver which always selects the best solver of the portfolio for a given problem.

Constraint Programming A Constraint Satisfaction Problem (CSP) [6] consists of a set of decision variables, each with a finite domain of values, and a set of constraints specifying allowed combinations of values for some variables. A solution to a CSP is an assignment of variables to values in their respective domains such that all of the constraints are satisfied. Constraint solvers typically explore partial assignments enforcing a local consistency property. A constraint c is generalized arc consistent (GAC) if and only if when a variable is assigned any of the values in its domain, there exist compatible values in the domains of all the other variables of c. In order to enforce a local consistency property on a constraint c during search, we employ filtering algorithms that remove inconsistent values from the domains of the variables of c. These filtering algorithms are repeatedly called until no more values are pruned. This process is called constraint propagation.

In this paper, we provide a novel construction of the linear-sized spectral sparsifiers of Batson, Spielman and Srivastava [BSS14]. While previous constructions required $\Omega(n^4)$ running time [BSS14, Zou12], our sparsification routine can be implemented in almost-quadratic running time $O(n^{2+\varepsilon})$. The fundamental conceptual novelty of our work is the leveraging of a strong connection between sparsification and a regret minimization problem over density matrices. This connection was known to provide an interpretation of the randomized sparsifiers of Spielman and Srivastava [SS11] via the application of matrix multiplicative weight updates (MWU) [CHS11, Vis14]. In this paper, we explain how matrix MWU naturally arises as an instance of the Follow-the-Regularized-Leader framework and generalize this approach to yield a larger class of updates. This new class allows us to accelerate the construction of linear-sized spectral sparsifiers, and give novel insights on the motivation behind Batson, Spielman and Srivastava [BSS14].