We address the problem of providing a logical formalization of arithmetic in declarative modelling languages for NP search problems. The challenge is to simultaneously allow quantification over an infinite domain such as the natural numbers, provide natural modelling facilities, and control expressive power of the language. To address the problem, we introduce an extension of the model expansion (MX) based framework to finite structures embedded in an infinite secondary structure, together with "double-guarded" logics for representing MX specifications for these structures. The logics also contain multi-set functions (aggregate operations). Our main result is that these logics capture the complexity class NP on "small-cost" arithmetical structures. 

Real-time heuristic search algorithms are used for planning by agents in situations where a constant-bounded amount of deliberation time is required for each action regardless of the problem size.  Such algorithms interleave their planning and execution to ensure real-time response. Furthermore, to guarantee completeness, they typically store improved heuristic estimates for previously expanded states.  Although subsequent planning steps can benefit from updated heuristic estimates, many of the same states are expanded over and over again.   Here we propose a variant of the A* algorithm, Time-Bounded A* (TBA*), that guarantees real-time response. In the domain of path-finding on video-game maps TBA* expands an order of magnitude fewer states than traditional real-time search algorithms, while finding paths of comparable quality. It reaches the same level of performance as recent state-of-the-art real-time search algorithms but, unlike these, requires neither state-space abstractions nor pre-computed pattern databases.

Skat is Germany's national card game played by millions of players around the world. In this paper, we present the world's first computer skat player that plays at the level of human experts. This performance is achieved by improving state evaluations using game data produced by human players and by using these state evaluations to perform inference on the unobserved hands of opposing players. Our results demonstrate the gains from adding inference to an imperfect information game player and show that training on data from average human players can result in expert-level playing strength.

Monte Carlo tree search has brought significant improvements to the level of computer players in games such as Go, but so far it has not been used very extensively in games of strongly imperfect information with a dynamic board and an emphasis on risk management and decision making under uncertainty. In this paper we explore its application to the game of Kriegspiel (invisible chess), providing three Monte Carlo methods of increasing strength for playing the game with little specific knowledge. We compare these Monte Carlo agents to the strongest known minimax-based Kriegspiel player, obtaining significantly better results with a considerably simpler logic and less domain-specific knowledge.

The rectangle packing problem consists of finding an enclosing rectangle of smallest area that can contain a given set of rectangles without overlap. Our algorithm picks the x-coordinates of all the rectangles before picking any of the y-coordinates. For the x-coordinates, we present a dynamic variable ordering heuristic and an adaptation of a pruning algorithm used in previous solvers. We then transform the rectangle packing problem into a perfect packing problem that has no empty space, and present inference rules to reduce the instance size. For the y-coordinates we search a space that models empty positions as variables and rectangles as values. Our solver is over 19 times faster than the previous state-of-the-art on the largest problem solved to date, allowing us to extend the known solutions for a consecutive-square packing benchmark from N=27 to N=32.

Alpha-Beta is the most common game tree search algorithm, due to its high-performance and straightforward implementation. In practice one must find the best trade-off between heuristic evaluation time and bringing the subset of nodes explored closer to a minimum proof graph. In this paper we present a series of structural properties of minimum proof graphs that help us to prove that finding such graphs is NP-hard for arbitrary DAG inputs, but can be done in linear time for trees. We then introduce the class of fastest-cut-first search heuristics that aim to approximate minimum proof graphs by sorting moves based on approximations of sub-DAG values and sizes. To explore how various aspects of the game tree (such as branching factor and distribution of move values) affect the performance of Alpha-Beta we introduce the class of ``Prefix Value Game Trees'' that allows us to label interior nodes with true minimax values on the fly without search. Using these trees we show that by explicitly attempting to approximate a minimum game tree we are able to achieve performance gains over Alpha-Beta with common extensions.

We study a multi-step hider-seeker game where the hider is moving on a graph and, in each step, the seeker is able to search c subsets of the graph nodes. We model this game as a zero-sum Bayesian game, which can be solved in weakly polynomial time in the players' action spaces. The seeker's action space is exponential in c, and both players' action spaces are exponential in the game horizon. To manage this intractability, we use a column/constraint generation approach for both players. This approach requires an oracle to determine best responses for each player. However, we show that computing a best response for the seeker is NP-hard, even for a single-step game when c is part of the input, and that computing a best response is NP-hard for both players for the multi-step game, even if c = 1. An integer programming formulation of the best response for the hider is practical for moderate horizons, but computing an exact seeker best response is impractical due to the exponential dependence on both c and the horizon. We therefore develop an approximate best response oracle with bounded suboptimality for the seeker. We prove performance bounds on the strategy that results when column/constraint generation with approximate best responses converges, and we measure the performance of our algorithm in simulations. In our experimental results, column/constraint generation converges to near-minimax strategies for both players fairly quickly.

Incremental search algorithms reuse information from previous searches to speed up the current search and are thus often able to find shortest paths for series of similar search problems faster than by solving each search problem independently from scratch. However, they do poorly on moving target search problems, where both the start and goal cells change over time. In this paper, we thus develop Fringe-Retrieving A* (FRA*), an incremental version of A* that repeatedly finds shortest paths for moving target search in known gridworlds. We demonstrate experimentally that it runs up to one order of magnitude faster than a variety of state-of-the-art incremental search algorithms applied to moving target search in known gridworlds.

Local pattern mining is concerned with finding the set of patterns that satisfy a constraint in a database. We study local pattern mining in the context of ProbLog, a probabilistic Prolog system, and introduce an approach for finding correlated patterns in the form of queries in such a Prolog system. The approach combines principles of inductive logic programming, data mining and statistical relational learning. Experiments on a challenging biological network mining task provide evidence for the interestingness of the approach.

A conservative estimate of the latter number is the number of distinct board Using efficient methods that reduce the search states in which the board is at most half full. This estimate space, we design an algorithm strong enough to includes some invalid states: those in which one player already solve all 8 8 Hex openings.