In the algebraic approach to CSP (Constraint Satisfaction Problem), the complexity of constraint languages is studied using closure operations called polymorphisms. Many of these operations are known to induce tractability of any language they preserve. We focus on the meta-problem: given a language G, decide if G has a polymorphism with nice properties. We design an algorithm that decides in polynomial-time if a constraint language has a conservative Mal'tsev polymorphism, and outputs one if one exists. As a corollary we obtain that the class of conservative Mal'tsev constraints is uniformly tractable, and we conjecture that this result remains true in the non-conservative case.

Many recent algorithms for approximate model counting are based on a reduction to combinatorial searches over random subsets of the space defined by parity or XOR constraints. Long parity constraints (involving many variables) provide strong theoretical guarantees but are computationally difficult. Short parity constraints are easier to solve but have weaker statistical properties. It is currently not known how long these parity constraints need to be. We close the gap by providing matching necessary and sufficient conditions on the required asymptotic length of the parity constraints. Further, we provide a new family of lower bounds and the first non-trivial upper bounds on the model count that are valid for arbitrarily short XORs. We empirically demonstrate the effectiveness of these bounds on model counting benchmarks and in a Satisfiability Modulo Theory (SMT) application motivated by the analysis of contingency tables in statistics.

Many inference problems are naturally formulated using hard and soft constraints over relational domains: the desired solution must satisfy the hard constraints, while optimizing the objectives expressed by the soft constraints. Existing techniques for solving such constraints rely on efficiently grounding a sufficient subset of constraints that is tractable to solve. We present an eager-lazy grounding algorithm that eagerly exploits proofs and lazily refutes counterexamples. We show that our algorithm achieves significant speedup over existing approaches without sacrificing soundness for real-world applications from information retrieval and program analysis.

Uncertainty in activity durations is a key characteristic of many real world scheduling problems in manufacturing, logistics and project management. RCPSP/max with durational uncertainty is a general  model that can be used to represent durational uncertainty in a wide variety of scheduling problems where there exist resource constraints. However, computing schedules or execution strategies for RCPSP/max with durational uncertainty is NP-hard and hence we focus on providing approximation methods in this paper. We provide a principled approximation approach based on Sample Average Approximation (SAA) to compute proactive schedules for RCPSP/max  with durational uncertainty. We further contribute an extension to SAA for improving scalability significantly without sacrificing on solution quality. Not only is our approach able to compute schedules at comparable runtimes as existing approaches, it also provides lower α-quantile makespan (also referred to as α-robust makespan) values than the best known approach on benchmark problems from the literature.

In this paper we propose an approach to modeling syntactically-motivated skeletal structure of source sentence for machine translation. This model allows for application of high-level syntactic transfer rules and low-level non-syntactic rules. It thus involves fully syntactic, non-syntactic, and partially syntactic derivations via a single grammar and decoding paradigm. On large-scale Chinese-English and English-Chinese translation tasks, we obtain an average improvement of +0.9 BLEU across the newswire and web genres.

The application of DCOP models to large problems faces two main limitations: (i) Modeling limitations, as each agent can handle only a single variable of the problem; and (ii) Resolution limitations, as current approaches do not exploit the local problem structure withineach agent. This paper proposes a novel Multi-Variable Agent (MVA) DCOP decompositiontechnique, which: (i) Exploits the co-locality of each agent's variables, allowing us to adopt efficient centralized techniques within each agent; (ii) Enables the use of hierarchical parallel models and proposes the use of GPUs; and (iii) Reduces the amount of computation and communication required in several classes of DCOP algorithms.

The decision to take vaccinations and other protective interventions for avoiding an infection is a natural game-theoretic setting. Most of the work on vaccination games has focused on decisions at the start of an epidemic. However, a lot of people defer their vaccination decisions, in practice. For example, in the case of the seasonal flu, vaccination rates gradually increase, as the epidemic rate increases. This motivates the study of temporal vaccination games, in which vaccination decisions can be made more than once. An important issue in the context of temporal decisions is that of resource limitations, which may arise due to production and distribution constraints. While there has been some work on temporal vaccination games, resource constraints have not been considered. In this paper, we study temporal vaccination games for epidemics in the SI (susceptible-infectious) model, with resource constraints in the form of a repeated game in complex social networks, with budgets on the number of vaccines that can be taken at any time. We find that the resource constraints and the vaccination and infection costs have a significant impact on the structure of Nash equilibria (NE). In general, the budget constraints can cause NE to become very inefficient, and finding efficient NE as well as the social optimum are NP-hard problems. We develop algorithms for finding NE and approximating the social optimum. We evaluate our results using simulations on different kinds of networks.

Outlier detection has been studied extensively and employed in diverse applications in the past decades. In this paper we formulate a related yet understudied problem which we call outlier description. This problem often arises in practice when we have a small number of data instances that had been identified to be outliers and we wish to explain why they are outliers. We propose a framework based on constraint programming to find an optimal subset of features that most differentiates the outliers and normal instances. We further demonstrate the framework offers great flexibility in incorporating diverse scenarios arising in practice such as multiple explanations and human in the loop extensions. We empirically evaluate our proposed framework on real datasets, including medical imaging and text corpus, and demonstrate how the results are useful and interpretable in these domains.

Qualitative spatio-temporal reasoning is an active research area in Artificial Intelligence. In many situations there is a need to reason about intertemporal qualitative spatial relations, i.e. qualitative relations between spatial regions at different time-points. However, these relations can never be explicitly observed since they are between regions at different time-points. In applications where the qualitative spatial relations are partly acquired by for example a robotic system it is therefore necessary to infer these relations. This problem has, to the best of our knowledge, not been explicitly studied before. The contribution presented in this paper is two-fold. First, we present a spatio-temporal logic MSTL, which allows for spatio-temporal stream reasoning. Second, we define the concept of a landmark as a region that does not change between time-points and use these landmarks to infer qualitative spatio-temporal relations between non-landmark regions at different time-points. The qualitative spatial reasoning is done in RCC-8, but the approach is general and can be applied to any similar qualitative spatial formalism.

We investigate the problem of repacking stations in the FCC's upcoming, multi-billion-dollar "incentive auction". Early efforts to solve this problem considered mixed-integer programming formulations, which we show are unable to reliably solve realistic, national-scale problem instances. We describe the result of a multi-year investigation of alternatives: a solver, SATFC, that has been adopted by the FCC for use in the incentive auction. SATFC is based on a SAT encoding paired with a wide range of techniques: constraint graph decomposition; novel caching mechanisms that allow for reuse of partial solutions from related, solved problems; algorithm configuration; algorithm portfolios; and the marriage of local-search and complete solver strategies. We show that our approach solves virtually all of a set of problems derived from auction simulations within the short time budget required in practice.