Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model-theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver yices, to the translation-based ASP solver lp2diff and to clingo on domains from the “Basic Decision” track of the 2017 Answer Set Programming competition. The results show that our approach is competitive to and often better than lp2diff, and that it can also be faster than clingo on non-tight domains.

Abstract The Nuclear Medicine Scheduling (NMS) problem consists of assigning patients to a day, on which the patient will undergo the medical check, the preparation and the actual image detection process. The schedule should consider the different requirements of the patients and the available resources, e.g. varying time required for different diseases and radiopharmaceuticals used, number of injection chairs and tomographs available. In this paper, we present two solutions to the NMS problem based on Answer Set Programming (ASP). The first solution is a direct ASP encoding, which is then processed by an ASP solver, while the second solution employs a Logic-based Bender Decomposition (LBBD) approach implemented through the usage of multi-shot solving. Experiments employing real data show that the direct encoding provides overall satisfying results in terms of solutions quality in a relatively short time, and that the LBBD approach also helps in improving scalability.

Stable models of logic programs have been studied and characterized in relation with other formalisms by many researchers. As already argued in previous papers, such characterizations are interesting for diverse reasons, including theoretical investigations and the possibility of leading to new algorithms for computing stable models of logic programs. At the theoretical level, complexity and expressiveness comparisons have brought about fundamental insights. Beyond that, practical implementations of the developed reductions enable the use of existing solvers for other logical formalisms to compute stable models. In this paper, we first provide a simple characterization of stable models that can be viewed as a proof-theoretic counterpart of the standard model-theoretic definition. We further show how it can be naturally encoded in difference logic. Such an encoding, compared to the existing reductions to classical logics, does not require Boolean variables. Then, we implement our novel translation to a Satisfiability Modulo Theories (SMT) formula. We finally compare our approach, employing the SMT solver yices , to the translation-based ASP solver lp2diff and to clingo on domains from the “Basic Decision” track of the 2017 Answer Set Programming competition. The results show that our approach is competitive to and often better than lp2diff , and that it can also be faster than clingo on non-tight domains.

Abstract The operating room scheduling (ORS) problem deals with the optimization of daily operating room surgery schedules. It is a challenging problem subject to many constraints, like to determine the starting time of different surgeries and allocating the required resources, including the availability of beds in different department units. Recently, solutions to this problem based on answer set programming (ASP) have been delivered. Such solutions are overall satisfying but, when applied to real data, they can currently only verify whether the encoding aligns with the actual data and, at most, suggest alternative schedules that could have been computed. As a consequence, it is not currently possible to generate provisional schedules. Furthermore, the resulting schedules are not always robust. In this paper, we integrate inductive and deductive techniques for solving these issues. We first employ machine learning algorithms to predict the surgery duration, from historical data, to compute provisional schedules. Then, we consider the confidence of such predictions as an additional input to our problem and update the encoding correspondingly in order to compute more robust schedules. Results on historical data from the ASL1 Liguria in Italy confirm the viability of our integration.

Abstract The problem of scheduling pre-operative assessment clinic (PAC) consists of assigning patients to a day for the exams needed before a surgical procedure, taking into account patients with different priority levels, due dates and operators availability. Realizing a satisfying schedule is of upmost importance for a hospital, since delay in PAC can cause delay in the subsequent phases, thus lowering patients’ satisfaction. In this paper, we propose a two-phase solution to the PAC problem: in the first phase, patients are assigned to a day taking into account a default list of exams; then, in the second phase, having the actual list of exams needed by each patient, we use the results of the first phase to assign a starting time to each exam. We first present a mathematical formulation for both problems. Further, we present a solution where modeling and solving are done via answer set programming. We then introduce a rescheduling solution that may come into play when the scheduling solution cannot be applied fully. Experiments employing synthetic benchmarks on both scheduling and rescheduling show that both solutions provide satisfying results in short time. We finally show the implementation and usage of a web application that allows to run our scheduling solution and analyze the results graphically in a transparent way.

Abstract The Operating Room Scheduling (ORS) problem deals with the optimization of daily operating room surgery schedules. It is a challenging problem subject to many constraints, like to determine the starting time of different surgeries and allocating the required resources, including the availability of beds in different units. In the past years, Answer Set Programming (ASP) has been successfully employed for addressing and solving the ORS problem. Despite its importance, due to the inherent difficulty of retrieving real data, all the analyses on ORS ASP encodings have been performed on synthetic data so far. In this paper, first we present a new, improved ASP encoding for the ORS problem. Then, we deal with the real case of ASL1 Liguria, an Italian health authority operating through three hospitals, and present adaptations of the ASP encodings to deal with the real-world data. Further, we analyse the resulting encodings on hospital scheduling data by ASL1 Liguria. Results on some scenarios show that the ASP solutions produce satisfying schedules also when applied to such challenging, real data.1

Abstract Answer set programming (ASP) is a popular declarative programming language for solving hard combinatorial problems. Although ASP has gained widespread acceptance in academic and industrial contexts, there are certain user groups who may find it more advantageous to employ a higher-level language that closely resembles natural language when specifying ASP programs. In this paper, we propose a novel tool, called CNL2ASP, for translating English sentences expressed in a controlled natural language (CNL) form into ASP. In particular, we first provide a definition of the type of sentences allowed by our CNL and their translation as ASP rules and then exemplify the usage of the CNL for the specification of both synthetic and real-world combinatorial problems. Finally, we report the results of an experimental analysis conducted on the real-world problems to compare the performance of automatically generated encodings with the ones written by ASP practitioners, showing that our tool can obtain satisfactory performance on these benchmarks.

Abstract The problem of finding a Master Surgical Schedule (MSS) consists of scheduling different specialties to the operating rooms (ORs) of a hospital clinic. To produce a proper MSS, each specialty must be assigned to some ORs, where the number of assignments is different for each specialty and can also vary during the considered planning horizon. The problem is enriched by considering resource availability such as beds, surgical teams and nurses. Realizing a satisfying schedule is of upmost importance for a hospital clinic, since a poorly scheduled MSS may lead to unbalanced specialties availability and increase patients’ waiting list, thus negatively affecting both the administrative costs of the hospital and the patient satisfaction. In this paper, we present compact solutions based on Answer Set Programming (ASP) to the MSS problem. We tested our solutions on different scenarios: experiments show that our ASP solutions provide satisfying results in short time, also when compared to other logic-based formalisms. Finally, we describe a web application we have developed for easy usage of our solution.

Abstract The problem of scheduling chemotherapy treatments in oncology clinics is a complex problem, given that the solution has to satisfy (as much as possible) several requirements such as the cyclic nature of chemotherapy treatment plans, maintaining a constant number of patients, and the availability of resources, for example, treatment time, nurses, and drugs. At the same time, realizing a satisfying schedule is of upmost importance for obtaining the best health outcomes. In this paper we first consider a specific instance of the problem which is employed in the San Martino Hospital in Genova, Italy, and present a solution to the problem based on Answer Set Programming (ASP). Then, we enrich the problem and the related ASP encoding considering further features often employed in other hospitals, desirable also in S. Martino, and/or considered in related papers. Results of an experimental analysis, conducted on the real data provided by the San Martino Hospital, show that ASP is an effective solving methodology also for this important scheduling problem.