This paper studies peek arc consistency, a reasoning technique that extends the well-known arc consistency technique for constraint satisfaction. In contrast to other more costly extensions of arc consistency that have been studied in the literature, peek arc consistency requires only linear space and quadratic time and can be parallelized in a straightforward way such that it runs in linear time with a linear number of processors. We demonstrate that for various constraint languages, peek arc consistency gives a polynomial-time decision procedure for the constraint satisfaction problem. We also present an algebraic characterization of those constraint languages that can be solved by peek arc consistency, and study the robustness of the algorithm.

Although the CSP (constraint satisfaction problem) is NP-complete, even in the case when all constraints are binary, certain classes of instances are tractable. We study classes of instances defined by excluding subproblems. This approach has recently led to the discovery of novel tractable classes. The complete characterisation of all tractable classes defined by forbidding patterns (where a pattern is simply a compact representation of a set of subproblems) is a challenging problem. We demonstrate a dichotomy in the case of forbidden patterns consisting of either one or two constraints. This has allowed us to discover new tractable classes including, for example, a novel generalisation of 2SAT.

We study propagation of the RegularGcc global constraint. This ensures that each row of a matrix of decision variables satisfies a Regular constraint, and each column satisfies a Gcc constraint. On the negative side, we prove that propagation is NP-hard even under some strong restrictions (e.g. just 3 values, just 4 states in the automaton, or just 5 columns to the matrix). On the positive side, we identify two cases where propagation is fixed parameter tractable. In addition, we show how to improve propagation over a simple decomposition into separate Regular and Gcc constraints by identifying some necessary but insufficient conditions for a solution. We enforce these conditions with some additional weighted row automata. Experimental results demonstrate the potential of these methods on some standard benchmark problems.

We propose a novel inference framework for finding maximal cliques in a weighted graph that satisfy hard constraints. The constraints specify the graph nodes that must belong to the solution as well as mutual exclusions of graph nodes, i.e., sets of nodes that cannot belong to the same solution. The proposed inference is based on a novel particle filter algorithm with state permeations. We apply the inference framework to a challenging problem of learning part-based, deformable object models. Two core problems in the learning framework, matching of image patches and finding salient parts, are formulated as two instances of the problem of finding maximal cliques with hard constraints. Our learning framework yields discriminative part based object models that achieve very good detection rate, and outperform other methods on object classes with large deformation.

We describe Dr.Fill, a program that solves American-style crossword puzzles. From a technical perspective, Dr.Fill works by converting crosswords to weighted CSPs, and then using a variety of novel techniques to find a solution. These techniques include generally applicable heuristics for variable and value selection, a variant of limited discrepancy search, and postprocessing and partitioning ideas. Branch and bound is not used, as it was incompatible with postprocessing and was determined experimentally to be of little practical value. Dr.Filll's performance on crosswords from the American Crossword Puzzle Tournament suggests that it ranks among the top fifty or so crossword solvers in the world.

This work presents Drake, a dynamic executive for temporal plans with choice. Dynamic plan execution strategies allow an autonomous agent to react quickly to unfolding events, improving the robustness of the agent. Prior work developed methods for dynamically dispatching Simple Temporal Networks, and further research enriched the expressiveness of the plans executives could handle, including discrete choices, which are the focus of this work. However, in some approaches to date, these additional choices induce significant storage or latency requirements to make flexible execution possible. Drake is designed to leverage the low latency made possible by a preprocessing step called compilation, while avoiding high memory costs through a compact representation. We leverage the concepts of labels and environments, taken from prior work in Assumption-based Truth Maintenance Systems (ATMS), to concisely record the implications of the discrete choices, exploiting the structure of the plan to avoid redundant reasoning or storage. Our labeling and maintenance scheme, called the Labeled Value Set Maintenance System, is distinguished by its focus on properties fundamental to temporal problems, and, more generally, weighted graph algorithms. In particular, the maintenance system focuses on maintaining a minimal representation of non-dominated constraints. We benchmark Drake's performance on random structured problems, and find that Drake reduces the size of the compiled representation by a factor of over 500 for large problems, while incurring only a modest increase in run-time latency, compared to prior work in compiled executives for temporal plans with discrete choices.

This paper presents an efficient topology information extraction algorithm that is capable of extracting primary topological relations, such as, interior, boundary, and exterior from a single spatial or spatio-temporal object stored in a linear constraint database. Any non-spatial constraints will be preserved so that the input spatio-temporal object’s temporal constraints will not be sacrificed by the algorithm. Based on the three primary topological relations, more topological relations between regions, lines, and points can be defined in a constraint database for future spatial analysis.

Freuder and Elfe (1996) introduced Neighborhood Inverse Consistency (NIC) as a new local consistency property for binary Constraint Satisfaction Problems (CSPs). Two advantages of the algorithm for enforcing NIC is that it automatically adapts its filtering power to the local connectivity of the network and has insignificant space overhead. However, studies on binary CSPs have shown that enforcing NIC is not effective on sparse graphs and too costly on dense graphs. In (Woodward et al. 2011), we introduced an algorithm for enforcing Relational Neighborhood Inverse Consistency (RNIC), which is an extension of NIC to non-binary CSPs. In this paper, we discuss how we enhance the propagation effectiveness of our algorithm and reduce its computational cost by reformulating the dual graph of the CSP. For that purpose, we describe two reformulation techniques that modify the topology of the dual graph without affecting the solution set of the problem. We present the two reformulations and their combinations, and discuss their effects on the consistency property enforced by the algorithm. We also describe a selection policy that nicely ties together the various components of our approach in a consistent, adaptive framework. Finally, we show that our automated selection policy outperforms all approaches in a statistically significant manner.

We present a novel method for generating a wide range of equivalent Boolean encodings of cardinality, while in contrast all previous Boolean encodings of cardinality have only one form. Experiments for applying this method to automated error diagnosis in formal verification of buggy variants of a complex reconfigurable VLIW processor indicate speedup of up to two orders of magnitude, relative to previous encodings of cardinality. Besides automated debugging of hardware and software, the presented Boolean encodings of cardinality have applications to many other problems.

We propose a novel method for combined Routing and Wave-length Assignment (RWA) in optical networks by reformulation to an equivalent Pseudo-Boolean Satisfiability (PB-SAT) problem. We introduce edge observability variables to represent whether an edge is on the optimal route, combined with either a simple or a hierarchical SAT encoding to select a wavelength for that edge only when the edge is on the route. This translation exponentially reduces the size of the solution space, making it independent of the number of wavelengths per link. We present experimental results for routing instances with up to 3,000 nodes, 15,000 edges, and 2,048 wavelengths per edge, and achieve at least 8 orders of magnitude speedup relative to a previous PB-SAT encoding by Aloul et al., such that the speedup is increasing with the number of nodes and edges in the network, and the number of wavelengths per edge. A portfolio of 4 parallel strategies, each based on the new approach and a different hierarchical encoding, resulted in additional speedup of up to 6 times, and reduced the variability of the run times for large networks.