Search

The Disjunctive Temporal Problem (DTP) involves conjunction of DTP constraints, each DTP constraint being a disjunction of difference constraints of the form x-y≤c, where x and y range over a domain of interpretation, and c is a numeric constant. The DTP is recognized to be an expressive framework for constraints modeling and processing. The addition of preferences, in the form of weights associated to difference constraints for their satisfaction, needs methods for aggregating preferences among and within DTP constraints to compute meaningful and high quality solutions, while further enhancing DTP expressivity and applicability. In this paper we consider an utilitarian aggregation of DTP constraints weights, and a prominent semantic for aggregating such weights from its difference constraints weights that considers the maximum among the weights associated to satisfied difference constraints in it. We present a novel approach that reduces the problem to Maximum Satisfiability of DTPs (Max-DTPs). In this way, we can employ off-the-shelf Max-DTP solvers with different solution methods, ranging from Satisfiability Modulo Theories (SMT), to interval-based and Boolean optimization-based solvers. We then compare the performance of our approach with different back-end solvers on both randomly generated and real-world benchmarks, in comparison with MAXILITIS, the best solver that can deal with DTPs with preferences using the aggregation methods considered. Results show that the YICES SMT solver is the best, and that YICES and the TSAT# solver based on Boolean optimization can be orders of magnitude faster than MAXILITIS. [ABSTRACT FROM AUTHOR]

A novel optimization paradigm, called Community of Scientists Optimization (CoSO), is presented in this paper. The approach is inspired to the behaviour of a community of scientists interacting, pursuing for research results and foraging the funds needed to held their research activities. The CoSO metaphor can be applied to general optimization domains, where optimal solutions emerge from the collective behaviour of a distributed community of interacting autonomous entities. The CoSO framework presents analogies and remarkable differences with other evolutionary optimization approaches: swarm behaviour, foraging and selection mechanism based on research funds competition, dynamically evolving multicapacity communication channels realized by journals and evolving population size regulated by research management strategies. Experiments and comparisons on benchmark problems show the effectiveness of the approach for numerical optimization. CoSO, with the design of appropriate foraging and competition strategies, also represents a great potential as a general meta-heuristic for applications in non-numerical and agent-based domains. [ABSTRACT FROM AUTHOR]

The predominance of multicore processors has increased the interest in developing parallel Boolean Satisfiability (SAT) solvers. As a result, more parallel SAT solvers are emerging. Even though parallel approaches are known to boost performance, parallel approaches developed for Boolean optimization are scarce. This paper proposes parallel search algorithms for Maximum Satisfiability (MaxSAT) and introduces PWBO, a new parallel solver for partial MaxSAT. Using two threads, an unsatisfiability-based algorithm is used to search on the lower bound of the optimal solution, while at the same time a linear search is performed on the upper bound of the optimal solution. Moreover, learned clauses are shared between threads during the search. For a larger number of threads two different strategies are proposed. The first strategy performs a portfolio approach by searching on the lower and upper bound values of the optimal solution using different encodings of cardinality constraints for each thread. The second strategy splits the search space considering different upper bound values of the optimal solution for each thread. Experimental results show that the techniques proposed in the paper enable PWBO to improve when increasing the number of threads. [ABSTRACT FROM AUTHOR]

The Capacitated Arc Routing Problem (CARP) is a combinatorial optimization problem similar to the well-known Capacitated Vehicle Routing Problem (CVRP). In the CARP, the customers' demands are located on the edges (arcs) of a general (not necessarily complete) graph. This is in contrast to the CVRP, where demand is located on the nodes of a complete graph. While the CVRP has been extensively studied over the past couple of decades, the number of articles and research results on the CARP is significantly lower. To partially fill this gap in the literature, a new heuristic and two new algorithms for the CARP are proposed and evaluated. Our Savings-based Heuristic for the ARP (SHARP) is inspired on the popular Clarke and Wright savings heuristic for the CVRP. The SHARP procedure outperforms the classical Path Scanning heuristic (PSH) and thus it can be integrated into most meta-heuristics to provide a 'good' and fast initial solution to medium-to-large size ARPs which cannot be solved using exact approaches. Using both SHARP and PSH as a base, two randomized algorithms are developed in this paper. These are multi-start algorithms which introduce a biased randomization process to each heuristic. This randomization process uses biased probability distributions, such as the geometric one, in order to induce some degree of randomness in the solution-construction stage while keeping most of the heuristic 'common sense'. In order to state their efficiency, both randomized algorithms are compared and evaluated using a standard set of benchmarks. The results show that our randomized version of SHARP, RandSHARP, is quite competitive and far superior to the PSH-based randomized algorithm. [ABSTRACT FROM AUTHOR]

In recent years, Satisfiability Modulo Theory (SMT) solvers are becoming increasingly popular in the Computer Aided Verification and Reasoning community. Used natively or as back-engines, they are accumulating a record of success stories and, as witnessed by the annual SMT competition, their performances and capacity are also increasing steadily. Introduced in previous contributions of ours, a new application domain providing an outstanding challenge for SMT solvers is represented by verification of Multi-Layer Perceptrons (MLPs) a widely-adopted kind of artificial neural network. In this paper we present an extensive evaluation of the current state-of-the-art SMT solvers and assess their potential in the promising domain of MLP verification. [ABSTRACT FROM AUTHOR]

Conflict-driven constraint learning provides big gains on many CSP and SAT problems. However, time and space costs to propagate the learned constraints can grow very quickly, so constraints are often discarded (forgotten) to reduce overhead. We conduct a major empirical investigation into the overheads introduced by unbounded constraint learning in CSP. To the best of our knowledge, this is the first published study in either CSP or SAT. We obtain three significant results. The first is that a small percentage of learnt constraints do most propagation. While this is conventional wisdom, it has not previously been the subject of empirical study. Second, we show that even constraints that do no effective propagation can incur significant time overheads. Finally, by implementing forgetting, we confirm that it can significantly improve the performance of modern learning CSP solvers, contradicting some previous research. [ABSTRACT FROM AUTHOR]

Minimally Unsatisfiable Subformulas (MUS) find a wide range of practical applications, including product configuration, knowledge-based validation, and hardware and software design and verification. MUSes also find application in recent Maximum Satisfiability algorithms and in CNF formula redundancy removal. Besides direct applications in Propositional Logic, algorithms for MUS extraction have been applied to more expressive logics. This paper proposes two algorithms for computation of MUSes of propositional formulas in Conjunctive Normal Form (CNF). The first algorithm is optimal in its class, meaning that it requires the smallest number of calls to a SAT solver. The second algorithm extends earlier work, but implements a number of new techniques. Among these, this paper analyzes in detail the technique of recursive model rotation, which provides significant performance gains in practice. Experimental results, obtained on representative practical benchmarks, indicate that the new algorithms achieve significant performance gains with respect to state of the art MUS extraction algorithms. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

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. [ABSTRACT FROM AUTHOR]

The SARS-CoV-2 pandemic reminded us how vaccination can be a divisive topic on which the public conversation is permeated by misleading claims, and thoughts tend to polarize, especially on online social networks. In this work, motivated by recent natural language processing techniques to systematically extract and quantify opinions from text messages, we present a differential framework for bivariate opinion formation dynamics that is coupled with a compartmental model for fake news dissemination. Thanks to a mean-field analysis we demonstrate that the resulting Fokker-Planck system permits to reproduce bimodal distributions of opinions as observed in polarization dynamics. The model is then applied to sentiment analysis data from social media platforms in Italy, in order to analyze the evolution of opinions about Covid-19 vaccination. We show through numerical simulations that the model is capable to describe correctly the formation of the bimodal opinion structure observed in the vaccine-hesitant dataset, which is witness of the known polarization effects that happen within closed online communities. [ABSTRACT FROM AUTHOR]

Every year about one third of the food production intended for humans gets lost or wasted. This wastefulness of resources leads to the emission of unnecessary greenhouse gas, contributing to global warming and climate change. The solution proposed by the SORT project is to "recycle" the surplus of food by reconditioning it into animal feed or fuel for biogas/biomass power plants. In order to maximize the earnings and minimize the costs, several choices must be made during the reconditioning process. Given the extremely complex nature of the process, Decision Support Systems (DSSs) could be helpful to reduce the human effort in decision making. In this paper, we present a DSS for food recycling developed using two approaches for finding the optimal solution: one based on Binary Linear Programming (BLP) and the other based on Answer Set Programming (ASP), which outperform our previous approach based on Constraint Logic Programming (CLP) on Finite Domains (CLP(FD)). In particular, the BLP and the CLP(FD) approaches are developed in ECL i PS e , a Prolog system that interfaces with various state-of-the-art Mathematical and Constraint Programming solvers. The ASP approach, instead, is developed in clingo. The three approaches are compared on several synthetic datasets that simulate the operative conditions of the DSS. • We propose a Decision Support System (DSS) for aiding the process of food recycling. • Three techniques are compared: Constraint Logic Programming, Binary Linear Programming and Answer Set Programming. • The method based on Binary Linear Programming scales better in this application. [ABSTRACT FROM AUTHOR]