The performance of a constraint model can often be improved by converting a subproblem into a single table constraint (referred to as tabulation). Finding subproblems to tabulate is traditionally a manual and time-intensive process, even for expert modellers. This paper presents TabID, an entirely automated method to identify promising subproblems for tabulation in constraint programming. We introduce a diverse set of heuristics designed to identify promising candidates for tabulation, aiming to improve solver performance. These heuristics are intended to encapsulate various factors that contribute to useful tabulation. We also present additional checks to limit the potential drawbacks of suboptimal tabulation. We comprehensively evaluate our approach using benchmark problems from existing literature that previously relied on manual identification by constraint programming experts of constraints to tabulate. We demonstrate that our automated identification and tabulation process achieves comparable, and in some cases improved results. We empirically evaluate the efficacy of our approach on a variety of solvers, including standard CP (Minion and Gecode), clause-learning CP (Chuffed and OR-Tools) and SAT solvers (Kissat). Our findings highlight the substantial potential of fully automated tabulation, suggesting its integration into automated model reformulation tools.

Puzznic is a tile-matching video game published by Taito in 1989 and ported to many platforms. The player manipulates blocks in a given grid until they match when two or more blocks of the same pattern are adjacent and are removed from play. The goal is to match all patterned blocks in the grid. Puzznic is rich in structure: levels have internal platforms and the blocks are affected by gravity, leading to complex state changes and the possibility of a cascaded series of matches following each move by the player. The puzzle is therefore a significant challenge to model, motivating our study. We study Puzznic from both constraint modelling and AI Planning perspectives, identifying their complementary strengths and weaknesses for this problem. We further exploit our constraint model to produce an automated tool for instance generation, parameterised on the grid, the combination of patterned blocks, and the steps required.

Abstract A classic result of Paul, Pippenger, Szemerédi and Trotter states that ${\textsf {DTIME}}(n) \subsetneq {\textsf {NTIME}}(n)$ DTIME ( n ) ⫋ NTIME ( n ) . The natural question then arises: could the inclusion ${\textsf {DTIME}}(t(n)) \subseteq {\textsf {NTIME}}(n)$ DTIME ( t ( n ) ) ⊆ NTIME ( n ) hold for some superlinear time-constructible function t(n)? If such a function t(n) does exist, then there also exist effective nondeterministic guessing strategies to speed up deterministic computations. In this work, we prove limitations on the effectiveness of nondeterministic guessing to speed up deterministic computations by showing that the existence of effective nondeterministic guessing strategies would have unlikely consequences. In particular, we show that if a subpolynomial amount of nondeterministic guessing could be used to speed up deterministic computation by a polynomial factor, then ${\textsf {P}}~ \subsetneq {\textsf {NTIME}}(n)$ P ⫋ NTIME ( n ) . Furthermore, even achieving a logarithmic speedup at the cost of making every step nondeterministic would show that SAT ∈NTIME(n) under appropriate encodings. Of possibly independent interest, under such encodings we also show that SAT can be decided in O(nlogn) steps on a nondeterministic multitape Turing machine, improving on the well-known O(n(logn)c) bound for some constant but undetermined exponent c ≥ 1.

We introduce techniques for proving superlinear conditional lower bounds for polynomial time problems. In particular, we show that CircuitSAT for circuits with m gates and log(m) inputs (denoted by log-CircuitSAT) is not decidable in essentially-linear time unless the exponential time hypothesis (ETH) is false and k-Clique is decidable in essentially-linear time in terms of the graph's size for all fixed k. Such conditional lower bounds have previously only been demonstrated relative to the strong exponential time hypothesis (SETH). Our results therefore offer significant progress towards proving unconditional superlinear time complexity lower bounds for natural problems in polynomial time.

Structured Neighbourhood Search (SNS) is a framework for constraint-based local search for problems expressed in the Essence abstract constraint specification language. The local search explores a structured neighbourhood, where each state in the neighbourhood preserves a high level structural feature of the problem. SNS derives highly structured problem-specific neighbourhoods automatically and directly from the features of the Essence specification of the problem. Hence, neighbourhoods can represent important structural features of the problem, such as partitions of sets, even if that structure is obscured in the low-level input format required by a constraint solver. SNS expresses each neighbourhood as a constrained optimisation problem, which is solved with a constraint solver. We have implemented SNS, together with automatic generation of neighbourhoods for high level structures, and report high quality results for several optimisation problems.

We study the problem of query containment of conjunctive queries over annotated databases. Annotations are typically attached to tuples and represent metadata, such as probability, multiplicity, comments, or provenance. It is usually assumed that annotations are drawn from a commutative semiring. Such databases pose new challenges in query optimization, since many related fundamental tasks, such as query containment, have to be reconsidered in the presence of propagation of annotations. We axiomatize several classes of semirings for each of which containment of conjunctive queries is equivalent to existence of a particular type of homomorphism. For each of these types, we also specify all semirings for which existence of a corresponding homomorphism is a sufficient (or necessary) condition for the containment. We develop new decision procedures for containment for some semirings which are not in any of these classes. This generalizes and systematizes previous approaches.

We study the problem of query containment of (unions of) conjunctive queries over annotated databases. Annotations are typically attached to tuples and represent metadata such as probability, multiplicity, comments, or provenance. It is usually assumed that annotations are drawn from a commutative semiring. Such databases pose new challenges in query optimization, since many related fundamental tasks, such as query containment, have to be reconsidered in the presence of propagation of annotations.

The constraint satisfaction problem (CSP) is a general problem central to computer science and artificial intelligence. Although the CSP is NP-hard in general, considerable effort has been spent on identifying tractable subclasses. The main two approaches consider structural properties (restrictions on the hypergraph of constraint scopes) and relational properties (restrictions on the language of constraint relations). Recently, some authors have considered hybrid properties that restrict the constraint hypergraph and the relations simultaneously. Our key contribution is the novel concept of a CSP pattern and classes of problems defined by forbidden patterns (which can be viewed as forbidding generic sub-problems). We describe the theoretical framework which can be used to reason about classes of problems defined by forbidden patterns. We show that this framework generalises certain known hybrid tractable classes. Although we are not close to obtaining a complete characterisation concerning the tractability of general forbidden patterns, we prove a dichotomy in a special case: classes of problems that arise when we can only forbid binary negative patterns (generic sub-problems in which only disallowed tuples are specified). In this case we show that all (finite sets of) forbidden patterns define either polynomial-time solvable or NP-complete classes of instances.

The constraint satisfaction problem (CSP) is a central generic problem in artificial intelligence. Considerable progress has been made in identifying properties which ensure tractability in such problems, such as the property of being tree-structured. In this paper we introduce the broken-triangle property, which allows us to define a hybrid tractable class for this problem which significantly generalizes the class of problems with tree structure. We show that the broken-triangle property is conservative (i.e., it is preserved under domain reduction and hence under arc consistency operations) and that there is a polynomial-time algorithm to determine an ordering of the variables for which the broken-triangle property holds (or to determine that no such ordering exists). We also present a non-conservative extension of the broken-triangle property which is also sufficient to ensure tractability and can be detected in polynomial time.