For graphs $G$ and $H$, a mapping $f: V(G)\dom V(H)$ is a homomorphism of $G$ to $H$ if $uv\in E(G)$ implies $f(u)f(v)\in E(H).$ If, moreover, each vertex $u \in V(G)$ is associated with costs $c_i(u), i \in V(H)$, then the cost of the homomorphism $f$ is $\sum_{u\in V(G)}c_{f(u)}(u)$. For each fixed graph $H$, we have the {\em minimum cost homomorphism problem}, written as MinHOM($H)$. The problem is to decide, for an input graph $G$ with costs $c_i(u),$ $u \in V(G), i\in V(H)$, whether there exists a homomorphism of $G$ to $H$ and, if one exists, to find one of minimum cost. Minimum cost homomorphism problems encompass (or are related to) many well studied optimization problems. We describe a dichotomy of the minimum cost homomorphism problems for graphs $H$, with loops allowed. When each connected component of $H$ is either a reflexive proper interval graph or an irreflexive proper interval bigraph, the problem MinHOM($H)$ is polynomial time solvable. In all other cases the problem MinHOM($H)$ is NP-hard. This solves an open problem from an earlier paper. Along the way, we prove a new characterization of the class of proper interval bigraphs.

A product configurator which is complete, backtrack free and able to compute the valid domains at any state of the configuration can be constructed by building a Binary Decision Diagram (BDD). Despite the fact that the size of the BDD is exponential in the number of variables in the worst case, BDDs have proved to work very well in practice. Current BDD-based techniques can only handle interactive configuration with small finite domains. In this paper we extend the approach to handle string variables constrained by regular expressions. The user is allowed to change the strings by adding letters at the end of the string. We show how to make a data structure that can perform fast valid domain computations given some assignment on the set of string variables. We first show how to do this by using one large DFA. Since this approach is too space consuming to be of practical use, we construct a data structure that simulates the large DFA and in most practical cases are much more space efficient. As an example a configuration problem on $n$ string variables with only one solution in which each string variable is assigned to a value of length of $k$ the former structure will use $Ω(k^n)$ space whereas the latter only need $O(kn)$. We also show how this framework easily can be combined with the recent BDD techniques to allow both boolean, integer and string variables in the configuration problem.

The scores can be used in themselv es or serve as the basis for ranking or choice. For the present, only a few scoring pro cedures are endowed with their axiomatic characterizations. At the same time, a large num ber of ingenious procedures are advocated and used in such disciplines as manageme nt science, operations research, psychometrics, applied statistics, processing of spor t tournaments, graph theory, etc. Very few social choice papers deal with them. The aim of this pa per is to take one circumspect step toward an axiomatic framework for comparin g the merits of these elaborate procedures. As a result, we would like to isolate a family of s coring procedures that comprises a majority of'reasonable' procedures (so that th e further axioms could be imposed on this family). Two main approaches are applicable. The first one is to express the desired properties axiomatically, the second is to gather the ex isting procedures and specify their common algebraic form.

Constraint Programming (CP)[21] is a powerful technique for spec ifying Constraint Satisfaction Problems (CSPs) based on allowing a constraintprogrammer to model problems in terms of high-level constraints. Using such global constraints allows easier specification of problems but also allows for faster solve rs that take advantage of the structure in the problem. The classica l approach to CSP solving is to explore the search tree of all possible assignment s to the variables in a depth-first search backtracking manner, guided by v arious heuristics, until a solution is found or proven not to exist. One of the most basic techniques for reducing the number of search tree nodes explore d is to perform domain propagation at each node. In order to get as much domain propagation as possible we wish for each constraint to remove from the variable d omains all values that cannot participate in a solution to that constraint.

INRA Toulouse, France Abstract Weighted Max-SA T is the optimization version of SA T and many important problems can be naturally encoded as such. Solving weighted Max-SA T is an important problem from both a theoretical and a practical point of view. In recent ye ars, there has been considerable interest in finding efficient solving techniques. Most of thi s work focus on the computation of good quality lower bounds to be used within a branch and bou nd DPLL-like algorithm. Most often, these lower bounds are described in a procedural way. Because of that, it is difficult to realize the logic that is behind. In this paper we introduce an original framework for Max-SA T that stresses the parallelism with classical SA T. Then, we extend the two basic SA T s olving techniques: search and inference. We show that many algorithmic tricks used in state-of-the-art Max-SA T solvers are easily expressable in logic terms with our framework in a unified manner. Besides, we introduce an original search algorithm that per forms a restricted amount of weighted resolution at each visited node. We empirically compare our algorithm w ith a variety of solving alternatives on several benchmarks. Our experiments, which constitute to the best of our knowledge the most comprehensive Max-sat eva luation ever reported, show that our algorithm is generally orders of magnitude faster t han any competitor. Preprint submitted to Elsevier Science 11 September 2018 1 Introduction Weighted Max-SA T is the optimization version of the SA T prob lem and many important problems can be naturally expressed as such. In recent years, there has been a considerable effort in finding efficient exact algorithms. A common drawback of all these alg orithms is that albeit the close relationship between SA T and Max-SA T, they cannot be easily described with logic terminology. For instance, the contributions of [11,12,13,14] are good quality lower bounds to be incorporated into a depth-first branch and bound procedure. These lower bounds are mostly defined in a procedural way and it is very difficult to see the logic that is behind the execution of the procedure. This is in contrast with SA T algorithms where the solving process can b e easily decomposed into atomic logical steps. In this paper we introduce an original framework for (weight ed) Max-SA T in which the notions of upper and lower bound are incorporated into the problem definition. Under this framework classical SA T is just a particular case of Max-SA T, and the main SA T solving techniques can be naturally extended. In pa rticular, we extend the basic simplification rules (for example, idempotency, absorption, unit clause reduction, etc) and introduce a new one, hardening, that does not make sense in the SA T context.

We study an alternative to the prevailing approach to modelling qualitative spatial reasoning (QSR) problems as constraint satisfaction problems. In the standard approach, a relation between objects is a constraint whereas in the alternative approach it is a variable. The relation-variable approach greatly simplifies integration and implementation of QSR. To substantiate this point, we discuss several QSR algorithms from the literature which in the relation-variable approach reduce to the customary constraint propagation algorithm enforcing generalised arc-consistency.

We introduce a constraint-based framework for studying infinite qualitative simulations concerned with contingencies such as time, space, shape, size, abstracted into a finite set of qualitative relations. To define the simulations, we combine constraints that formalize the background knowledge concerned with qualitative reasoning with appropriate inter-state constraints that are formulated using linear temporal logic. We implemented this approach in a constraint programming system by drawing on ideas from bounded model checking. The resulting system allows us to test and modify the problem specifications in a straightforward way and to combine various knowledge aspects.

Constraint propagation algorithms implement logical infe r-ence. For efficiency, it is essential to control whether and in what order basic inference steps are taken. We provide a high-level fra mework that clearly differentiates between information needed for cont rolling propagation versus that needed for the logical semantics of complex constraints composed from primitive ones. We argue for the appropriaten ess of our controlled propagation framework by showing that it captures the underlying principles of manually designed propagation algo rithms, such as literal watching for unit clause propagation and the lexi cographic ordering constraint. We provide an implementation and benchm ark results that demonstrate the practicality and efficiency of our frame work.

In this short paper we present a linear constraint solver for the UniCalc system, an environment for reliable solution of mathematical modeling problems.

We discuss here constraint programming (CP) by using a proof-theoretic perspective. To this end we identify three levels of abstraction. Each level sheds light on the essence of CP. In particular, the highest level allows us to bring CP closer to the computation as deduction paradigm. At the middle level we can explain various constraint propagation algorithms. Finally, at the lowest level we can address the issue of automatic generation and optimization of the constraint propagation algorithms.