Most planners are based on grounding, that is, generating all instances of a parameterized action during a preprocessing phase. For some problems the number of ground actions is too high, causing a performance bottleneck. Building upon an existing approach, we present an enhanced method to split action schemas automatically during the grounding phase, to reduce the number of ground actions. First, we propose to exploit the structural knowledge of the problems to have a more informative dependency graph. Then, we suggest a better objective function to define and choose the best split. Finally, we present a more effective search to find it. We experimentally measure the impact of each of these improvements, and show that our approach significantly outperforms the state of the art.

Finding a graph with given properties occurs as a sub-problem of many important problems in A.I. and other areas of computer science. Main approaches to solving such problems include automated reasoning and constraint satisfaction methods. These can often be substantially sped up by considering only a subset of graphs for each equivalence class of isomorphic graphs, motivating the use of symmetry-breaking constraints for graphs. We present a symmetry-breaking constraint for directed graphs, generalizing earlier works that have presented such constraints for undirected graphs without loops, and experimentally demonstrate their effectiveness.

Indirect effects of agent's actions have traditionally been formalized as condition-effect rules that always fire whenever applicable, after each action taken by the agent. In this work, we investigate a core problem of indirect effects, the possibility of arbitrarily or infinitely long sequences of rule firings. Specifically we investigate the termination of rule firings, as well as their confluence, that is, the uniqueness of the state that is ultimately reached. Both problems turn out to be PSPACE-complete. After this, we devise practically interesting syntactic and structural restrictions that guarantee polynomial-time termination and confluence tests. Finally, in the context of planning languages that support indirect effects, we propose new implementation technologies.

We introduce novel methods for encoding acyclicity and s-t-reachability constraints for propositional formulas with underlying directed graphs, based on vertex elimination graphs, which makes them suitable for cases where the underlying graph has a low directed elimination width. In contrast to solvers with ad hoc constraint propagators for graph constraints such as GraphSAT, our methods encode these constraints as standard propositional clauses, making them directly applicable with any SAT solver. An empirical study demonstrates that our methods do often outperform both earlier encodings of these constraints as well as GraphSAT especially when underlying graphs have a low directed elimination width.

We introduce a novel method for encoding cost optimal delete-free STRIPS Planning as SAT. Our method is based on representing relaxed plans as partial functions from the set of propositions to the set of actions. This function can map any proposition to a unique action that adds the proposition during execution of the relaxed plan. We show that a relaxed plan can be produced by maintaining acyclicity in the graph of all causal relations among propositions, represented by the mentioned partial function. We also show that by efficient encoding of action cost propagation and enforcing a series of upper bounds on the total costs of the output plan, an optimal plan can effectively be produced for a given delete-free STRIPS problem. Our empirical results indicate that this method is quite competitive with the state of the art, demonstrating a better coverage compared to that of competing methods on standard STRIPS planning benchmark problems.

Abstract Many knowledge representation tasks involve trees or similar structures as abstract datatypes. However, devising compact and efficient declarative representations of such structural properties is non-obvious and can be challenging indeed. In this article, we take a number of acyclicity properties into consideration and investigate various logic-based approaches to encode them. We use answer set programming as the primary representation language but also consider mappings to related formalisms, such as propositional logic, difference logic and linear programming. We study the compactness of encodings and the resulting computational performance on benchmarks involving acyclic or tree structures.

Computation of invariants, which are approximate reachability information for state-space search problems such as AI planning, has been considered to be more scalable when using a schematic representation of actions/events rather than an instantiated/ground representation. A disadvantage of schematic algorithms, however, is their complexity, which also leads to high runtimes when the number of schematic events/actions is high. We propose algorithms that reduce the problem of finding schematic invariants to solving a smaller ground problem.

We propose more scalable encodings of temporal planning in SMT. The first contribution is practical clock-based encodings of resources and effect delays. Existing encodings of effect delays (Shin and Davis, 2015) have a quadratic size, due to the necessity to determine the time differences between steps for a linear number of steps. Clocks improve this to linear. The second contribution is a new relaxed scheme for steps. Existing schemes require a step for every time point with discontinuous change. This is relaxed, improving scalability.

The problem of planning or discrete control for timed system has earlier been solved with various constraint-based solution methods, including Constraint Programming, SAT solvers, SAT modulo Theories solvers, and Mixed Integer-Linear Programming. In this work we investigate the encoding of time in such constraint-based representations. A main issue with existing encodings is the necessity to allow arbitrary interleavings of concurrent actions' starting and ending times. The complex combinatorics of this can lead to poor scalability of leading search methods. We show how real or rational time in temporal models can in many practically important cases be replaced by integer time, and how this leads to far simpler encodings of planning as constraints. We demonstrate that the simplified encodings substantially improve the scalability of constraint-based planning.

We propose revisions to the research agenda in Automated Planning. The proposal is based on a review of the role of the Planning Domain Definition Language (PDDL) in the activities of the AI planning community and the impact of PDDL on parts of its research agenda. We specifically show how specific properties of PDDL have impacted research on planning, by putting emphasis on certain research topics and complicating others. We argue that the development of more advanced modeling languages would be — analogously to the impact PDDL has had — a low overhead and smooth route for the ICAPS community shift its research focus to increasingly promising and relevant research topics.

Answer set programming (ASP) is a declarative programming paradigm for solving search problems arising in knowledge-intensive domains. One viable way to implement the computation of answer sets corresponding to problem solutions is to recast a logic program as a Boolean satisfiability (SAT) problem and to use existing SAT solver technology for the actual search. Such mappings can be obtained by augmenting Clark's completion with constraints guaranteeing the strong justifiability of answer sets. To this end, we consider an extension of SAT by graphs subject to an acyclicity constraint, called SAT modulo acyclicity. We devise a linear embedding of logic programs and study the performance of answer set computation with SAT modulo acyclicity solvers.

We investigate the problem of learning the structure of a Markov network from data. It is shown that the structure of such networks can be described in terms of constraints which enables the use of existing solver technology with optimization capabilities to compute optimal networks starting from initial scores computed from the data. To achieve efficient encodings, we develop a novel characterization of Markov network structure using a balancing condition on the separators between cliques forming the network. The resulting translations into propositional satisfiability and its extensions such as maximum satisfiability, satisfiability modulo theories, and answer set programming, enable us to prove the optimality of networks which have been previously found by stochastic search.

Logic, and declarative representation of knowledge in general, have long been a preferred framework for problem solving in AI. However, specific subareas of AI have been eager to abandon general-purpose knowledge representation in favor of methods that seem to address their computational core problems better. In planning, for example, state-space search has in the last several years been preferred to logic-based methods such as SAT. In our recent work, we have demonstrated that the observed performance differences between SAT and specialized state-space search methods largely go back to the difference between a blind (or at least planning-agnostic) and a planning-specific search method. If SAT search methods are given even simple heuristics which make the search goal-directed, the efficiency differences disappear.

We study the relationship between optimal planning algorithms, in the form of (iterative deepening) A with (forward) state-space search, and the reduction of the problem to SAT. Our results establish a strict dominance relation between the two approaches:

Many forms of reasoning about actions and planning can be reduced to regression, the computation of the weakest precondition a state has to satisfy to guarantee the satisfaction of another condition in the successor state. In this work we formalize a general syntactic regression operation for ground PDDL operators, show its correctness, and define a composition operation based on regression. As applications we present a very simple yet powerful algorithm for computing invariants, as well as a generalization of the hnheuristic of Haslum and Geffner to PDDL.

Control of networks like those for transportation, power distribution, communication to name a few, provides challenges to planning and scheduling. Many problems can be defined in terms of a basic state space model, but more general problems require an expressive language for talking about the topology and connectivity of the system, which are outside the scope of standard planning languages. In this work we introduce a general framework for defining planning languages for networked systems, with capability to express properties of connectivity and topology of such systems.

The research on conditional planning rejects the assumptions that there is no uncertainty or incompleteness of knowledge with respect to the state and changes of the system the plans operate on. Without these assumptions the sequences of operations that achieve the goals depend on the initial state and the outcomes of nondeterministic changes in the system. This setting raises the questions of how to represent the plans and how to perform plan search. The answers are quite different from those in the simpler classical framework. In this paper, we approach conditional planning from a new viewpoint that is motivated by the use of satisfiability algorithms in classical planning. Translating conditional planning to formulae in the propositional logic is not feasible because of inherent computational limitations. Instead, we translate conditional planning to quantified Boolean formulae. We discuss three formalizations of conditional planning as quantified Boolean formulae, and present experimental results obtained with a theorem-prover.

In default reasoning, usually not all possible ways of resolving conflicts between default rules are acceptable. Criteria expressing acceptable ways of resolving the conflicts may be hardwired in the inference mechanism, for example specificity in inheritance reasoning can be handled this way, or they may be given abstractly as an ordering on the default rules. In this article we investigate formalizations of the latter approach in Reiter's default logic. Our goal is to analyze and compare the computational properties of three such formalizations in terms of their computational complexity: the prioritized default logics of Baader and Hollunder, and Brewka, and a prioritized default logic that is based on lexicographic comparison. The analysis locates the propositional variants of these logics on the second and third levels of the polynomial hierarchy, and identifies the boundary between tractable and intractable inference for restricted classes of prioritized default theories.