Constraint-Based Reasoning
Automated Modelling and Solving in Constraint Programming
O' (University College Cork) | Sullivan, Barry
Constraint programming can be divided very crudely into modeling and solving. Modeling defines the problem, in terms of variables that can take on different values, subject to restrictions (constraints) on which combinations of variables are allowed. Solving finds values for all the variables that simultaneously satisfy all the constraints. However, the impact of constraint programming has been constrained by a lack of "user-friendliness''. Constraint programming has a major "declarative" aspect, in that a problem model can be handed off for solution to a variety of standard solving methods. These methods are embedded in algorithms, libraries, or specialized constraint programming languages. To fully exploit this declarative opportunity however, we must provide more assistance and automation in the modeling process, as well as in the design of application-specific problem solvers. Automated modelling and solving in constraint programming presents a major challenge for the artificial intelligence community. Artificial intelligence, and in particular machine learning, is a natural field in which to explore opportunities for moving more of the burden of constraint programming from the user to the machine. This paper presents technical challenges in the areas of constraint model acquisition, formulation and reformulation, synthesis of filtering algorithms for global constraints, and automated solving. We also present the metrics by which success and progress can be measured.
Computing Cost-Optimal Definitely Discriminating Tests
Schumann, Anika (Cork Constraint Computation Centre) | Huang, Jinbo (NICTA and Australian National University) | Sachenbacher, Martin (Technische Universitรคt Mรผnchen)
The goal of testing is to discriminate between multiple hypotheses about a system - for example, different fault diagnoses - by applying input patterns and verifying or falsifying the hypotheses from the observed outputs. Definitely discriminating tests (DDTs) are those input patterns that are guaranteed to discriminate between different hypotheses of non-deterministic systems. Finding DDTs is important in practice, but can be very expensive. Even more challenging is the problem of finding a DDT that minimizes the cost of the testing process, i.e., an input pattern that can be most cheaply enforced and that is a DDT. This paper addresses both problems. We show how we can transform a given problem into a Boolean structure in decomposable negation normal form (DNNF), and extract from it a Boolean formula whose models correspond to DDTs. This allows us to harness recent advances in both knowledge compilation and satisfiability for efficient and scalable DDT computation in practice. Furthermore, we show how we can generate a DNNF structure compactly encoding all DDTs of the problem and use it to obtain a cost-optimal DDT in time linear in the size of the structure. Experimental results from a real-world application show that our method can compute DDTs in less than 1 second for instances that were previously intractable, and cost-optimal DDTs in less than 20 seconds where previous approaches could not even compute an arbitrary DDT.
Security Games with Arbitrary Schedules: A Branch and Price Approach
Jain, Manish (University of Southern California) | Kardes, Erim (University of Southern California) | Kiekintveld, Christopher (University of Southern California) | Ordonez, Fernando (University of Southern California) | Tambe, Milind (University of Southern California)
Security games, and important class of Stackelberg games, are used in deployed decision-support tools in use by LAX police and the Federal Air Marshals Service. The algorithms used to solve these games find optimal randomized schedules to allocate security resources for infrastructure protection. Unfortunately, the state of the art algorithms either fail to scale or to provide a correct solution for large problems with arbitrary scheduling constraints. We introduce ASPEN, a branch-and-price approach that overcomes these limitations based on two key contributions: (i) A column-generation approach that exploits a novel network flow representation, avoiding a combinatorial explosion of schedule allocations; (ii) A branch-and-bound algorithm that generates bounds via a fast algorithm for solving security games with relaxed scheduling constraints. ASPEN is the first known method for efficiently solving massive security games with arbitrary schedules.
Dominance Testing via Model Checking
Santhanam, Ganesh Ram (Iowa State University) | Basu, Samik (Iowa State University) | Honavar, Vasant (Iowa State University)
Dominance testing, the problem of determining whether an outcome is preferred over another, is of fundamental importance in many applications. Hence, there is a need for algorithms and tools for dominance testing. CP-nets and TCP-nets are some of the widely studied languages for representing and reasoning with preferences. We reduce dominance testing in TCP-nets to reachability analysis in a graph of outcomes. We provide an encoding of TCP-nets in the form of a Kripke structure for CTL. We show how to compute dominance using NuSMV, a model checker for CTL. We present results of experiments that demonstrate the feasibility of our approach to dominance testing.
Propagating Conjunctions of AllDifferent Constraints
Bessiere, Christian (LIRMM, CNRS) | Katsirelos, George (CRIL-CNRS) | Narodytska, Nina (NICTA and UNSW) | Quimper, Claude-Guy (Universite Laval) | Walsh, Toby (NICTA and UNSW)
We study propagation algorithms for the conjunction of two AllDifferent constraints. Solutions of an AllDifferent constraint can be seen as perfect matchings on the variable/value bipartite graph. Therefore, we investigate the problem of finding simultaneous bipartite matchings. We present an extension of the famous Hall theorem which characterizes when simultaneous bipartite matchings exists. Unfortunately, finding such matchings is NP-hard in general. However, we prove a surprising result that finding a simultaneous matching on a convex bipartite graph takes just polynomial time. Based on this theoretical result, we provide the first polynomial time bound consistency algorithm for the conjunction of two AllDifferent constraints. We identify a pathological problem on which this propagator is exponentially faster compared to existing propagators. Our experiments show that this new propagator can offer significant benefits over existing methods.
Towards Interesting Patterns of Hard CSPs with Functional Constraints
Li, Chendong (University of Connecticut)
The hardness of finite domain Constraint Satisfaction Problems (CSPs) is an important research topic in Constraint Programming (CP) community. In this paper, we study the association rule mining techniques together with rule deduction and propose a cascaded approach to extract interesting patterns of hard CSPs with functional constraints. Specifically, we generate random CSPs, collect controlling parameters and hardness characteristics by solving all the CSP instances. Afterwards, we apply association rule mining with rule deduction on the collected data set and further extract interesting patterns of the hardness of the randomly generated CSPs. As far as we know, this problem is investigated with data mining techniques for the first time.
Exploiting Monotonicity in Interval Constraint Propagation
Araya, Ignacio (INRIA) | Trombettoni, Gilles (INRIA, University of Nice-Sophia) | Neveu, Bertrand (Imagine LIGM university Paris-Est)
We propose in this paper a new interval constraint propagation algorithm, called MOnotonic Hull Consistency (Mohc), that exploits monotonicity of functions. The propagation is standard, but the Mohc-Revise procedure, used to filter/contract the variable domains w.r.t. an individual constraint, uses monotonic versions of the classical HC4-Revise and BoxNarrow procedures. Mohc-Revise appears to be the first adaptive revise procedure ever proposed in (interval) constraint programming.ย Also, when a function is monotonic w.r.t. every variable, Mohc-Revise is proven to compute the optimal/sharpest box enclosing all the solutions of the corresponding constraint (hull consistency). Very promising experimental results suggest that Mohc has the potential to become an alternative to the state-of-the-art HC4 and Box algorithms.
In Defense of Large Qualitative Calculi
Li, Jason Jingshi (The Australian National University) | Renz, Jochen (The Australian National University)
The next challenge in qualitative spatial and temporal reasoning is to develop calculi that deal with different aspects of space and time. One approach to achieve this is to combine existing calculi that cover the different aspects. This, however, can lead to calculi that have a very large number of relations and it is a matter of ongoing discussions within the research community whether such large calculi are too large to be useful. In this paper we develop a procedure for reasoning about some of the largest known calculi, the Rectangle Algebra and the Block Algebra with about 10 661 ย relations. We demonstrate that reasoning over these calculi is possible and can be done efficiently in many cases. This is a clear indication that one of the main goals of the field can be achieved: highly expressive spatial and temporal representations that support efficient reasoning.
Simultaneous Elicitation of Preference Features and Utility
Boutilier, Craig (University of Toronto) | Regan, Kevin (University of Toronto) | Viappiani, Paolo (University of Toronto)
Most frameworks for utility elicitation assume a predefined set of features over which user preferences are expressed. We consider utility elicitation in the presence of subjective or user-defined features, whose definitions are not known in advance. We treat the problem of learning a user's feature definition as one of concept learning, but whose goal is to learn only enough about the concept definition to enable a good decision to be made. This is complicated by the fact that user utility is unknown. We describe computational procedures for identifying optimal alternatives w.r.t minimax regret in the presence of both utility and concept uncertainty; and develop several heuristic query strategies that focus simultaneously on reduction of relevant concept and utility uncertainty.
A Stronger Consistency for Soft Global Constraints in Weighted Constraint Satisfaction
Lee, Jimmy (The Chinese University of Hong Kong) | Leung, K. L. (The Chinese University of Hong Kong)
Weighted Constraint Satisfaction is made practical by powerful consistency techniques, such as AC*, FDAC* and EDAC*, which reduce search space effectively and efficiently during search, but they are designed for only binary and ternary constraints. To allow soft global constraints, usually of high arity, to enjoy the same benefits, Lee and Leung give polynomial time algorithms to enforce generalized AC* (GAC*) and FDAC* (FDGAC*) for projection-safe soft non-binary constraints. Generalizing the stronger EDAC* is less straightforward. In this paper, we first reveal the oscillation problem when enforcing EDAC* on constraints sharing more than one variable. To avoid oscillation, we propose a weak version of EDAC* and generalize it to weak EDGAC* for non-binary constraints. Weak EDGAC* is stronger than FDGAC* and GAC*, but weaker than VAC and soft k -consistency for k > 2. We also show that weak EDGAC* can be enforced in polynomial time for projection-safe constraints. Extensive experimentation confirms the efficiency of our proposal.