2016 Workshop on Planning and Problem Solving

When? 18 October 2016, 10h30 - 17h30
Where? Auditorium, Campus Poblenou, Universitat Pompeu Fabra

Schedule

• J. Levy (IIIA-CSIC), Real-World SAT Instances.
  No abstract provided.
• F. Manyà & J. R. Soler (IIIA-CSIC), Clause Tableaux for SAT, MaxSAT and MinSAT.
  We will present how clause tableaux for solving SAT can be extended to solve both MaxSAT and MinSAT. Moreover, we will prove that the presented calculi are sound and complete, and discuss how these results can be incorporated into existing MaxSAT/MinSAT solvers.
• D. Larraz (UPC), Compositional Program Analysis using Max-SMT .
  Applications of Max-SMT solvers to program verification are presented. In particular, an automated compositional program verification technique for safety properties based on conditional inductive invariants is introduced. For a given program part (e.g., a single loop) and postcondition, we show how to, using a Max-SMT solver, an inductive invariant together with a precondition can be synthesized so that the precondition ensures the validity of the invariant and that the invariant implies the postcondition. From this, we build a bottom-up program verification framework that propagates preconditions of small program parts as postconditions for preceding program parts.
• J. Coll Caballero (UdG), Solving the Multi-Mode Resource-Constrained Project Scheduling Problem with SMT .
  The Multi-Mode Resource-Constrained Project Scheduling Problem (MRCPSP) is a generalization of the well known Resource-Constrained Project Scheduling Problem (RCPSP). The most common exact approaches for solving this problem are based on branch-and-bound algorithms, mixedinteger linear programming and Boolean satisfiability (SAT). We present a new exact approach for solving this problem, using Satisfiability Modulo Theories (SMT). We provide two encodings into SMT and several reformulation and preprocessing techniques. The optimization algorithm that we propose, uses an SMT solver as an oracle and depending on its answer is able to update the encoding for the next optimization step. We report extensive performance experiments showing the utility of the proposed techniques and the good performance of our approach that allows us to close several open instances.

• J. Larrosa (UPC), Limited Discrepancy AND/OR search .
  No abstract provided.
• P. Meseguer (IIIA-CSIC), Distributed constraint satisfaction with several variables per agent .
  La mayoría de algoritmos para DisCSP suponen agentes con una sola variable. Sin embargo, es natural que cada agente maneje varias variables. Teóricamente, este problema se resuelve mediante decomposition o compilation, que reformulan el problema para obtener agentes con una sola variable, aunque en la práctica estos métodos presentan inconvenientes y no se suelen utilizar (ineficiencia, memoria exponencial desde el principio de la ejecución). Proponemos mantener el problema local de cada agente con las variables originales, de forma que el problema local sea resuelto internamente, y se coordine la resolución del problema global mediante un algoritmo de DisCSP (ABT). Para mantener completitud, se puede necesitar memoria exponencial (caso peor). Proponemos aplicar estas ideas al caso de planificación multiagente bajo la aproximación SATPLAN. Resultados preliminares avalan la factibilidad de esta propuesta.
• H.Geffner (UPF), Width-based Search Algorithms .
  No abstract provided.

• S. Jiménez (UPF), Computing generalized plans with classical planning .
  Generalized planning is the task of generating a single solution valid for multiple planning instances. In this talk we introduce a novel formalism for representing generalized plans that borrows two useful mechanisms from structured programming: control flow and procedure calls. On the one hand control flow structures allow to compactly represent solutions that generalize over different instances. On the other hand procedure calls allow to represent hierarchical and recursive solutions as well as to reuse existing generalized plans. The talk also shows how to compute solutions of this kind with off-the-shelf planners using a generalized planning into classical planning compilation. Interestingly the compilation can incorporate prior knowledge in the form of auxiliary procedures which expands the applicability of our approach to more challenging tasks. Experiments show that a classical planner using our compilation can compute generalized plans to a wide range of generalized planning tasks including sorting lists of variable-size or DFS traversing variable-size binary trees.
• J. Espasa Arxer (UdG), A Semantic Notion of Interference for Planning Modulo Theories .
  The aim of being able to reason about quantities, time, space and much more has been the main objective of the many efforts on the integration of propositional planning with extensions to handle different theories. Planning Modulo Theories (PMT) is an approximation inspired by Satisfiability Modulo Theories (SMT) that generalizes the integration of arbitrary theories with propositional planning. Parallel plans are crucial to reduce plan lengths and hence the time needed to reach a feasible plan in many approaches. Parallelization of actions relies on the notion of (non-)interference, which is usually determined syntactically at compile time. In this paper we present a general semantic notion of interference between actions in PMT. Along its generality, this notion can be efficiently checked at compile time by means of satisfiability checks.
• J. Segovia (UPF), Planning with Partially Specified Behaviors .
  In this paper we present a framework called PPSB for combining reinforcement learning and planning to solve sequential decision problems. Our aim is to show that reinforcement learning and planning complement each other well, in that each can take advantage of the strengths of the other. PPSB uses partial action specifications to decompose sequential decision problems into tasks that serve as an interface between reinforcement learning and planning. On the bottom level, we use reinforcement learning to compute policies for achieving each individual task. On the top level, we use planning to produce a sequence of tasks that achieves an overall goal. Experiments show that our framework is competitive with realistic environments where a robot has to perform some tasks.
• J. Ferrer Mestres (UPF), Combined Task and Motion Planning with Classical Planners Off the Shelf .
  The aim of this work is to provide an alternative integration of task and motion planning where the symbolic and geometrical components are addressed in combination, with neither part taking the back seat. Unlike recent works that have the same motivation, our integration results in problems that can be solved with classical planners off the shelf.
• G. Francès (UPF), Planning in Functional STRIPS: Between Planning and Constraint Satisfaction .
  The derivation of heuristics from first-order planning languages such as Functional STRIPS raises a number of interesting issues at the intersection of planning and constraint satisfaction, that I'll address in the talk.

• J. Lobo (UPF), Using Answer Set Programming for the analysis of distributed algorithms .
  Distributed applications, including routing protocols, can be specified using a Declarative Networking Programming language that extends Datalog. I will describe how one can prove properties of distributed applications with the help of ASP solvers based on these specifications.
• V. Gómez (UPF), Action selection in growing state spaces: Control of Network Structure Growth .
  The dynamical processes taking place on a network depend on its topology. Influencing the growth process of a network therefore has important implications on such dynamical processes. We formulate the problem of influencing the growth of a network as a stochastic optimal control problem in which a structural cost function penalizes undesired topologies. We approximate this control problem with a restricted class of control problems that can be solved using probabilistic inference methods. To deal with the increasing problem dimensionality, we introduce an adaptive importance sampling method for approximating the optimal control. We illustrate this methodology in the context of formation of information cascades, considering the task of influencing the structure of a growing conversation thread, as in Internet forums. Using a realistic model of growing trees, we show that our approach can yield conversation threads with better structural properties than the ones observed without control.
• I. Dotu (GRIB), Combinatorial Optimization in Biology .
  I will describe a couple of applications of Combinatorial Optimization techniques such as Constraint Programming, Local Search and Large Neighborhood Search in RNA Biology.
• P. Gay (UdG), Constraint-programming Approach for Multiset and Sequence Mining .
  Constraint-based data mining is a field that recently has started to receive more attention. Describing a problem through a declarative model enables very descriptive and easy to extend implementations. Our work uses a previous itemset mining model in order to extend it with the capabilities to discover different and interesting patterns that have not been explored yet: multisets and sequences. The classic example domain is the retailer organizations, trying to mine the most common combinations of items bought together. Multisets would allow mining not only this itemsets but also the quantities of each item and sequences the order in with the items are retrieved. In this paper, we provide the background of the original work and we describe the modifications done to the model to extend it and support these new patterns. We also test the new models using real world data to prove their feasibility
• F. Torrent Fontbona (UdG), Assignació de generació d'energia utilitzant auto-organització i canons de justícia distributiva .
  El problema de gestionar (micro)-xarxes elèctriques amb varis generadors distribuïts està esdevenint cada vegada més comú i complex. Aquest consisteix en un problema de resource allocation. Aquí presentem una nova manera d'abordar aquest problema utilitzant un sistema de justícia distribuïda en diferents canons per tal d'incloure varis conceptes de justícia. La rellevància de cada cànon és votada pels diferents agents de la xarxa i l'assignació de recursos s'acaba calculant en base al que diuen els canons al temps que es satisfan les restriccions del problema.