We aim at providing a foundation of a theory of "good" SAT representations F of boolean functions f. We argue that the hierarchy UC_k of unit-refutation complete clause-sets of level k, introduced by the authors, provides the most basic target classes, that is, F in UC_k is to be achieved for k as small as feasible. If F does not contain new variables, i.e., F is equivalent (as a CNF) to f, then F in UC_1 is similar to "achieving (generalised) arc consistency" known from the literature (it is somewhat weaker, but theoretically much nicer to handle). We show that for polysize representations of boolean functions in this sense, the hierarchy UC_k is strict. The boolean functions for these separations are "doped" minimally unsatisfiable clause-sets of deficiency 1; these functions have been introduced in [Sloan, Soerenyi, Turan, 2007], and we generalise their construction and show a correspondence to a strengthened notion of irredundant sub-clause-sets. Turning from lower bounds to upper bounds, we believe that many common CNF representations fit into the UC_k scheme, and we give some basic tools to construct representations in UC_1 with new variables, based on the Tseitin translation. Note that regarding new variables the UC_1-representations are stronger than mere "arc consistency", since the new variables are not excluded from consideration.

The Stable Marriage Problem (SMP) is a well-known matching problem first introduced and solved by Gale and Shapley (1962). Several variants and extensions to this problem have since been investigated to cover a wider set of applications. Each time a new variant is considered, however, a new algorithm needs to be developed and implemented. As an alternative, in this paper we propose an encoding of the SMP using Answer Set Programming (ASP). Our encoding can easily be extended and adapted to the needs of specific applications. As an illustration we show how stable matchings can be found when individuals may designate unacceptable partners and ties between preferences are allowed. Subsequently, we show how our ASP based encoding naturally allows us to select specific stable matchings which are optimal according to a given criterion. Each time, we can rely on generic and efficient off-the-shelf answer set solvers to find (optimal) stable matchings.

Over the last two decades, propositional satisfiability (SAT) has become one of the most successful and widely applied techniques for the solution of NP-complete problems. The aim of this paper is to investigate theoretically how Sat can be utilized for the efficient solution of problems that are harder than NP or co-NP. In particular, we consider the fundamental reasoning problems in propositional disjunctive answer set programming (ASP), Brave Reasoning and Skeptical Reasoning, which ask whether a given atom is contained in at least one or in all answer sets, respectively. Both problems are located at the second level of the Polynomial Hierarchy and thus assumed to be harder than NP or co-NP. One cannot transform these two reasoning problems into SAT in polynomial time, unless the Polynomial Hierarchy collapses. We show that certain structural aspects of disjunctive logic programs can be utilized to break through this complexity barrier, using new techniques from Parameterized Complexity. In particular, we exhibit transformations from Brave and Skeptical Reasoning to SAT that run in time O(2^k n^2) where k is a structural parameter of the instance and n the input size. In other words, the reduction is fixed-parameter tractable for parameter k. As the parameter k we take the size of a smallest backdoor with respect to the class of normal (i.e., disjunction-free) programs. Such a backdoor is a set of atoms that when deleted makes the program normal. In consequence, the combinatorial explosion, which is expected when transforming a problem from the second level of the Polynomial Hierarchy to the first level, can now be confined to the parameter k, while the running time of the reduction is polynomial in the input size n, where the order of the polynomial is independent of k.

One of the big challenges in the development of probabilistic relational (or probabilistic logical) modeling and learning frameworks is the design of inference techniques that operate on the level of the abstract model representation language, rather than on the level of ground, propositional instances of the model. Numerous approaches for such "lifted inference" techniques have been proposed. While it has been demonstrated that these techniques will lead to significantly more efficient inference on some specific models, there are only very recent and still quite restricted results that show the feasibility of lifted inference on certain syntactically defined classes of models. Lower complexity bounds that imply some limitations for the feasibility of lifted inference on more expressive model classes were established early on in (Jaeger 2000). However, it is not immediate that these results also apply to the type of modeling languages that currently receive the most attention, i.e., weighted, quantifier-free formulas. In this paper we extend these earlier results, and show that under the assumption that NETIME =/= ETIME, there is no polynomial lifted inference algorithm for knowledge bases of weighted, quantifier- and function-free formulas. Further strengthening earlier results, this is also shown to hold for approximate inference, and for knowledge bases not containing the equality predicate.

The output of the former type of recognition is a set of activities taking place in a short period of time: 'short-term activities'. The output of the latter type of recognition is a set of'long-term activities', ie predefined temporal combinations of short-term activities. We focus on high-level recognition. We define a set of long-term activities of interest, such as'fighting' and'meeting', as temporal combinations of short-term activities -- eg, 'walking', 'running', and'inactive' (standing still) -- using a logic programming implementation of the Event Calculus [9]. More precisely, we employ the Event Calculus to express the temporal constraints on a set of short-term activities that, if satisfied, lead to the recognition of a long-term activity. We presented preliminary results on activity recognition from video content in [2].

We present a system for recognising human activity given a symbolic representation of video content. The input of our system is a set of time-stamped short-term activities (STA) detected on video frames. The output is a set of recognised long-term activities (LTA), which are pre-defined temporal combinations of STA. The constraints on the STA that, if satisfied, lead to the recognition of a LTA, have been expressed using a dialect of the Event Calculus. In order to handle the uncertainty that naturally occurs in human activity recognition, we adapted this dialect to a state-of-the-art probabilistic logic programming framework. We present a detailed evaluation and comparison of the crisp and probabilistic approaches through experimentation on a benchmark dataset of human surveillance videos.

Probabilistic logic programs are logic programs in which some of the facts are annotated with probabilities. This paper investigates how classical inference and learning tasks known from the graphical model community can be tackled for probabilistic logic programs. Several such tasks such as computing the marginals given evidence and learning from (partial) interpretations have not really been addressed for probabilistic logic programs before. The first contribution of this paper is a suite of efficient algorithms for various inference tasks. It is based on a conversion of the program and the queries and evidence to a weighted Boolean formula. This allows us to reduce the inference tasks to well-studied tasks such as weighted model counting, which can be solved using state-of-the-art methods known from the graphical model and knowledge compilation literature. The second contribution is an algorithm for parameter estimation in the learning from interpretations setting. The algorithm employs Expectation Maximization, and is built on top of the developed inference algorithms. The proposed approach is experimentally evaluated. The results show that the inference algorithms improve upon the state-of-the-art in probabilistic logic programming and that it is indeed possible to learn the parameters of a probabilistic logic program from interpretations.

Many real world problems naturally appear as constraints satisfaction problems (CSP), for which very efficient algorithms are known. Most of these involve the combination of two techniques: some direct propagation of constraints between variables (with the goal of reducing their sets of possible values) and some kind of structured search (depth-first, breadth-first,...). But when such blind search is not possible or not allowed or when one wants a 'constructive' or a 'pattern-based' solution, one must devise more complex propagation rules instead. In this case, one can introduce the notion of a candidate (a 'still possible' value for a variable). Here, we give this intuitive notion a well defined logical status, from which we can define the concepts of a resolution rule and a resolution theory. In order to keep our analysis as concrete as possible, we illustrate each definition with the well known Sudoku example. Part I proposes a general conceptual framework based on first order logic; with the introduction of chains and braids, Part II will give much deeper results.

Probability answer set programming is a declarative programming that has been shown effective for representing and reasoning about a variety of probability reasoning tasks. However, the lack of probability aggregates, e.g. {\em expected values}, in the language of disjunctive hybrid probability logic programs (DHPP) disallows the natural and concise representation of many interesting problems. In this paper, we extend DHPP to allow arbitrary probability aggregates. We introduce two types of probability aggregates; a type that computes the expected value of a classical aggregate, e.g., the expected value of the minimum, and a type that computes the probability of a classical aggregate, e.g, the probability of sum of values. In addition, we define a probability answer set semantics for DHPP with arbitrary probability aggregates including monotone, antimonotone, and nonmonotone probability aggregates. We show that the proposed probability answer set semantics of DHPP subsumes both the original probability answer set semantics of DHPP and the classical answer set semantics of classical disjunctive logic programs with classical aggregates, and consequently subsumes the classical answer set semantics of the original disjunctive logic programs. We show that the proposed probability answer sets of DHPP with probability aggregates are minimal probability models and hence incomparable, which is an important property for nonmonotonic probability reasoning.

We present a unified logical framework for representing and reasoning about both probability quantitative and qualitative preferences in probability answer set programming [Saad and Pontelli, 2006; Saad, 2006; Saad, 2007a], called probability answer set optimization programs. The proposed framework is vital to allow defining probability quantitative preferences over the possible outcomes of qualitative preferences. We show the application of probability answer set optimization programs to a variant of the well-known nurse restoring problem [Bard and Purnomo, 2005], called the nurse restoring with probability preferences problem. To the best of our knowledge, this development is the first to consider a logical framework for reasoning about probability quantitative preferences, in general, and reasoning about both probability quantitative and qualitative preferences in particular.