ABSTRACT. Due to the availability of powerful SAT solvers, propositional encoding is a successful technique of solving constraint systems over finite domains. As these domains are often flat and non-structured, we aim to extend this concept by enriching the underlying domain with user-defined product types and sum types. The co4 language is a syntactically subset of Haskell and allows to specify constraint systems over such enriched domains using algebraic data types, pattern-matching, higher-order functions and polymorphism. This paper gives an overview over the transformation into propositional logic and illustrates examples and use-cases for co4.

ABSTRACT. The formalisms for MaxSat and SoftCSPs are strongly related much like SAT and CP. Both address the problem of constrained optimization. The formalism that is the 800-kg gorilla of this area is Mixed Integer Programming (MIPS). Of these three formalisms the technology for solving MIPs is the most developed, although MaxSat and SoftCSP solvers have also made significant progress. All three formalisms have focused on exploiting quite distinct algorithmic methods, and empirical evidence indicates that each of these formalisms can dominate the others on particular problems. A promising research direction is to explore the hybridization of these formalisms, and in this talk I will discuss some of the work that has been done and that is yet to be done in exploiting the disparate strengths of these formalisms.

ABSTRACT. In this paper, we investigate the complexity of algorithms for solving CSPs which are classically implemented in real practical solvers, such as Forward Checking or Bactracking with Arc Consistency (RFL or MAC).. We introduce a new parameter for measuring their complexity and then we derive new complexity bounds. By relating the complexity of CSP algorithms to graph-theoretical parameters, our analysis allows us to define new tractable classes, which can be solved directly by the usual CSP algorithms in polynomial time, and without the need to recognize the classes in advance. So, our approach allows us to propose new tractable classes of CSPs that are naturally exploited by solvers, which indicates new ways to explain in some cases the practical efficiency of classical search algorithms.

ABSTRACT. Symmetry is a topic studied by both the Satisfiability (SAT) and Constraint Programming (CP) community. However, few attempts at transferring results between both communities have been made. This paper makes the link by explaining how symmetries from Constraint Satisfiaction Problems (CSP's) transfer to their direct SAT-encoding. We point out that many interesting symmetry groups of CP all map to piecewise row symmetries of their CSP's SAT-encoding, which -using a CP result- can be broken completely. We then show that the standard SAT symmetry approaches do not break these symmetries completely, so we address this issue by designing a new symmetry breaking preprocessor, implemented as the BreakIDGlucose SAT-solver. BreakIDGlucose's first place in the hard combinatorial track of 2013's SAT-competition proves the relevance of this approach.