Fundamenta Informaticae - Volume 107, issue 2-3

Authors: Gavanelli, Marco | Mancini, Toni | Pettorossi, Alberto

Article Type: Other

DOI: 10.3233/FI-2011-396

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. i-ii, 2011

Authors: Cesta, Amedeo | Fratini, Simone | Orlandini, Andrea | Finzi, Alberto | Tronci, Enrico

Article Type: Research Article

Abstract: Timeline-based planning techniques have demonstrated wide application possibilities in heterogeneous real world domains. For a wider diffusion of this technology, a more thorough investigation of the connections with formal methods is needed. This paper is part of a research program aimed at studying the interconnections between timeline-based planning and standard techniques for formal validation and verification (V&V). In this line, an open issue consists of studying the link between plan generation and plan execution from the particular perspective of verifying temporal plans before their actual execution. The present work addresses the problem of verifying flexible temporal plans, i.e., those plans …usually produced by least-commitment temporal planners. Such plans only impose minimal temporal constraints among the planned activities, hence are able to adapt to on-line environmental changes by trading some of the retained flexibility. This work shows how a model-checking verification tool based on Timed Game Automata (TGA) can be used to verify such plans. In particular, flexible plan verification is cast as a model-checking problem on those automata. The effectiveness of the proposed approach is shown by presenting a detailed experimental analysis with a real world domain which is used as a flexible benchmark. Show more

Keywords: Timeline-based Planning, Validation and Verification, Model Checking

DOI: 10.3233/FI-2011-397

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 111-137, 2011

Authors: Lewis, Matthew | Schubert, Tobias | Becker, Bernd | Marin, Paolo | Narizzano, Massimo | Giunchiglia, Enrico

Article Type: Research Article

Abstract: In this paper we present the parallel QBF Solver PaQuBE. This new solver leverages the additional computational power that can be exploited from modern computer architectures, from pervasive multi-core boxes to clusters and grids, to solve more relevant instances faster than previous generation solvers. Furthermore, PaQuBE's progressive MPI based parallel framework is the first to support advanced knowledge sharing in which solution cubes as well as conflict clauses can be exchanged between solvers. Knowledge sharing plays a critical role in the performance of PaQuBE. However, due to the overhead associated with sending and receiving MPI messages, and the restricted communication/network …bandwidth available between solvers, it is essential to optimize not only what information is shared, but the way in which it is shared. In this context, we compare multiple conflict clause and solution cube sharing strategies, and finally show that an adaptive method provides the best overall results. Show more

Keywords: QBF, Parallel Solving, Knowledge Sharing, MPI

DOI: 10.3233/FI-2011-398

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 139-166, 2011

Authors: Gerevini, Alfonso | Saetti, Alessandro | Serina, Ivan

Article Type: Research Article

Abstract: Planning through local search and action graphs is a powerful approach to fully-automated planning which is implemented in the well-known LPG planner. The approach is based on a stochastic local search procedure exploring a space of partial plans and several heuristic features with different possible options. In this paper, we experimentally analyze the most important of them, with the goal of understanding and evaluating their impact on the performance of LPG, and of identifying default settings that work well on a large class of problems. In particular, we analyze several heuristic techniques for (a) evaluating the search neighborhood, (b) defining/restricting …the search neighborhood, (c) selecting the next plan flaw to handle, (d) setting the “noise” parameter randomizing the search, and (e) computing reachability information that can be exploited by the heuristic functions used to evaluate the neighborhood elements. Some of these techniques were introduced in previous work on LPG, while others are new. Additional experimental results indicate that the current version of LPG using the identified best heuristic techniques as the default settings is competitive with the winner of the last (2008) International Planning Competition. Show more

Keywords: Automated planning, domain-independent planning, efficient planning, experimental evaluation of planning techniques

DOI: 10.3233/FI-2011-399

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 167-197, 2011

Authors: Zanzotto, Fabio Massimo | Dell'Arciprete, Lorenzo | Moschitti, Alessandro

Article Type: Research Article

Abstract: One of the most important research area in Natural Language Processing concerns the modeling of semantics expressed in text. Since foundational work in Natural Language Understanding has shown that a deep semantic approach is still not feasible, current research is focused on shallow methods combining linguistic models and machine learning techniques. The latter aim at learning semantic models, like those that can detect the entailment between the meaning of two text fragments, by means of training examples described by specific features. These are rather difficult to design since there is no linguistic model that can effectively encode the lexico-syntactic level …of a sentence and its corresponding semantic models. Thus, the adopted solution consists in exhaustively describing training examples by means of all possible combinations of sentence words and syntactic information. The latter, typically expressed as parse trees of text fragments, is often encoded in the learning process using graph algorithms. In this paper, we propose a class of graphs, the tripartite directed acyclic graphs (tDAGs), which can be efficiently used to design algorithms for graph kernels for semantic natural language tasks involving sentence pairs. These model the matching between two pairs of syntactic trees in terms of all possible graph fragments. Interestingly, since tDAGs encode the association between identical or similar words (i.e. variables), it can be used to represent and learn first-order rules, i.e. rules describable by first-order logic. We prove that our matching function is a valid kernel and we empirically show that, although its evaluation is still exponential in the worst case, it is extremely efficient and more accurate than the previously proposed kernels. Show more

DOI: 10.3233/FI-2011-400

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 199-222, 2011

Authors: He, Jun | Flener, Pierre | Pearson, Justin

Article Type: Research Article

Abstract: We explore the idea of using automata to implement new constraints for local search. This is already a successful approach in constraint-based global search. We show how to maintain the violations of a constraint and its variables via a deterministic finite automaton that describes a ground checker for that constraint. We extend the approach to counter automata, which are often much more convenient than finite automata, if not more independent of the constraint instance. We establish the practicality of our approach on several real-life combinatorial problems.

Keywords: Automaton constraint, Counter automaton, Local search

DOI: 10.3233/FI-2011-401

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 223-248, 2011

Authors: Lynce, Inês | Marques-Silva, Joao

Article Type: Research Article

Abstract: The extraction of a Minimal Unsatisfiable Core (MUC) in a Constraint Satisfaction Problem (CSP) aims to identify a subset of constraints that make a CSP instance unsatisfiable. Recent work has addressed the identification of a Minimal Set of Unsatisfiable Tuples (MUST) in order to restore the CSP satisfiability with respect to that MUC. A two-step algorithm has been proposed: first, a MUC is identified, and second, a MUST in the MUC is identified. This paper proposes an integrated algorithm for restoring satisfiability in a CSP, making use of a MaxSAT solver. The proposed approach encodes the CSP instance as a …partial MaxSAT instance, in such a way that solving the MaxSAT instance corresponds to identifying the smallest set of tuples to be removed from the CSP instance to restore satisfiability. Experimental results illustrate the feasibility of the approach. Show more

Keywords: constraint satisfaction problems, minimal unsatisfiable cores, minimal set of unsatisfiable tuples, maximum satisfiability

DOI: 10.3233/FI-2011-402

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 249-266, 2011

Authors: Lombardi, Michele | Milano, Michela | Roli, Andrea | Zanarini, Alessandro

Article Type: Research Article

Abstract: We investigate the impact of information extracted from sampling and diving on the solution of Constraint Satisfaction Problems (CSP). A sample is a complete assignment of variables to values taken from their domain according to a given distribution. Diving consists in repeatedly performing depth first search attempts with random variable and value selection, constraint propagation enabled and backtracking disabled; each attempt is called a dive and, unless a feasible solution is found, it is a partial assignment of variables (whereas a sample is a –possibly infeasible– complete assignment). While the probability of finding a feasible solution via sampling or diving …is negligible if the problem is difficult enough, samples and dives are very fast to generate and, intuitively, even when they are infeasible, they can provide some statistical information on search space structure. The aim of this paper is to understand to what extent it is possible to support the CSP solving process with information derived from sampling and diving. In particular, we are interested in extracting from samples and dives precise indications on the quality of individual variable-value assignments with respect to feasibility. We formally prove that even uniform sampling could provide precise evaluation of the quality of single variable-value assignments; as expected, this requires huge sample sizes and is therefore not useful in practice. On the contrary, diving is much better suited for assignment evaluation purposes. We undertake a thorough experimental analysis on a collection of Partial Latin Square and Car Sequencing instances to assess the quality of information provided by dives. Dive features are identified and their impact on search is evaluated. Results show that diving provides information that can be fruitfully exploited. Show more

Keywords: Constraint Satisfaction Problem, Sampling, Diving, Solution Counting, Heuristics Evaluation

DOI: 10.3233/FI-2011-403

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 267-287, 2011

Authors: Hyvärinen, Antti E.J. | Junttila, Tommi | Niemelä, Ilkka

Article Type: Research Article

Abstract: This paper studies the following question: given an instance of the propositional satisfiability problem, a randomized satisfiability solver, and a cluster of n computers, what is the best way to use the computers to solve the instance? Two approaches, simple distribution and search space partitioning as well as their combinations are investigated both analytically and empirically. It is shown that the results depend heavily on the type of the problem (unsatisfiable, satisfiable with few solutions, and satisfiable with many solutions) as well as on how good the search space partitioning function is. In addition, the behavior of a real search …space partitioning function is evaluated in the same framework. The results suggest that in practice one should combine the simple distribution and search space partitioning approaches. Show more

Keywords: SAT solving, Randomized search, Distributed constraint-based search

DOI: 10.3233/FI-2011-404

Citation: Fundamenta Informaticae, vol. 107, no. 2-3, pp. 289-311, 2011