AI Communications - Volume 28, issue 2

Authors: Mancini, Toni | Oddi, Angelo

Article Type: Other

DOI: 10.3233/AIC-140655

Citation: AI Communications, vol. 28, no. 2, pp. 159-160, 2015

Authors: Janota, Mikoláš | Lynce, Inês | Marques-Silva, Joao

Article Type: Research Article

Abstract: The problem of propositional satisfiability (SAT) has found a number of applications in both theoretical and practical computer science. In many applications, however, knowing a formula's satisfiability alone is insufficient. Often, some other properties of the formula need to be computed. This article focuses on one such property: the backbone of a formula, which is the set of literals that are true in all the formula's models. Backbones find theoretical applications in characterization of SAT problems and they also find practical applications in product configuration or fault localization. This article overviews existing algorithms for backbone computation and introduces two novel …ones. Further, an extensive evaluation of the algorithms is presented. This evaluation demonstrates that one of the novel algorithms significantly outperforms the existing ones. Show more

Keywords: Backbones, SAT, necessary assignments, mandatory assignments

DOI: 10.3233/AIC-140640

Citation: AI Communications, vol. 28, no. 2, pp. 161-177, 2015

Authors: González, Miguel A. | Vela, Camino R. | Varela, Ramiro | González-Rodríguez, Inés

Article Type: Research Article

Abstract: In this paper we tackle the makespan minimization in the job shop scheduling problem with sequence-dependent non-anticipatory setup times. To this end, we design a scatter search algorithm which incorporates path relinking and tabu search in its core. The good performance of this algorithm relies on a new neighborhood structure proposed in this paper based on a graph model that incorporates the non-anticipatory characteristic of setup times. To define this structure, we consider all single moves, i.e., reversals of single arcs in the solution graph, and we give some conditions that establish the feasibility and the chance of improvement for …the neighbors. We present the results of an experimental study across usual benchmarks to analyze our algorithm and to compare it with the state-of-the-art. In particular, our approach establishes new best solutions for all the instances. Show more

Keywords: Job shop scheduling, neighborhood structures, scatter search, path relinking, tabu search, non-anticipatory setup times

DOI: 10.3233/AIC-140631

Citation: AI Communications, vol. 28, no. 2, pp. 179-193, 2015

Authors: Heras, Federico | Morgado, Antonio | Marques-Silva, Joao

Article Type: Research Article

Abstract: Weighted Partial MaxSAT (WPMS) is a well-known optimization variant of Boolean Satisfiability (SAT) that finds a wide range of practical applications. WPMS divides the formula in two sets of clauses: The hard clauses that must be satisfied and the soft clauses that can be falsified with a penalty given by their associated weight. However, some applications may require each original constraint to be modeled as a set or group of clauses. Then, the cost or penalty of falsifying one or several clauses of the same group is exactly the same. The resulting formalism is referred to as Group MaxSAT. This …paper overviews Group MaxSAT, and shows how several optimization problems can be modeled as Group MaxSAT. Several encodings from Group MaxSAT to standard MaxSAT are formalized and refined. A comprehensive empirical study compares the performance of several MaxSAT solvers with the proposed encodings. The results indicate that, depending on the underlying MaxSAT solver and problem domain, the solver may perform better with a given encoding than with the others. Show more

Keywords: Group MaxSAT, MaxSAT, Boolean optimization

DOI: 10.3233/AIC-140636

Citation: AI Communications, vol. 28, no. 2, pp. 195-214, 2015

Authors: Cattafi, Massimiliano | Herrero, Rosa | Gavanelli, Marco | Nonato, Maddalena | Malucelli, Federico

Article Type: Research Article

Abstract: Although sometimes it is necessary, no one likes to stay in a hospital, and patients who need to stay in bed but do not require constant medical surveillance prefer their own bed at home. At the same time, a patient in a hospital has a high cost for the community, that is not acceptable if the patient needs service only a few minutes a day. For these reasons, the current trend in Europe and North-America is to send nurses to visit patients at their home: this choice reduces costs for the community and gives better quality of life to patients. …The challenge is to deliver the service in a cost effective manner without a detriment of the service quality. These social and health management issues have interesting implications from the mathematical viewpoint, introducing a challenging combinatorial optimization problem. The problem consists in assigning patients' services to traveling nurses and defining the nurse itineraries so that the following optimization aspects are considered: the nurse workloads (including service as well as travel time) are balanced, patients are preferentially served by a single nurse or just a few ones, and the overall travel time is minimized. These objectives are somehow conflicting and a reasonable trade off must be found. The complexity of the problem calls for suitable optimization-based algorithmic support to decisions, in particular in the perspective of an increasing diffusion of the service. This problem is known in the literature as the Home Health Care (HHC) problem. In this paper, we address the HHC problem in the municipality of Ferrara, a mid-sized city in the North of Italy. The problem is currently solved by hand, starting from a partitioning of patients based on predefined zones. We describe a Constraint Programming model that solves the HHC problem, and show significant improvements with respect to the current manual solution. Show more

Keywords: Constraint programming, nurse scheduling applications, home health care, large neighbourhood search, routing problems, Lagrangian relaxation

DOI: 10.3233/AIC-140632

Citation: AI Communications, vol. 28, no. 2, pp. 215-237, 2015

Authors: Palacios, Juan José | González-Rodríguez, Inés | Vela, Camino R. | Puente, Jorge

Article Type: Research Article

Abstract: In the sequel, we consider a multiobjective open shop scheduling problem with uncertain durations modelled as fuzzy numbers. Given crisp due dates, the objective is to minimise both the makespan and the maximum tardiness. We formulate the multiobjective problem as a fuzzy goal programming model based on lexicographical minimisation of expected values. The resulting problem is solved using a particle swarm optimisation approach searching in the space of possibly active schedules. To asses the performance of this algorithm, we present results of an extensive experimental study on several problem instances, including: a parametric analysis, the experimental evaluation of different priority …structures compared to single-objective approaches in terms of objective values as well target achievement, an experimental analysis of the relationship between lexicographical and Pareto solutions and an empirical study based on a-posteriori semantics showing the advantages of taking into account the uncertainty along the scheduling process. Show more

Keywords: Open shop scheduling, fuzzy processing times, particle swarm optimisation, lexicographic goal programming

DOI: 10.3233/AIC-140637

Citation: AI Communications, vol. 28, no. 2, pp. 239-257, 2015

Authors: Gavanelli, Marco | Nonato, Maddalena | Peano, Andrea | Alvisi, Stefano | Franchini, Marco

Article Type: Research Article

Abstract: This paper heuristically tackles a challenging scheduling problem arising in the field of hydraulic distribution systems in case of a contamination event, that is, optimizing the scheduling of a set of tasks so that the consumed volume of contaminated water is minimized. Each task consists of manually activating a given device, located on the hydraulic network of the water distribution system. In practice, once contamination has been detected, a given number of response teams move along the network to operate each device on site. The consumed volume of contaminated water depends on the time at which each device is operated, …according to complex hydraulic laws, so that the value associated to each schedule must be evaluated by a hydraulic simulation. We explore the potentials of Genetic Algorithms as a viable tool for tackling this optimization-simulation problem. We compare different encodings and propose ad hoc crossover operators that exploit the combinatorial structure of the feasible region, featuring hybridization with Mixed Integer Linear Programming. Extensive computational results are provided for a real life hydraulic network of average size, showing the effectiveness of the approach. Indeed, we greatly improve upon common sense inspired solutions which are commonly adopted in practice. Show more

Keywords: Hybrid genetic algorithms, simulation-optimization, scheduling

DOI: 10.3233/AIC-140638

Citation: AI Communications, vol. 28, no. 2, pp. 259-282, 2015

Authors: Miller, Christian | Marin, Paolo | Becker, Bernd

Article Type: Research Article

Abstract: SAT solving is an indispensable core component of numerous formal verification tools and has found widespread use in industry, in particular when using it in an incremental fashion, e.g., in Bounded Model Checking (BMC). On the other hand, for some applications SAT formulas are not expressive enough, whereas a description via Quantified Boolean Formulas (QBF) is much more adequate, for instance when dealing with partial designs. Motivated by the success of incremental SAT, in this paper we explore various approaches to solve QBF problems in an incremental fashion and thereby make this technology usable as a core component of …BMC. Firstly, we realized an incremental QBF solver based on the state-of-the-art QBF solver QuBE: Taking profit from the reuse of some information from previous iterations, the search space can be pruned, in some cases, to even less than a quarter. However, the need for preprocessing QBF formulas prior to the solving phase, that in general cannot be paired with incremental solving because of the non-predictable elimination of variables in the future incremental steps, posed the question of incremental QBF preprocessing. In this context we present an approach for retaining the QBF formula being preprocessed while extending its clauses and prefix incrementally. This procedure results in a significant size reduction of the QBF formulas, hence leading to a reduced solving time. As this may come together with a high preprocessing time, we analyze various heuristics to dynamically disable incremental preprocessing when its overhead raises over a certain threshold and is not compensated by the reduced solving time anymore. For proving the efficacy of our methods experimentally, as an application we consider BMC for partial designs (i.e., designs containing so-called blackboxes which represent unknown parts). Here, we disprove realizability, that is, we prove that an unsafe state is reachable no matter how the blackboxes are implemented. We examine all these incremental approaches from both the point of view of the effectiveness of the single procedure and the benefits that a range of QBF solvers can take from it. On a domain of partial design benchmarks, engaging incremental QBF methods significant performance gains over non incremental BMC can be achieved. Show more

Keywords: Incremental QBF, BMC, partial design verification, blackbox

DOI: 10.3233/AIC-140633

Citation: AI Communications, vol. 28, no. 2, pp. 283-307, 2015

Authors: Badaloni, Silvana | Sambo, Francesco | Venco, Francesco

Article Type: Research Article

Abstract: Bayesian Networks (BN) are probabilistic graphical models used to encode in a compact way a joint probability distribution over a set of random variables. The NP-complete problem of finding the most probable BN structure given the observed data has been largely studied in recent years. In the literature, several complete algorithms have been proposed for the problem; in parallel, several tests for statistical independence between the random variables have been proposed, in order to reduce the size of the search space. In this work, we study how to hybridize the algorithm representing the state-of-the-art in complete search with two types …of independence tests, and assess the performance of the two hybrid algorithms in terms of both solution quality and computational time. Experimental results show that hybridization with both types of independence test results in a substantial gain in computational time, against a limited loss in solution quality, and allow us to provide some guidelines on the choice of the test type, given the number of nodes in the network and the sample size. Show more

Keywords: Bayesian networks, structure learning, hybrid algorithms

DOI: 10.3233/AIC-140634

Citation: AI Communications, vol. 28, no. 2, pp. 309-322, 2015

Authors: Gerevini, Alfonso Emilio | Saetti, Alessandro | Vallati, Mauro

Article Type: Research Article

Abstract: The use of automatically learned knowledge for a planning domain can significantly improve the performance of a generic planner when solving a problem in this domain. In this work, we focus on the well-known SAT-based approach to planning and investigate two types of learned knowledge: macro-actions and planning horizon. Macro-actions are sequences of actions that typically occur in the solution plans, while a planning horizon of a problem is the length of a (possibly optimal) plan solving it. We propose a method that uses a machine learning tool for building a predictive model of the optimal planning horizon, and variants …of the well-known planner SatPlan and solver MiniSat that can exploit macro actions and learned planning horizons to improve their performance. An experimental analysis illustrates the effectiveness of the proposed techniques demonstrating that significant speedups can be obtained. Show more

Keywords: Planning as satisfiability, machine learning for planning

DOI: 10.3233/AIC-140641

Citation: AI Communications, vol. 28, no. 2, pp. 323-344, 2015