Core-guided approaches to solving MAXSAT have proved to be effective on industrial problems. These approaches solve a MAXSAT formula by building a sequence of SAT formulas, where in each formula a greater weight of soft clauses can be relaxed. The soft clauses are relaxed via the addition of blocking variables, and the total weight of soft clauses that can be relaxed is limited by placing constraints on the blocking variables. In this work we propose an alternative approach. Our approach also builds a sequence of new SAT formulas. However, these formulas are constructed using MAXSAT resolution, a sound rule of inference for MAXSAT. MAXSAT resolution can in the worst case cause a quadratic blowup in the formula, so we propose a new compressed version of MAXSAT resolution. Using compressed MAXSAT resolution our new core-guided solver improves the state-of-theart, solving significantly more problems than other state-ofthe-art solvers on the industrial benchmarks used in the 2013 MAXSAT Solver Evaluation.

Constraints over finite sequences of variables are ubiquitous in sequencing and timetabling. This led to general modelling techniques and generic propagators, often based on deterministic finite automata (DFA) and their extensions. We consider counter-DFAs (cDFA), which provide concise models for regular counting constraints, that is constraints over the number of times a regular-language pattern occurs in a sequence. We show how to enforce domain consistency in polynomial time for at-most and at-least regular counting constraints based on the frequent case of a cDFA with only accepting states and a single counter that can be increased by transitions. We also show that the satisfaction of exact regular counting constraints is NP-hard and that an incomplete propagator for exact regular counting constraints is faster and provides more pruning than the existing propagator from (Beldiceanu, Carlsson, and Petit 2004). Finally, by avoiding the unrolling of the cDFA used by COSTREGULAR, the space complexity reduces from O(n · |Σ| · |Q|) to O(n · (|Σ| + |Q|)), where Σ is the alphabet and Q the state set of the cDFA.

This paper resolves previous problems in the Multi-Strategy architecture for online learning of robotic behaviours. The hybrid method includes a symbolic qualitative planner that constructs an approximate solution to a control problem. The approximate solution provides constraints for a numerical optimisation algorithm, which is used to refine the qualitative plan into an operational policy. Introducing quantitative constraints into the planner gives previously unachievable domain independent reasoning. The method is demonstrated on a multi-tracked robot intended for urban search and rescue.

Consider a family whose home is equipped with several service robots. The actions planned for the robots must adhere to Interaction Constraints (ICs) relating them to human activities and preferences. These constraints must be sufficiently expressive to model both temporal and logical dependencies among robot actions and human behavior, and must accommodate incomplete information regarding human activities. In this paper we introduce an approach for automatically generating plans that are conformant wrt. given ICs and partially specified human activities. The approach allows to separate causal reasoning about actions from reasoning about ICs, and we illustrate the computational advantage this brings with experiments on a large-scale (semi-)realistic household domain with hundreds of human activities and several robots.

There has been a great deal of interest about negotiations having interdependent issues and nonlinear utility spaces as they arise in many realistic situations. In this case, reaching a consensus among agents becomes more difficult as the search space and the complexity of the problem grow. Nevertheless, none of the proposed approaches tries to quantitatively assess the complexity of the scenarios in hand, or to exploit the topology of the utility space necessary to concretely tackle the complexity and the scaling issues. We address these points by adopting a representation that allows a modular decomposition of the issues and constraints by mapping the utility space into an issue-constraint hypergraph. Exploring the utility space reduces then to a message passing mechanism along the hyperedges by means of utility propagation. Adopting such representation paradigm will allow us to rigorously show how complexity arises in nonlinear scenarios. To this end, we use the concept of information entropy in order to measure the complexity of the hypergraph. Being able to assess complexity allows us to improve the message passing algorithm by adopting a low-complexity propagation scheme. We evaluated our model using parametrized random hyper- graphs, showing that it can optimally handle complex utility spaces while outperforming previous sampling approaches.

The fundamental reasoning problem in RCC-8 is deciding In contrast to the synthetic RCC-8 networks that have the consistency of a set of constraints Θ, i.e., whether there been used in the literature for evaluating the aforementioned is a spatial configuration where the relations between the reasoners, the real-world networks of Table 1 are very sparse regions can be described by Θ. Traditionally in qualitative and one to two orders of magnitude larger. The labels on spatial reasoning (QSR) consistency of such sets is decided their edges contain 1 or 2 base RCC-8 relations forming a by a backtracking algorithm which optionally uses a pathconsistency disjunction. This kind of networks have not been employed algorithm as a preprocessing step for forward in any experimental evaluation of RCC-8 reasoners with the checking. In general, this problem is NPcomplete (Renz exception of (Sioutis and Koubarakis 2012) in which the network and Nebel 1999). However it has been shown in (Renz 1999) adm1 has been used. Typically, the literature focuses that there are tractable subsets of RCC-8 for which the consistency on quite smaller networks (20 to 1000 nodes) with an average problem can be decided by path-consistency. of 4 base RCC-8 relations per edge, and an average Table 1 depicts the characteristics of some real-world node degree ranging from 4 to 20. Deciding the consistency RCC-8 networks recording the topological relations between of real-world networks is a very important task. Inconsistencies administrative regions in Europe (networks nuts, might arise because their RCC-8 relations are computed adm1, and adm2) and the world (networks gadm1 and based on the geometries of geographical objects which gadm2), and the performance of the following reasoners often have not been captured correctly (e.g., overlapping geometries regarding consistency checking: Renz-Nebel01 (Renz and between two regions that in principle are externally Nebel 2001), GQR-1500 (Gantner, Westphal, and Woelfl connected). This is the case for the networks gadm1 and 2008; Westphal and Hué 2012), PPyRCC8 (Sioutis and gadm2.

Constraints over variable sequences are ubiquitous and many of their propagators have been inspired by dynamic programming (DP). We propose a conceptual framework for designing such propagators: pruning rules, in a functional notation, are refined upon the application of transformation operators to a DP-style formulation of a constraint; a representation of the (tuple) variable domains is picked; and a control of the pruning rules is picked.

The paper proposes a dynamic method, Recursive SBDS(ReSBDS), for efficient partial symmetry breaking. Wefirst demonstrate how (partial) Symmetry BreakingDuring Search (SBDS) misses important pruning opportunitieswhen given only a subset of symmetries tobreak. The investigation pinpoints the culprit and in turnsuggests rectification. The main idea is to add extra conditionalconstraints during search recursively to prunealso symmetric nodes of some pruned subtrees. Thus,ReSBDS can break extra symmetry compositions, butis carefully designed to break only the ones that areeasy to identify and inexpensive to break. We presenttheorems to guarantee the soundness and terminationof our approach, and compare our method with popularstatic and dynamic methods. When the variable (value)heuristic is static, ReSBDS is also complete in eliminatingall interchangeable variables (values) given only thegenerator symmetries. Extensive experimentations confirmthe efficiency of ReSBDS, when compared againststate of the art methods.

Bi-Objective Combinatorial Optimization problems are ubiquitous in real-world applications and designing approaches to solve them efficiently is an important research area of Artificial Intelligence. In Constraint Programming, the recently introduced bi-objective Pareto constraint allows one to solve bi-objective combinatorial optimization problems exactly. Using this constraint, every non-dominated solution is collected in a single tree-search while pruning sub-trees that cannot lead to a non-dominated solution. This paper introduces a simpler and more efficient filtering algorithm for the bi-objective Pareto constraint. The efficiency of this algorithm is experimentally confirmed on classical bi-objective benchmarks.

The concepts of MSS (Maximal Satisfiable Subset) andCoMSS (also called Minimal Correction Subset) playa key role in many A.I. approaches and techniques. Inthis paper, a novel algorithm for partitioning a BooleanCNF formula into one MSS and the correspondingCoMSS is introduced. Extensive empirical evaluationshows that it is more robust and more efficient on mostinstances than currently available techniques.