Fundamenta Informaticae - Volume 102, issue 3-4

Authors: Gavanelli, Marco | Mancini, Toni

Article Type: Other

DOI: 10.3233/FI-2010-306

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. i-ii, 2010

Authors: Balafoutis, Thanasis | Stergiou, Kostas

Article Type: Research Article

Abstract: A key factor that can dramatically reduce the search space during constraint solving is the criterion under which the variable to be instantiated next is selected. For this purpose numerous heuristics have been proposed. Some of the best of such heuristics exploit information about failures gathered throughout search and recorded in the form of constraint weights, while others measure the importance of variable assignments in reducing the search space. In this work we experimentally evaluate the most recent and powerful variable ordering heuristics, and new variants of them, over a wide range of benchmarks. Results demonstrate that heuristics based on …failures are in general more efficient. Based on this, we then derive new revision ordering heuristics that exploit recorded failures to efficiently order the propagation list when arc consistency is maintained during search. Interestingly, in addition to reducing the number of constraint checks and list operations, these heuristics are also able to cut down the size of the explored search tree. Show more

Keywords: Constraint Satisfaction, Search heuristics, Variable ordering, Revision ordering

DOI: 10.3233/FI-2010-307

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 229-261, 2010

Authors: Brito, Ismel | Meseguer, Pedro

Article Type: Research Article

Abstract: Some distributed constraint optimization algorithms use a linear number of messages in the number of agents, but of exponential size. This is often the main limitation for their practical applicability. Here we present some distributed algorithms for these problems when they are arranged in a tree of agents. The exact algorithm, DCTE, computes the optimal solution but requires messages of size exp(s), where s is a structural parameter. Its approximate version, DMCTE(r), requires smaller messages of size exp(r), r < s, at the cost of computing approximate solutions. It provides a cost interval that bounds the error of the approximation. …Using the technique of cost function filtering, we obtain DMCTEf(r). Combining cost function filtering with bound reasoning, we propose DIMCTEf, an algorithm based on repeated executions of DMCTEf(r) with increasing r. DIMCTEf uses messages of previous iterations to decrease the size of messages in the current iteration, which allows to alleviate their high size. We provide evidences of the benefits of our approach on two benchmarks. Show more

Keywords: Distributed constraint optimization, distributed cluster-tree elimination, function filtering

DOI: 10.3233/FI-2010-308

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 263-286, 2010

Authors: Gerevini, Alfonso E. | Serina, Ivan

Article Type: Research Article

Abstract: Fast plan adaptation is important in many AI applications. From a theoretical point of view, in the worst case adapting an existing plan to solve a new problem is no more efficient than a complete regeneration of the plan. However, in practice plan adaptation can be much more efficient than plan generation, especially when the adapted plan can be obtained by performing a limited amount of changes to the original plan. In this paper, we investigate a domain-independent method for plan adaptation that modifies the original plan by replanning within limited temporal windows containing portions of the plan that need …to be revised. Each window is associated with a particular replanning subproblem that contains some “heuristic goals” facilitating the plan adaptation, and that can be solved using different planning methods. An experimental analysis shows that, in practice, adapting a given plan for solving a new problem using our techniques can be much more efficient than replanning from scratch. Show more

Keywords: Plan Adaptation and Reuse, Graphplan-based Algorithms, Plan efficiency, Mixed-initiative planning

DOI: 10.3233/FI-2010-309

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 287-323, 2010

Authors: Montali, Marco | Torroni, Paolo | Chesani, Federico | Mello, Paola | Alberti, Marco | Lamma, Evelina

Article Type: Research Article

Abstract: We discuss the static verification of declarative Business Processes. We identify four desiderata about verifiers, and propose a concrete framework which satisfies them. The framework is based on the ConDec graphical notation for modeling Business Processes, and on Abductive Logic Programming technology for verification of properties. Empirical evidence shows that our verification method seems to perform and scale better, in most cases, than other state of the art techniques (model checkers, in particular). A detailed study of our framework’s theoretical properties proves that our approach is sound and complete when applied to ConDec models that do not contain loops, and …it is guaranteed to terminate when applied to models that contain loops. Show more

Keywords: static verification, business process management, declarative business process modeling, abductive logic programming, model checking

DOI: 10.3233/FI-2010-310

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 325-361, 2010

Authors: Morgado, António | Marques-Silva, Joao

Article Type: Research Article

Abstract: Phylogenetic analysis is a widely used technique, for example in biology and biomedical sciences. The construction of phylogenies can be computationally hard. A commonly used solution for construction of phylogenies is to start from a set of biological species and relations among those species. This work addresses the case where the relations among species are specified as quartet topologies. Moreover, the problem to be solved consists of computing a phylogeny that satisfies the maximum number of quartet topologies. This is referred to as the Maximum Quartet Consistency (MQC) problem, and represents an NP-hard optimization problem. MQC has been solved both …heuristically and exactly. Exact solutions for MQC include those based on Constraint Programming, Answer Set Programming, Pseudo-Boolean Optimization (PBO), and Satisfiability Modulo Theories (SMT). This paper provides a comprehensive overview of the use of PBO and SMT for solving MQC, and builds on recent work in this area. Moreover, the paper provides new insights on how to use SMT for solving optimization problems, by focusing on the concrete case of MQC. The solutions based on PBO and SMT were experimentally compared with other exact solutions. The results show that for instances with small percentage of quartet errors, the models based on SMT can be competitive, whereas for instances with higher number of quartet errors the PBO models are more efficient. Show more

Keywords: maximum quartet consistency, optimization algorithms, pseudo-boolean optimization, satisfiability modulo theories

DOI: 10.3233/FI-2010-311

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 363-389, 2010

Authors: Pulina, Luca | Tacchella, Armando

Article Type: Research Article

Abstract: From an empirical point of view, the hardness of quantified Boolean formulas (QBFs), can be characterized by the (in)ability of current state-of-the-art QBF solvers to decide about the truth of formulas given limited computational resources. In this paper, we start from the problem of computing empirical hardness markers, i.e., features that can discriminate between hard and easy QBFs, and we end up showing that such markers can be useful to improve our understanding of QBF preprocessors. In particular, considering the connection between classes of tractable QBFs and the treewidth of associated graphs, we show that (an approximation of) treewidth is …indeed a marker of empirical hardness and it is the only parameter which succeeds consistently in being so, even considering several other purely syntactic candidates which have been successfully employed to characterize QBFs in other contexts. We also show that treewidth approximations can be useful to describe the effect of QBF preprocessors, in that some QBF solvers benefit from a preprocessing phase when it reduces the treewidth of their input. Our experiments suggest that structural simplifications reducing treewidth are a potential enabler for the solution of hard QBF encodings. Show more

Keywords: Automated Reasoning, Structural Decompositions, QBF preprocessing

DOI: 10.3233/FI-2010-312

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 391-427, 2010

Authors: Riguzzi, Fabrizio

Article Type: Research Article

Abstract: Logic Programs with Annotated Disjunctions (LPADs) allow to express probabilistic information in logic programming. The semantics of an LPAD is given in terms of the well-founded models of the normal logic programs obtained by selecting one disjunct from each ground LPAD clause. Inference on LPADs can be performed using either the system Ailog2, that was developed for the Independent Choice Logic, or SLDNFAD, an algorithm based on SLDNF. However, both of these algorithms run the risk of going into infinite loops and of performing redundant computations. In order to avoid these problems, we present SLGAD resolution that computes …the (conditional) probability of a ground query from a range-restricted LPAD and is based on SLG resolution for normal logic programs. As SLG, it uses tabling to avoid some infinite loops and to avoid redundant computations. The performances of SLGAD are evaluated on classical benchmarks for normal logic programs under the well-founded semantics, namely a 2-person game and the ancestor relation, and on games of dice. SLGAD is compared with Ailog2 and SLDNFAD on the problems in which they do not go into infinite loops, namely those that are described by a modularly acyclic program. The results show that SLGAD is sometimes slower than Ailog2 and SLDNFAD but, if the program requires the repeated computations of the same goals, as for the dice games, then SLGAD is faster than both. Show more

Keywords: Probabilistic Logic Programming, Well-Founded Semantics, Logic Programs with Annotated Disjunctions, SLG Resolution

DOI: 10.3233/FI-2010-313

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 429-466, 2010

Authors: Soh, Takehide | Inoue, Katsumi | Tamura, Naoyuki | Banbara, Mutsunori | Nabeshima, Hidetomo

Article Type: Research Article

Abstract: We propose a satisfiability testing (SAT) based exact approach for solving the two-dimensional strip packing problem (2SPP). In this problem, we are given a set of rectangles and one large rectangle called a strip. The goal of the problem is to pack all rectangles without overlapping, into the strip by minimizing the overall height of the packing. Although the 2SPP has been studied in Operations Research, some instances are still hard to solve. Our method solves the 2SPP by translating it into a SAT problem through a SAT encoding called order encoding. The translated SAT problems tend to be large; …thus, we apply several techniques to reduce the search space by symmetry breaking and positional relations of rectangles. To solve a 2SPP, that is, to compute the minimum height of a 2SPP, we need to repeatedly solve similar SAT problems. We thus reuse learned clauses and assumptions from the previously solved SAT problems. To evaluate our approach, we obtained results for 38 instances from the literature and made comparisons with a constraint satisfaction solver and an ad-hoc 2SPP solver. Show more

Keywords: Boolean satisfiability, Strip packing problem, SAT encoding, Constraint satisfaction problem

DOI: 10.3233/FI-2010-314

Citation: Fundamenta Informaticae, vol. 102, no. 3-4, pp. 467-487, 2010