Search

LIPIcs, Volume 210, CP 2021, Complete Volume, LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 1-1000

Front Matter, Table of Contents, Preface, Conference Organization, LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 0:i-0:xxii

Un problema importante de la ingeniería de software es la visualización de modelos, para facilitar su comprensión y evolución. Zoomable User Interfaces (ZUI) es un paradigma con potencial de mejorar la visualización de modelos, el cual utiliza el zoom como medio para navegar entre diferentes niveles de abstracción. Este artículo, primer paso de una investigación en dicha dirección, describe un prototipo de herramienta meta-case, llamado ZooMEnv, para la definición e instanciación de sintaxis concretas (notación) de lenguajes visuales de modelado. El énfasis de la herramienta es la utilización de un meta-modelo pequeño para representar la notación de manera genérica y, como elemento novedoso, la incorporación de ZUI a través de jerarquías de composición y zoom semántico. Cinco notaciones diferentes son desarrolladas como casos de estudio para probar las capacidades de la herramienta y definir futuras mejoras. Model visualization is an important problem in software engineering, to assist designers to understand and evolve models. Zoomable User Interfaces (ZUI), which uses zoom as the main mechanism to navigate between different levels of abstraction, has the potential to improve model visualization. This paper, the first step in this research direction, presents a prototype meta-case tool, called ZooMEnv, to define and utilize concrete syntaxes (notations) of visual modeling languages. The focus of the tool is to rely on a small meta-model to represent notation in a generic way and incorporate, as a novel concept, ZUI capabilities through composition hierarchies and semantic zooming. Five different notations are developed as case studies to explore the capabilities of this tool and determine future improvements.

We introduce a new Multi-Agent Path Finding (MAPF) problem which is motivated by an industrial application. Given a fleet of robots that move on a workspace that may contain static obstacles, we must find paths from their current positions to a set of destinations, and the goal is to minimise the length of the longest path. The originality of our problem comes from the fact that each robot is attached with a cable to an anchor point, and that robots are not able to cross these cables. We formally define the Non-Crossing MAPF (NC-MAPF) problem and show how to compute lower and upper bounds by solving well known assignment problems. We introduce a Variable Neighbourhood Search (VNS) approach for improving the upper bound, and a Constraint Programming (CP) model for solving the problem to optimality. We experimentally evaluate these approaches on randomly generated instances., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 45:1-45:16

Maximum satisfiability (MaxSAT) is a viable approach to solving NP-hard optimization problems. In the realm of core-guided MaxSAT solving - one of the most effective MaxSAT solving paradigms today - algorithmic variants employing so-called soft cardinality constraints have proven very effective. In this work, we propose to combine weight-aware core extraction (WCE) - a recently proposed approach that enables relaxing multiple cores instead of a single one during iterations of core-guided search - with a novel form of structure sharing in the cardinality-based core relaxation steps performed in core-guided MaxSAT solvers. In particular, the proposed form of structure sharing is enabled by WCE, which has so-far not been widely integrated to MaxSAT solvers, and allows for introducing fewer variables and clauses during the MaxSAT solving process. Our results show that the proposed techniques allow for avoiding potential overheads in the context of soft cardinality constraint based core-guided MaxSAT solving both in theory and in practice. In particular, the combination of WCE and structure sharing improves the runtime performance of a state-of-the-art core-guided MaxSAT solver implementing the central OLL algorithm., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 28:1-28:19

The paper introduces the Seesaw algorithm, which explores the Pareto frontier of two given functions. The algorithm is complete and generalizes the well-known implicit hitting set paradigm. The first given function determines a cost of a hitting set and is optimized by an exact solver. The second, called the oracle function, is treated as a black-box. This approach is particularly useful in the optimization of functions that are impossible to encode into an exact solver. We show the effectiveness of the algorithm in the context of static solver portfolio selection. The existing implicit hitting set paradigm is applied to cost function and an oracle predicate. Hence, the Seesaw algorithm generalizes this by enabling the oracle to be a function. The paper identifies two independent preconditions that guarantee the correctness of the algorithm. This opens a number of avenues for future research into the possible instantiations of the algorithm, depending on the cost and oracle functions used., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 31:1-31:16

Recent developments in applying and extending Boolean satisfiability (SAT) based techniques have resulted in new types of approaches to pseudo-Boolean optimization (PBO), complementary to the more classical integer programming techniques. In this paper, we develop the first approach to pseudo-Boolean optimization based on instantiating the so-called implicit hitting set (IHS) approach, motivated by the success of IHS implementations for maximum satisfiability (MaxSAT). In particular, we harness recent advances in native reasoning techniques for pseudo-Boolean constraints, which enable efficiently identifying inconsistent assignments over subsets of objective function variables (i.e. unsatisfiable cores in the context of PBO), as a basis for developing a native IHS approach to PBO, and study the impact of various search techniques applicable in the context of IHS for PBO. Through an extensive empirical evaluation, we show that the IHS approach to PBO can outperform other currently available PBO solvers, and also provides a complementary approach to PBO when compared to classical integer programming techniques., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 51:1-51:20

The enumeration of finite models of first order logic formulas is an indispensable tool in computational algebra. The task is hindered by the existence of isomorphic models, which are of no use to mathematicians and therefore are typically filtered out a posteriori. This paper proposes a divide-and-conquer approach to speed up and parallelize this process. We design a series of invariant properties that enable us to partition existing models into mutually non-isomorphic blocks, which are then tackled separately. The presented approach is integrated into the popular tool Mace4, where it shows tremendous speed-ups for a variety of algebraic structures., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 4:1-4:9

Explaining decisions is at the heart of explainable AI. We investigate the computational complexity of providing a formally-correct and minimal explanation of a decision taken by a classifier. In the case of threshold (i.e. score-based) classifiers, we show that a complexity dichotomy follows from the complexity dichotomy for languages of cost functions. In particular, submodular classifiers allow tractable explanation of positive decisions, but not negative decisions (assuming P≠NP). This is an example of the possible asymmetry between the complexity of explaining positive and negative decisions of a particular classifier. Nevertheless, there are large families of classifiers for which explaining both positive and negative decisions is tractable, such as monotone or linear classifiers. We extend tractable cases to constrained classifiers (when there are constraints on the possible input vectors) and to the search for contrastive rather than abductive explanations. Indeed, we show that tractable classes coincide for abductive and contrastive explanations in the constrained or unconstrained settings., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 21:1-21:18

In many application problems, including physical security and wildlife conservation, infrastructure must be configured to ensure or deny paths between specified locations. We model the problem as sub-graph design subject to constraints on paths and path lengths, and propose length-bound reachability constraints. Although reachability in graphs has been modelled before in constraint programming, the interaction of positive and negative reachability has not been studied in depth. We prove that deciding whether a set of positive and negative reachability constraints are satisfiable is NP complete. We show the effectiveness of our approach on decision problems, and also on optimisation problems. We compare our approach with existing constraint models, and we demonstrate significant improvements in runtime and solution costs, on a new problem set., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 46:1-46:16

The traditional Capacitated Vehicle Routing Problem (CVRP) minimizes the total distance of the routes under the capacity constraints of the vehicles. But more often, the objective involves multiple criteria including not only the total distance of the tour but also other factors such as travel costs, travel time, and fuel consumption. Moreover, in reality, there are numerous implicit preferences ingrained in the minds of the route planners and the drivers. Drivers, for instance, have familiarity with certain neighborhoods and knowledge of the state of roads, and often consider the best places for rest and lunch breaks. This knowledge is difficult to formulate and balance when operational routing decisions have to be made. This motivates us to learn the implicit preferences from past solutions and to incorporate these learned preferences in the optimization process. These preferences are in the form of arc probabilities, i.e., the more preferred a route is, the higher is the joint probability. The novelty of this work is the use of a neural network model to estimate the arc probabilities, which allows for additional features and automatic parameter estimation. This first requires identifying suitable features, neural architectures and loss functions, taking into account that there is typically few data available. We investigate the difference with a prior weighted Markov counting approach, and study the applicability of neural networks in this setting., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 42:1-42:17

Recent advances in solvers for the Boolean satisfiability (SAT) based optimization paradigm of maximum satisfiability (MaxSAT) have turned MaxSAT into a viable approach to finding provably optimal solutions for various types of hard optimization problems. In various types of real-world problem settings, a sequence of related optimization problems need to solved. This calls for studying ways of enabling incremental computations in MaxSAT, with the hope of speeding up the overall computation times. However, current state-of-the-art MaxSAT solvers offer no or limited forms of incrementality. In this work, we study ways of enabling incremental computations in the context of the implicit hitting set (IHS) approach to MaxSAT solving, as both one of the key MaxSAT solving approaches today and a relatively well-suited candidate for extending to incremental computations. In particular, motivated by several recent applications of MaxSAT in the context of interpretability in machine learning calling for this type of incrementality, we focus on enabling incrementality in IHS under changes to the objective function coefficients (i.e., to the weights of soft clauses). To this end, we explain to what extent different search techniques applied in IHS-based MaxSAT solving can and cannot be adapted to this incremental setting. As practical result, we develop an incremental version of an IHS MaxSAT solver, and show it provides significant runtime improvements in recent application settings which can benefit from incrementality but in which MaxSAT solvers have so-far been applied only non-incrementally, i.e., by calling a MaxSAT solver from scratch after each change to the problem instance at hand., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 44:1-44:19

High-performance Computing (HPC) systems have become essential instruments in our modern society. As they get closer to exascale performance, HPC systems become larger in size and more heterogeneous in their computing resources. With recent advances in AI, HPC systems are also increasingly being used for applications that employ many short jobs with strict timing requirements. HPC job dispatchers need to therefore adopt techniques to go beyond the capabilities of those developed for small or homogeneous systems, or for traditional compute-intensive applications. In this paper, we present a job dispatcher suitable for today’s large and heterogeneous systems running modern applications. Unlike its predecessors, our dispatcher solves the entire dispatching problem using Constraint Programming (CP) with a model size independent of the system size. Experimental results based on a simulation study show that our approach can bring about significant performance gains over the existing CP-based dispatchers in a large or heterogeneous system., LIPIcs, Vol. 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021), pages 26:1-26:16