Constraint programming (CP) modeling languages, like MiniZinc, Essence and CPMpy, play a crucial role in making CP technology accessible to non-experts. Both solver-independent modeling frameworks and solvers themselves are complex pieces of software that can contain bugs, which undermines their usefulness. Mutational fuzz testing is a way to test complex systems by stochastically mutating input and verifying preserved properties of the mutated output. We investigate different mutations and verification methods that can be used on the constraint specifications directly. This includes methods proposed in the context of SMT problem specifications, as well as new methods related to global constraints, optimization, and solution counting/preservation. Our results show that such a fuzz testing approach improves the overall code coverage of a modeling system compared to only unit testing, and is able to find bugs in the whole toolchain, from the modeling language transformations themselves to the underlying solvers.

Core-guided techniques have revolutionized Boolean satisfiability approaches to optimization problems (MaxSAT), but the process at the heart of these methods, strengthening bounds on solutions by repeatedly adding cardinality constraints, remains a bottleneck. Cardinality constraints require significant work to be re-encoded to SAT, and SAT solvers are notoriously weak at cardinality reasoning. In this work, we lift core-guided search to pseudo-Boolean (PB) solvers, which deal with more general PB optimization problems and operate natively with cardinality constraints. The cutting planes method used in such solvers allows us to derive stronger cardinality constraints, which yield better updates to solution bounds, and the increased efficiency of objective function reformulation also makes it feasible to switch repeatedly between lower-bounding and upper- bounding search. A thorough evaluation on applied and crafted benchmarks shows that our core-guided PB solver significantly improves on the state of the art in pseudo-Boolean optimization.

Abstract Technological progress in Answer Set Programming (ASP) has been stimulated by the use of common standards, such as the ASP-Core-2 language. While ASP has its roots in nonmonotonic reasoning, efforts have also been made to reconcile ASP with classical first-order (FO) logic. This has resulted in the development of FO(·), an expressive extension of FO, which allows ASP-like problem solving in a purely classical setting. This language may be more accessible to domain experts already familiar with FO and may be easier to combine with other formalisms that are based on classical logic. It is supported by the IDP inference system, which has successfully competed in a number of ASP competitions. Here, however, technological progress has been hampered by the limited number of systems that are available for FO(·). In this paper, we aim to address this gap by means of a translation tool that transforms an FO(·) specification into ASP-Core-2, thereby allowing ASP-Core-2 solvers to be used as solvers for FO(·) as well. We present experimental results to show that the resulting combination of our translation with an off-the-shelf ASP solver is competitive with the IDP system as a way of solving problems formulated in FO(·).

Systems mixing Boolean logic and arithmetic have been a long-standing challenge for verification tools such as SATbased bit-vector solvers.Though SAT solvers can be highly efficient for Boolean reasoning, they scale poorly once multiplication is involved.Algebraic methods using Gröbner basis reduction have recently been used to efficiently verify multiplier circuits in isolation, but generally do not perform well on problems involving bit-level reasoning.We propose that pseudo-Boolean solvers equipped with cutting planes reasoning have the potential to combine the complementary strengths of the existing SAT and algebraic approaches while avoiding their weaknesses.Theoretically, we show that there are optimal-length cutting planes proofs for a large class of bit-level properties of some well known multiplier circuits.This scaling is significantly better than the smallest proofs known for SAT and, in some instances, for algebraic methods.We also show that cutting planes reasoning can extract bit-level consequences of word-level equations in exponentially fewer steps than methods based on Gröbner bases.Experimentally, we demonstrate that pseudo-Boolean solvers can verify the word-level equivalence of adder-based multiplier architectures, as well as commutativity of bit-vector multiplication, in times comparable to the best algebraic methods.We then go further than previous approaches and also verify these properties at the bit-level.Finally, we find examples of simple nonlinear bit-vector inequalities that are intractable for current bit-vector and SAT solvers but easy for pseudo-Boolean solvers.

Abstract Symmetry in combinatorial problems is an extensively studied topic. We continue this research in the context of model expansion problems, with the aim of automating the workflow of detecting and breaking symmetry. We focus onlocal domain symmetry, which is induced by permutations of domain elements, and which can be detected on a first-order level. As such, our work is a continuation of the symmetry exploitation techniques of model generation systems, while it differs from more recent symmetry breaking techniques in answer set programming which detect symmetry on ground programs. Our main contributions are sufficient conditions for symmetry of model expansion problems, the identification oflocal domain interchangeability, which can often be broken completely, and efficient symmetry detection algorithms for both local domain interchangeability as well as local domain symmetry in general. Our approach is implemented in the model expansion system IDP, and we present experimental results showcasing the strong and weak points of our approach compared tosbass, a symmetry breaking technique for answer set programming.

Many state-of-the-art declarative systems use a ground-and-solve approach, where the problem statement, expressed in a high-level language, is first grounded into a low-level representation. Next, a solver is used to search a solution for the low-level representation. In order to prevent a combinatorial blowup of the grounding, many intelligent techniques have been developed. In this paper we study in detail three such techniques (Lifted Unit Propagation, Grounding With Bounds, and Reduced Grounding) to get a better insight in their individual merits and their interactions. Our experiments take as benchmarks all the NP problems of the previous Answer Set Programming (ASP) competitions. The experiments are performed with IDP3 and all tools needed to run them are made publicly available. The first experiment discusses the impact of the three techniques on the "efficiency" of the grounding step, and on each other. In a second set of experiments we show that a reduction in the grounding size as a result of the application of these grounding techniques does not reduce the search space. We give an in-depth analysis of our results and discuss what this means for the development of grounding techniques for declarative systems.

The traditional approach to Model Expansion (MX) is to reduce the theory to a propositional language and apply a search algorithm to the resulting theory. Function symbols are typically replaced by predicate symbols representing the graph of the function, an operation that blows up the reduced theory. In this paper, we present an improved approach to handle function symbols in a ground-and-solve methodology, building on ideas from Constraint Programming. We do so in the context of FO(.)IDP, the knowledge representation language that extends First-Order Logic (FO) with, among others, inductive definitions, arithmetic and aggregates. An MX algorithm is developed, consisting of (i) a grounding algorithm for FO(.)^IDP, parametrised by the function symbols allowed to occur in the reduced theory, and (ii) a search algorithm for unrestricted, ground FO(.)^IDP. The ideas are implemented in the IDP knowledge-base system and experimental evaluation shows that both more compact groundings and improved search performance are obtained.

For constraint programming, many well performing dynamic symmetry breaking techniques have been devised. For propositional satisfiability solving, dynamic symmetry breaking is still either slower or less general than static symmetry breaking. This paper presents Symmetry Propagation, which is an improvement to Lightweight Dynamic Symmetry Breaking, a dynamic symmetry breaking approach from CP. Symmetry Propagation uses any given symmetry as a propagator, and as a result is a general symmetry breaking technique. Experiments with an implementation in the SAT solver Minisat show that on many benchmarks, Symmetry Propagation outperforms the state-of-the-art static symmetry breaking method Shatter.