LIPIcs, Volume 210

27th International Conference on Principles and Practice of Constraint Programming (CP 2021)



Thumbnail PDF

Event

CP 2021, October 25-29, 2021, Montpellier, France (Virtual Conference)

Editor

Laurent D. Michel
  • University of Connecticut, USA

Publication Details

  • published at: 2021-10-15
  • Publisher: Schloss Dagstuhl – Leibniz-Zentrum für Informatik
  • ISBN: 978-3-95977-211-2
  • DBLP: db/conf/cp/cp2021

Access Numbers

Documents

No documents found matching your filter selection.
Document
Complete Volume
LIPIcs, Volume 210, CP 2021, Complete Volume

Authors: Laurent D. Michel


Abstract
LIPIcs, Volume 210, CP 2021, Complete Volume

Cite as

27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 1-1000, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@Proceedings{michel:LIPIcs.CP.2021,
  title =	{{LIPIcs, Volume 210, CP 2021, Complete Volume}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{1--1000},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021},
  URN =		{urn:nbn:de:0030-drops-152907},
  doi =		{10.4230/LIPIcs.CP.2021},
  annote =	{Keywords: LIPIcs, Volume 210, CP 2021, Complete Volume}
}
Document
Front Matter
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Laurent D. Michel


Abstract
Front Matter, Table of Contents, Preface, Conference Organization

Cite as

27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 0:i-0:xxii, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{michel:LIPIcs.CP.2021.0,
  author =	{Michel, Laurent D.},
  title =	{{Front Matter, Table of Contents, Preface, Conference Organization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{0:i--0:xxii},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.0},
  URN =		{urn:nbn:de:0030-drops-152916},
  doi =		{10.4230/LIPIcs.CP.2021.0},
  annote =	{Keywords: Front Matter, Table of Contents, Preface, Conference Organization}
}
Document
Invited Talk
The Bi-Objective Long-Haul Transportation Problem on a Road Network (Invited Talk)

Authors: Claudia Archetti, Ola Jabali, Andrea Mor, Alberto Simonetto, and M.Grazia Speranza


Abstract
Long-haul truck transportation is concerned with freight transportation from shipments' origins to destinations, with vehicle trips lasting from some hours to several days. Drivers performing long-haul transportation are subject to strict rules derived from Hours of Service (HoS) regulations. There exists a large body of literature integrating HoS regulations within long-haul transportation. The optimization problems in this context generally deal with routing and scheduling decisions aimed at determining where a driver should stop and how long a rest should be. However, the overwhelming majority of the literature on long-haul transportation ignores refueling decisions and treats fuel costs as proportional to the traveled distance. In this talk we analyze a long-haul truck scheduling problem where a path has to be determined for a vehicle traveling from a specified origin to a specified destination. We consider refueling decisions along the path while accounting for heterogeneous fuel prices in a road network. Furthermore, the path has to comply with Hours of Service (HOS) regulations. Therefore, a path is defined by the actual road trajectory traveled by the vehicle, as well as the locations where the vehicle stops due to refueling, compliance with HOS regulations, or a combination of the two. This setting is cast in a bi-objective optimization problem, considering the minimization of fuel cost and the minimization of path duration. An algorithm is proposed to solve the problem on a road network. The algorithm builds a set of non-dominated paths with respect to the two objectives. Given the enormous theoretical size of the road network, the algorithm follows an interactive path construction mechanism. Specifically, the algorithm dynamically interacts with a geographic information system to identify the relevant potential paths and stop locations. Computational tests are made on real-sized instances where the distance covered ranges from 500 to 1500 km. The algorithm is compared with solutions obtained from a policy mimicking the current practice of a logistics company. The results show that the non-dominated solutions produced by the algorithm significantly dominate the ones generated by the current practice, in terms of fuel costs, while achieving similar path durations. The average number of non-dominated paths is 2.7, which allows decision-makers to ultimately visually inspect the proposed alternatives.

Cite as

Claudia Archetti, Ola Jabali, Andrea Mor, Alberto Simonetto, and M.Grazia Speranza. The Bi-Objective Long-Haul Transportation Problem on a Road Network (Invited Talk). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, p. 1:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{archetti_et_al:LIPIcs.CP.2021.1,
  author =	{Archetti, Claudia and Jabali, Ola and Mor, Andrea and Simonetto, Alberto and Speranza, M.Grazia},
  title =	{{The Bi-Objective Long-Haul Transportation Problem on a Road Network}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{1:1--1:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.1},
  URN =		{urn:nbn:de:0030-drops-152926},
  doi =		{10.4230/LIPIcs.CP.2021.1},
  annote =	{Keywords: Truck scheduling problem, hours of service regulations, fuel costs}
}
Document
Invited Talk
Constrained-Based Differential Privacy (Invited Talk)

Authors: Ferdinando Fioretto


Abstract
Data sets and statistics about groups of individuals are increasingly collected and released, feeding many optimization and learning algorithms. In many cases, the released data contain sensitive information whose privacy is strictly regulated. For example, in the U.S., the census data is regulated under Title 13, which requires that no individual be identified from any data released by the Census Bureau. In Europe, data release is regulated according to the General Data Protection Regulation, which addresses the control and transfer of personal data. Differential privacy has emerged as the de-facto standard to protect data privacy. In a nutshell, differentially private algorithms protect an individual’s data by injecting random noise into the output of a computation that involves such data. While this process ensures privacy, it also impacts the quality of data analysis, and, when private data sets are used as inputs to complex machine learning or optimization tasks, they may produce results that are fundamentally different from those obtained on the original data and even rise unintended bias and fairness concerns. In this talk, I will first focus on the challenge of releasing privacy-preserving data sets for complex data analysis tasks. I will introduce the notion of Constrained-based Differential Privacy (C-DP), which allows casting the data release problem to an optimization problem whose goal is to preserve the salient features of the original data. I will review several applications of C-DP in the context of very large hierarchical census data, data streams, energy systems, and in the design of federated data-sharing protocols. Next, I will discuss how errors induced by differential privacy algorithms may propagate within a decision problem causing biases and fairness issues. This is particularly important as privacy-preserving data is often used for critical decision processes, including the allocation of funds and benefits to states and jurisdictions, which ideally should be fair and unbiased. Finally, I will conclude with a roadmap to future work and some open questions.

Cite as

Ferdinando Fioretto. Constrained-Based Differential Privacy (Invited Talk). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fioretto:LIPIcs.CP.2021.2,
  author =	{Fioretto, Ferdinando},
  title =	{{Constrained-Based Differential Privacy}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{2:1--2:1},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.2},
  URN =		{urn:nbn:de:0030-drops-152931},
  doi =		{10.4230/LIPIcs.CP.2021.2},
  annote =	{Keywords: Optimization, Differential Privacy, Fairness}
}
Document
Invited Talk
Learning in Local Branching (Invited Talk)

Authors: Defeng Liu and Andrea Lodi


Abstract
Although state-of-the-art solvers for Mixed-Integer Programming (MIP) experienced a dramatic performance improvement over the past decades, the resolution of some MIPs is still challenging, requiring hours of computations while, in practice, high-quality solutions are often required to be computed within a very restricted time frame. In such cases, it might be preferable to provide anytime solutions, i.e., a first reasonable solution should be generated as early as possible, then better ones produced in the subsequent computation with the user deciding where to stop. In this respect, the local branching (LB) heuristic [Fischetti and Lodi, 2003] was proposed to improve an incumbent solution either at very early stages of the computation within a general MIP framework or as a stand-alone algorithmic framework. Roughly speaking, given a feasible solution, the method iterates by first defining a solution neighborhood through the so-called local branching cut, then by exploring it by calling a black-box MIP solver. In the local branching algorithm, the choice of the neighborhood size is crucial to performance. In principle, it is desirable to have neighborhoods to be relatively small for efficient computation but still large enough to contain improving solutions. In [Fischetti and Lodi, 2003], the size of the neighborhood is mostly initialized by a fixed constant value, then adjusted at run time. Nonetheless, it is reasonable to believe that there is no a priori single best neighborhood size and the choice of the value should depend on the characteristics of the problem. Furthermore, it is worth noting that, in many applications, instances of the same problem are solved repeatedly. Real-world problems have a rich structure: while more and more data points are collected, patterns and regularities appear. Therefore, problem-specific and task-specific knowledge can be learned from data and applied to adapting the corresponding optimization scenario. This motives a broader paradigm of sizing the solution neighborhoods in local branching. Following the line of work analyzed and surveyed in [Bengio et al., 2021] on the use of Machine Learning (ML) for combinatorial optimization, in this work, we aim to guide the (local) search of the local branching heuristic by ML techniques. In particular, given a problem instance and a time limit for (heuristically) solving it, we exploit ML tools to predict reasonable good values of the neighborhood size, in order to maximize the performance of the local branching algorithm. We computationally show that the neighborhood size can indeed be learnt leading to improved performances and that the overall algorithm generalizes well both with respect to the instance size and, more surprisingly, across instances.

Cite as

Defeng Liu and Andrea Lodi. Learning in Local Branching (Invited Talk). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CP.2021.3,
  author =	{Liu, Defeng and Lodi, Andrea},
  title =	{{Learning in Local Branching}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.3},
  URN =		{urn:nbn:de:0030-drops-152948},
  doi =		{10.4230/LIPIcs.CP.2021.3},
  annote =	{Keywords: Local search, learning, mixed-integer programming}
}
Document
Short Paper
Filtering Isomorphic Models by Invariants (Short Paper)

Authors: João Araújo, Choiwah Chow, and Mikoláš Janota


Abstract
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.

Cite as

João Araújo, Choiwah Chow, and Mikoláš Janota. Filtering Isomorphic Models by Invariants (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 4:1-4:9, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{araujo_et_al:LIPIcs.CP.2021.4,
  author =	{Ara\'{u}jo, Jo\~{a}o and Chow, Choiwah and Janota, Mikol\'{a}\v{s}},
  title =	{{Filtering Isomorphic Models by Invariants}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{4:1--4:9},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.4},
  URN =		{urn:nbn:de:0030-drops-152956},
  doi =		{10.4230/LIPIcs.CP.2021.4},
  annote =	{Keywords: finite model enumeration, isomorphism, invariants, Mace4}
}
Document
Short Paper
Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper)

Authors: Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang


Abstract
This work is dedicated to improving local search solvers for the Boolean satisfiability (SAT) problem on structured instances. We propose a construct-and-cut (CnC) algorithm based on unit propagation, which is used to produce initial assignments for local search. We integrate our CnC initialization procedure within several state-of-the-art local search SAT solvers, and obtain the improved solvers. Experiments are carried out with a benchmark encoded from a spectrum repacking project as well as benchmarks encoded from two important mathematical problems namely Boolean Pythagorean Triple and Schur Number Five. The experiments show that the CnC initialization improves the local search solvers, leading to better performance than state-of-the-art SAT solvers based on Conflict Driven Clause Learning (CDCL) solvers.

Cite as

Shaowei Cai, Chuan Luo, Xindi Zhang, and Jian Zhang. Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 5:1-5:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cai_et_al:LIPIcs.CP.2021.5,
  author =	{Cai, Shaowei and Luo, Chuan and Zhang, Xindi and Zhang, Jian},
  title =	{{Improving Local Search for Structured SAT Formulas via Unit Propagation Based Construct and Cut Initialization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{5:1--5:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.5},
  URN =		{urn:nbn:de:0030-drops-152969},
  doi =		{10.4230/LIPIcs.CP.2021.5},
  annote =	{Keywords: Satisfiability, Local Search, Unit Propagation, Mathematical Problems}
}
Document
Short Paper
Unit Propagation with Stable Watches (Short Paper)

Authors: Markus Iser and Tomáš Balyo


Abstract
Unit propagation is the hottest path in CDCL SAT solvers, therefore the related data-structures, algorithms and implementation details are well studied and highly optimized. State-of-the-art implementations are based on reduced occurrence tracking with two watched literals per clause and one blocking literal per watcher in order to further reduce the number of clause accesses. In this paper, we show that using runtime statistics for watched literal selection can improve the performance of state-of-the-art SAT solvers. We present a method for efficiently keeping track of spans during which literals are satisfied and using this statistic to improve watcher selection. An implementation of our method in the SAT solver CaDiCaL can solve more instances of the SAT Competition 2019 and 2020 benchmark sets and is specifically strong on satisfiable cryptographic instances.

Cite as

Markus Iser and Tomáš Balyo. Unit Propagation with Stable Watches (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 6:1-6:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{iser_et_al:LIPIcs.CP.2021.6,
  author =	{Iser, Markus and Balyo, Tom\'{a}\v{s}},
  title =	{{Unit Propagation with Stable Watches}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{6:1--6:8},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.6},
  URN =		{urn:nbn:de:0030-drops-152973},
  doi =		{10.4230/LIPIcs.CP.2021.6},
  annote =	{Keywords: Unit Propagation, Two-Watched Literals, Literal Stability}
}
Document
Short Paper
Towards Better Heuristics for Solving Bounded Model Checking Problems (Short Paper)

Authors: Anissa Kheireddine, Etienne Renault, and Souheib Baarir


Abstract
This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results.

Cite as

Anissa Kheireddine, Etienne Renault, and Souheib Baarir. Towards Better Heuristics for Solving Bounded Model Checking Problems (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 7:1-7:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{kheireddine_et_al:LIPIcs.CP.2021.7,
  author =	{Kheireddine, Anissa and Renault, Etienne and Baarir, Souheib},
  title =	{{Towards Better Heuristics for Solving Bounded Model Checking Problems}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{7:1--7:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.7},
  URN =		{urn:nbn:de:0030-drops-152982},
  doi =		{10.4230/LIPIcs.CP.2021.7},
  annote =	{Keywords: Bounded model checking, SAT, Structural information, Linear Programming}
}
Document
Short Paper
Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)

Authors: Tuukka Korhonen and Matti Järvisalo


Abstract
Propositional model counting (#SAT), the problem of determining the number of satisfying assignments of a propositional formula, is the archetypical #P-complete problem with a wide range of applications in AI. In this paper, we show that integrating tree decompositions of low width into the decision heuristics of a reference exact model counter (SharpSAT) significantly improves its runtime performance. In particular, our modifications to SharpSAT (and its derivant GANAK) lift the runtime efficiency of SharpSAT to the extent that it outperforms state-of-the-art exact model counters, including earlier-developed model counters that exploit tree decompositions.

Cite as

Tuukka Korhonen and Matti Järvisalo. Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 8:1-8:11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{korhonen_et_al:LIPIcs.CP.2021.8,
  author =	{Korhonen, Tuukka and J\"{a}rvisalo, Matti},
  title =	{{Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{8:1--8:11},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.8},
  URN =		{urn:nbn:de:0030-drops-152992},
  doi =		{10.4230/LIPIcs.CP.2021.8},
  annote =	{Keywords: propositional model counting, decision heuristics, tree decompositions, empirical evaluation}
}
Document
Short Paper
Failure Based Variable Ordering Heuristics for Solving CSPs (Short Paper)

Authors: Hongbo Li, Minghao Yin, and Zhanshan Li


Abstract
Variable ordering heuristics play a central role in solving constraint satisfaction problems. In this paper, we propose failure based variable ordering heuristics. Following the fail first principle, the new heuristics use two aspects of failure information collected during search. The failure rate heuristics consider the failure proportion after the propagations of assignments of variables and the failure length heuristics consider the length of failures, which is the number of fixed variables composing a failure. We performed a vast experiments in 41 problems with 1876 MiniZinc instances. The results show that the failure based heuristics outperform the existing ones including activity-based search, conflict history search, the refined weighted degree and correlation-based search. They can be new candidates of general purpose variable ordering heuristics for black-box CSP solvers.

Cite as

Hongbo Li, Minghao Yin, and Zhanshan Li. Failure Based Variable Ordering Heuristics for Solving CSPs (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 9:1-9:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CP.2021.9,
  author =	{Li, Hongbo and Yin, Minghao and Li, Zhanshan},
  title =	{{Failure Based Variable Ordering Heuristics for Solving CSPs}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{9:1--9:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.9},
  URN =		{urn:nbn:de:0030-drops-153002},
  doi =		{10.4230/LIPIcs.CP.2021.9},
  annote =	{Keywords: Constraint Satisfaction Problem, Variable Ordering Heuristic, Failure Rate, Failure Length}
}
Document
Short Paper
Generating Magical Performances with Constraint Programming (Short Paper)

Authors: Guilherme de Azevedo Silveira


Abstract
Professional magicians employ the use of interesting properties of a deck of cards to create magical effects. These properties were traditionally discovered through trial and error, the application of heuristics or analytical proofs. We discuss the limitations of relying on humans for such methods and present how professional magicians can use constraint programming as a computer-aided design tool to search for desired properties in a deck of cards. Furthermore, we implement a solution in Python making use of generative magic to design a new effect, demonstrating how this process broadens the level of freedom a magician can decree to their volunteers while retaining control of the outcomes of the magic. Finally, we demonstrate the model can be easily adapted to multiple languages.

Cite as

Guilherme de Azevedo Silveira. Generating Magical Performances with Constraint Programming (Short Paper). In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 10:1-10:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{deazevedosilveira:LIPIcs.CP.2021.10,
  author =	{de Azevedo Silveira, Guilherme},
  title =	{{Generating Magical Performances with Constraint Programming}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{10:1--10:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.10},
  URN =		{urn:nbn:de:0030-drops-153018},
  doi =		{10.4230/LIPIcs.CP.2021.10},
  annote =	{Keywords: Constraint, generative design, computer aided design, constraint programming, generative magic, magical performance}
}
Document
Vehicle Dynamics in Pickup-And-Delivery Problems Using Electric Vehicles

Authors: Saman Ahmadi, Guido Tack, Daniel Harabor, and Philip Kilby


Abstract
Electric Vehicles (EVs) are set to replace vehicles based on internal combustion engines. Path planning and vehicle routing for EVs need to take their specific characteristics into account, such as reduced range, long charging times, and energy recuperation. This paper investigates the importance of vehicle dynamics parameters in energy models for EV routing, particularly in the Pickup-and-Delivery Problem (PDP). We use Constraint Programming (CP) technology to develop a complete PDP model with different charger technologies. We adapt realistic instances that consider vehicle dynamics parameters such as vehicle mass, road gradient and driving speed to varying degrees. The results of our experiments show that neglecting such fundamental vehicle dynamics parameters can affect the feasibility of planned routes for EVs, and fewer/shorter charging visits will be planned if we use energy-efficient paths instead of conventional shortest paths in the underlying system model.

Cite as

Saman Ahmadi, Guido Tack, Daniel Harabor, and Philip Kilby. Vehicle Dynamics in Pickup-And-Delivery Problems Using Electric Vehicles. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 11:1-11:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ahmadi_et_al:LIPIcs.CP.2021.11,
  author =	{Ahmadi, Saman and Tack, Guido and Harabor, Daniel and Kilby, Philip},
  title =	{{Vehicle Dynamics in Pickup-And-Delivery Problems Using Electric Vehicles}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{11:1--11:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.11},
  URN =		{urn:nbn:de:0030-drops-153020},
  doi =		{10.4230/LIPIcs.CP.2021.11},
  annote =	{Keywords: Electric vehicle routing, pickup-and-delivery problem, vehicle dynamics}
}
Document
Building High Strength Mixed Covering Arrays with Constraints

Authors: Carlos Ansótegui, Jesús Ojeda, and Eduard Torres


Abstract
Covering arrays have become a key piece in Combinatorial Testing. In particular, we focus on the efficient construction of Covering Arrays with Constraints of high strength. SAT solving technology has been proven to be well suited when solving Covering Arrays with Constraints. However, the size of the SAT reformulations rapidly grows up with higher strengths. To this end, we present a new incomplete algorithm that mitigates substantially memory blow-ups. The experimental results confirm the goodness of the approach, opening avenues for new practical applications.

Cite as

Carlos Ansótegui, Jesús Ojeda, and Eduard Torres. Building High Strength Mixed Covering Arrays with Constraints. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 12:1-12:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ansotegui_et_al:LIPIcs.CP.2021.12,
  author =	{Ans\'{o}tegui, Carlos and Ojeda, Jes\'{u}s and Torres, Eduard},
  title =	{{Building High Strength Mixed Covering Arrays with Constraints}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{12:1--12:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.12},
  URN =		{urn:nbn:de:0030-drops-153036},
  doi =		{10.4230/LIPIcs.CP.2021.12},
  annote =	{Keywords: Combinatorial Testing, Covering Arrays, Maximum Satisfiability}
}
Document
On How Turing and Singleton Arc Consistency Broke the Enigma Code

Authors: Valentin Antuori, Tom Portoleau, Louis Rivière, and Emmanuel Hebrard


Abstract
In this paper, we highlight an intriguing connection between the cryptographic attacks on Enigma’s code and local consistency reasoning in constraint programming. The coding challenge proposed to the students during the 2020 ACP summer school, to be solved by constraint programming, was to decipher a message encoded using the well known Enigma machine, with as only clue a tiny portion of the original message. A number of students quickly crafted a model, thus nicely showcasing CP technology - as well as their own brightness. The detail that is slightly less favorable to CP technology is that solving this model on modern hardware is challenging, whereas the "Bombe", an antique computing device, could solve it eighty years ago. We argue that from a constraint programming point of vue, the key aspects of the techniques designed by Polish and British cryptanalysts can be seen as, respectively, path consistency and singleton arc consistency on some constraint satisfaction problems.

Cite as

Valentin Antuori, Tom Portoleau, Louis Rivière, and Emmanuel Hebrard. On How Turing and Singleton Arc Consistency Broke the Enigma Code. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 13:1-13:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{antuori_et_al:LIPIcs.CP.2021.13,
  author =	{Antuori, Valentin and Portoleau, Tom and Rivi\`{e}re, Louis and Hebrard, Emmanuel},
  title =	{{On How Turing and Singleton Arc Consistency Broke the Enigma Code}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.13},
  URN =		{urn:nbn:de:0030-drops-153040},
  doi =		{10.4230/LIPIcs.CP.2021.13},
  annote =	{Keywords: Constraint Programming, Cryptography}
}
Document
Combining Monte Carlo Tree Search and Depth First Search Methods for a Car Manufacturing Workshop Scheduling Problem

Authors: Valentin Antuori, Emmanuel Hebrard, Marie-José Huguet, Siham Essodaigui, and Alain Nguyen


Abstract
Many state-of-the-art methods for combinatorial games rely on Monte Carlo Tree Search (MCTS) method, coupled with machine learning techniques, and these techniques have also recently been applied to combinatorial optimization. In this paper, we propose an efficient approach to a Travelling Salesman Problem with time windows and capacity constraints from the automotive industry. This approach combines the principles of MCTS to balance exploration and exploitation of the search space and a backtracking method to explore promising branches, and to collect relevant information on visited subtrees. This is done simply by replacing the Monte-Carlo rollouts by budget-limited runs of a DFS method. Moreover, the evaluation of the promise of a node in the Monte-Carlo search tree is key, and is a major difference with the case of games. For that purpose, we propose to evaluate a node using the marginal increase of a lower bound of the objective function, weighted with an exponential decay on the depth, in previous simulations. Finally, since the number of Monte-Carlo rollouts and hence the confidence on the evaluation is higher towards the root of the search tree, we propose to adjust the balance exploration/exploitation to the length of the branch. Our experiments show that this method clearly outperforms the best known approaches for this problem.

Cite as

Valentin Antuori, Emmanuel Hebrard, Marie-José Huguet, Siham Essodaigui, and Alain Nguyen. Combining Monte Carlo Tree Search and Depth First Search Methods for a Car Manufacturing Workshop Scheduling Problem. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 14:1-14:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{antuori_et_al:LIPIcs.CP.2021.14,
  author =	{Antuori, Valentin and Hebrard, Emmanuel and Huguet, Marie-Jos\'{e} and Essodaigui, Siham and Nguyen, Alain},
  title =	{{Combining Monte Carlo Tree Search and Depth First Search Methods for a Car Manufacturing Workshop Scheduling Problem}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{14:1--14:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.14},
  URN =		{urn:nbn:de:0030-drops-153052},
  doi =		{10.4230/LIPIcs.CP.2021.14},
  annote =	{Keywords: Monte-Carlo Tree Search, Travelling Salesman Problem, Scheduling}
}
Document
Practical Bigraphs via Subgraph Isomorphism

Authors: Blair Archibald, Kyle Burns, Ciaran McCreesh, and Michele Sevegnani


Abstract
Bigraphs simultaneously model the spatial and non-spatial relationships between entities, and have been used for systems modelling in areas including biology, networking, and sensors. Temporal evolution can be modelled through a rewriting system, driven by a matching algorithm that identifies instances of bigraphs to be rewritten. The previous state-of-the-art matching algorithm for bigraphs with sharing is based on Boolean satisfiability (SAT), and suffers from a large encoding that limits scalability and makes it hard to support extensions. This work instead adapts a subgraph isomorphism solver that is based upon constraint programming to solve the bigraph matching problem. This approach continues to support bigraphs with sharing, is more open to other extensions and side constraints, and improves performance by over two orders of magnitude on a range of problem instances drawn from real-world mixed-reality, protocol, and conference models.

Cite as

Blair Archibald, Kyle Burns, Ciaran McCreesh, and Michele Sevegnani. Practical Bigraphs via Subgraph Isomorphism. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 15:1-15:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{archibald_et_al:LIPIcs.CP.2021.15,
  author =	{Archibald, Blair and Burns, Kyle and McCreesh, Ciaran and Sevegnani, Michele},
  title =	{{Practical Bigraphs via Subgraph Isomorphism}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{15:1--15:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.15},
  URN =		{urn:nbn:de:0030-drops-153068},
  doi =		{10.4230/LIPIcs.CP.2021.15},
  annote =	{Keywords: bigraphs, subgraph isomorphism, constraint programming, rewriting systems}
}
Document
The Hybrid Flexible Flowshop with Transportation Times

Authors: Eddie Armstrong, Michele Garraffa, Barry O'Sullivan, and Helmut Simonis


Abstract
This paper presents the hybrid, flexible flowshop problem with transportation times between stages, which is an extension of an existing scheduling problem that is well-studied in the literature. We explore different models for the problem with Constraint Programming, MILP, and local search, and compare them on generated benchmark problems that reflect the problem of the industrial partner. We then study two different factory layout design problems, and use the optimization tool to understand the impact of the design choices on the solution quality.

Cite as

Eddie Armstrong, Michele Garraffa, Barry O'Sullivan, and Helmut Simonis. The Hybrid Flexible Flowshop with Transportation Times. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{armstrong_et_al:LIPIcs.CP.2021.16,
  author =	{Armstrong, Eddie and Garraffa, Michele and O'Sullivan, Barry and Simonis, Helmut},
  title =	{{The Hybrid Flexible Flowshop with Transportation Times}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{16:1--16:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.16},
  URN =		{urn:nbn:de:0030-drops-153075},
  doi =		{10.4230/LIPIcs.CP.2021.16},
  annote =	{Keywords: Constraint Programming, scheduling, hybrid flowshop}
}
Document
CLR-DRNets: Curriculum Learning with Restarts to Solve Visual Combinatorial Games

Authors: Yiwei Bai, Di Chen, and Carla P. Gomes


Abstract
We introduce a curriculum learning framework for challenging tasks that require a combination of pattern recognition and combinatorial reasoning, such as single-player visual combinatorial games. Our work harnesses Deep Reasoning Nets (DRNets) [Chen et al., 2020], a framework that combines deep learning with constraint reasoning for unsupervised pattern demixing. We propose CLR-DRNets (pronounced Clear-DRNets), a curriculum-learning-with-restarts framework to boost the performance of DRNets. CLR-DRNets incrementally increase the difficulty of the training instances and use restarts, a new model selection method that selects multiple models from the same training trajectory to learn a set of diverse heuristics and apply them at inference time. An enhanced reasoning module is also proposed for CLR-DRNets to improve the ability of reasoning and generalize to unseen instances. We consider Visual Sudoku, i.e., Sudoku with hand-written digits or letters, and Visual Mixed Sudoku, a substantially more challenging task that requires the demixing and completion of two overlapping Visual Sudokus. We propose an enhanced reasoning module for the DRNets framework for encoding these visual games We show how CLR-DRNets considerably outperform DRNets and other approaches on these visual combinatorial games.

Cite as

Yiwei Bai, Di Chen, and Carla P. Gomes. CLR-DRNets: Curriculum Learning with Restarts to Solve Visual Combinatorial Games. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 17:1-17:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bai_et_al:LIPIcs.CP.2021.17,
  author =	{Bai, Yiwei and Chen, Di and Gomes, Carla P.},
  title =	{{CLR-DRNets: Curriculum Learning with Restarts to Solve Visual Combinatorial Games}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{17:1--17:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.17},
  URN =		{urn:nbn:de:0030-drops-153086},
  doi =		{10.4230/LIPIcs.CP.2021.17},
  annote =	{Keywords: Unsupervised Learning, Combinatorial Optimization}
}
Document
An Interval Constraint Programming Approach for Quasi Capture Tube Validation

Authors: Abderahmane Bedouhene, Bertrand Neveu, Gilles Trombettoni, Luc Jaulin, and Stéphane Le Menec


Abstract
Proving that the state of a controlled nonlinear system always stays inside a time moving bubble (or capture tube) amounts to proving the inconsistency of a set of nonlinear inequalities in the time-state space. In practice however, even with a good intuition, it is difficult for a human to find such a capture tube except for simple examples. In 2014, Jaulin et al. established properties that support a new interval approach for validating a quasi capture tube, i.e. a candidate tube (with a simple form) from which the mobile system can escape, but into which it enters again before a given time. A quasi capture tube is easy to find in practice for a controlled system. Merging the trajectories originated from the candidate tube yields the smallest capture tube enclosing it. This paper proposes an interval constraint programming solver dedicated to the quasi capture tube validation. The problem is viewed as a differential CSP where the functional variables correspond to the state variables of the system and the constraints define system trajectories that escape from the candidate tube "for ever". The solver performs a branch and contract procedure for computing the trajectories that escape from the candidate tube. If no solution is found, the quasi capture tube is validated and, as a side effect, a corrected smallest capture tube enclosing the quasi one is computed. The approach is experimentally validated on several examples having 2 to 5 degrees of freedom.

Cite as

Abderahmane Bedouhene, Bertrand Neveu, Gilles Trombettoni, Luc Jaulin, and Stéphane Le Menec. An Interval Constraint Programming Approach for Quasi Capture Tube Validation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{bedouhene_et_al:LIPIcs.CP.2021.18,
  author =	{Bedouhene, Abderahmane and Neveu, Bertrand and Trombettoni, Gilles and Jaulin, Luc and Le Menec, St\'{e}phane},
  title =	{{An Interval Constraint Programming Approach for Quasi Capture Tube Validation}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{18:1--18:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.18},
  URN =		{urn:nbn:de:0030-drops-153093},
  doi =		{10.4230/LIPIcs.CP.2021.18},
  annote =	{Keywords: Constraint satisfaction problem, Interval analysis, Dynamical systems, Contractor}
}
Document
Exhaustive Generation of Benzenoid Structures Sharing Common Patterns

Authors: Yannick Carissan, Denis Hagebaum-Reignier, Nicolas Prcovic, Cyril Terrioux, and Adrien Varet


Abstract
Benzenoids are a subfamily of hydrocarbons (molecules that are only made of hydrogen and carbon atoms) whose carbon atoms form hexagons. These molecules are widely studied both experimentally and theoretically and can have various physicochemical properties (mechanical resistance, electronic conductivity, ...) from which a lot of concrete applications are derived. These properties can rely on the existence or absence of fragments of the molecule corresponding to a given pattern (some patterns impose the nature of certain bonds, which has an impact on the whole electronic structure). The exhaustive generation of families of benzenoids sharing the absence or presence of given patterns is an important problem in chemistry, particularly in theoretical chemistry, where various methods can be used to better understand the link between their shapes and their electronic properties. In this paper, we show how constraint programming can help chemists to answer different questions around this problem. To do so, we propose different models including one based on a variant of the subgraph isomorphism problem and we generate the desired structures using Choco solver.

Cite as

Yannick Carissan, Denis Hagebaum-Reignier, Nicolas Prcovic, Cyril Terrioux, and Adrien Varet. Exhaustive Generation of Benzenoid Structures Sharing Common Patterns. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 19:1-19:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{carissan_et_al:LIPIcs.CP.2021.19,
  author =	{Carissan, Yannick and Hagebaum-Reignier, Denis and Prcovic, Nicolas and Terrioux, Cyril and Varet, Adrien},
  title =	{{Exhaustive Generation of Benzenoid Structures Sharing Common Patterns}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{19:1--19:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.19},
  URN =		{urn:nbn:de:0030-drops-153106},
  doi =		{10.4230/LIPIcs.CP.2021.19},
  annote =	{Keywords: Constraint satisfaction problem, modeling, pattern, application, theoretical chemistry}
}
Document
Combining VSIDS and CHB Using Restarts in SAT

Authors: Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux


Abstract
Conflict Driven Clause Learning (CDCL) solvers are known to be efficient on structured instances and manage to solve ones with a large number of variables and clauses. An important component in such solvers is the branching heuristic which picks the next variable to branch on. In this paper, we evaluate different strategies which combine two state-of-the-art heuristics, namely the Variable State Independent Decaying Sum (VSIDS) and the Conflict History-Based (CHB) branching heuristic. These strategies take advantage of the restart mechanism, which helps to deal with the heavy-tailed phenomena in SAT, to switch between these heuristics thus ensuring a better and more diverse exploration of the search space. Our experimental evaluation shows that combining VSIDS and CHB using restarts achieves competitive results and even significantly outperforms both heuristics for some chosen strategies.

Cite as

Mohamed Sami Cherif, Djamal Habet, and Cyril Terrioux. Combining VSIDS and CHB Using Restarts in SAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 20:1-20:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cherif_et_al:LIPIcs.CP.2021.20,
  author =	{Cherif, Mohamed Sami and Habet, Djamal and Terrioux, Cyril},
  title =	{{Combining VSIDS and CHB Using Restarts in SAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{20:1--20:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.20},
  URN =		{urn:nbn:de:0030-drops-153110},
  doi =		{10.4230/LIPIcs.CP.2021.20},
  annote =	{Keywords: Satisfiability, Branching Heuristic, Restarts}
}
Document
On the Tractability of Explaining Decisions of Classifiers

Authors: Martin C. Cooper and João Marques-Silva


Abstract
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.

Cite as

Martin C. Cooper and João Marques-Silva. On the Tractability of Explaining Decisions of Classifiers. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cooper_et_al:LIPIcs.CP.2021.21,
  author =	{Cooper, Martin C. and Marques-Silva, Jo\~{a}o},
  title =	{{On the Tractability of Explaining Decisions of Classifiers}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.21},
  URN =		{urn:nbn:de:0030-drops-153125},
  doi =		{10.4230/LIPIcs.CP.2021.21},
  annote =	{Keywords: machine learning, tractability, explanations, weighted constraint satisfaction}
}
Document
A Collection of Constraint Programming Models for the Three-Dimensional Stable Matching Problem with Cyclic Preferences

Authors: Ágnes Cseh, Guillaume Escamocher, Begüm Genç, and Luis Quesada


Abstract
We introduce five constraint models for the 3-dimensional stable matching problem with cyclic preferences and study their relative performances under diverse configurations. While several constraint models have been proposed for variants of the two-dimensional stable matching problem, we are the first to present constraint models for a higher number of dimensions. We show for all five models how to capture two different stability notions, namely weak and strong stability. Additionally, we translate some well-known fairness notions (i.e. sex-equal, minimum regret, egalitarian) into 3-dimensional matchings, and present how to capture them in each model. Our tests cover dozens of problem sizes and four different instance generation methods. We explore two levels of commitment in our models: one where we have an individual variable for each agent (individual commitment), and another one where the determination of a variable involves pairing the three agents at once (group commitment). Our experiments show that the suitability of the commitment depends on the type of stability we are dealing with. Our experiments not only led us to discover dependencies between the type of stability and the instance generation method, but also brought light to the role that learning and restarts can play in solving this kind of problems.

Cite as

Ágnes Cseh, Guillaume Escamocher, Begüm Genç, and Luis Quesada. A Collection of Constraint Programming Models for the Three-Dimensional Stable Matching Problem with Cyclic Preferences. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cseh_et_al:LIPIcs.CP.2021.22,
  author =	{Cseh, \'{A}gnes and Escamocher, Guillaume and Gen\c{c}, Beg\"{u}m and Quesada, Luis},
  title =	{{A Collection of Constraint Programming Models for the Three-Dimensional Stable Matching Problem with Cyclic Preferences}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.22},
  URN =		{urn:nbn:de:0030-drops-153137},
  doi =		{10.4230/LIPIcs.CP.2021.22},
  annote =	{Keywords: Three-dimensional stable matching with cyclic preferences, 3DSM-cyc, Constraint Programming, fairness}
}
Document
Bounds on Weighted CSPs Using Constraint Propagation and Super-Reparametrizations

Authors: Tomáš Dlask, Tomáš Werner, and Simon de Givry


Abstract
We propose a framework for computing upper bounds on the optimal value of the (maximization version of) Weighted CSP (WCSP) using super-reparametrizations, which are changes of the weights that keep or increase the WCSP objective for every assignment. We show that it is in principle possible to employ arbitrary (under certain technical conditions) constraint propagation rules to improve the bound. For arc consistency in particular, the method reduces to the known Virtual AC (VAC) algorithm. Newly, we implemented the method for singleton arc consistency (SAC) and compared it to other strong local consistencies in WCSPs on a public benchmark. The results show that the bounds obtained from SAC are superior for many instance groups.

Cite as

Tomáš Dlask, Tomáš Werner, and Simon de Givry. Bounds on Weighted CSPs Using Constraint Propagation and Super-Reparametrizations. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 23:1-23:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{dlask_et_al:LIPIcs.CP.2021.23,
  author =	{Dlask, Tom\'{a}\v{s} and Werner, Tom\'{a}\v{s} and de Givry, Simon},
  title =	{{Bounds on Weighted CSPs Using Constraint Propagation and Super-Reparametrizations}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{23:1--23:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.23},
  URN =		{urn:nbn:de:0030-drops-153149},
  doi =		{10.4230/LIPIcs.CP.2021.23},
  annote =	{Keywords: Weighted CSP, Super-Reparametrization, Linear Programming, Constraint Propagation}
}
Document
Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization

Authors: Johannes K. Fichte, Markus Hecher, and Valentin Roland


Abstract
Propositional model counting (MC) and its extensions as well as applications in the area of probabilistic reasoning have received renewed attention in recent years. As a result, also the need for quickly solving counting-based problems with automated solvers is critical for certain areas. In this paper, we present experiments evaluating various techniques in order to improve the performance of parallel model counting on general purpose graphics processing units (GPGPUs). Thereby, we mainly consider engineering efficient algorithms for model counting on GPGPUs that utilize the treewidth of a propositional formula by means of dynamic programming. The combination of our techniques results in the solver GPUSAT3, which is based on the programming framework Cuda that -compared to other frameworks- shows superior extensibility and driver support. When combining all findings of this work, we show that GPUSAT3 not only solves more instances of the recent Model Counting Competition 2020 (MCC 2020) than existing GPGPU-based systems, but also solves those significantly faster. A portfolio with one of the best solvers of MCC 2020 and GPUSAT3 solves 19% more instances than the former alone in less than half of the runtime.

Cite as

Johannes K. Fichte, Markus Hecher, and Valentin Roland. Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 24:1-24:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.CP.2021.24,
  author =	{Fichte, Johannes K. and Hecher, Markus and Roland, Valentin},
  title =	{{Parallel Model Counting with CUDA: Algorithm Engineering for Efficient Hardware Utilization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{24:1--24:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.24},
  URN =		{urn:nbn:de:0030-drops-153150},
  doi =		{10.4230/LIPIcs.CP.2021.24},
  annote =	{Keywords: Propositional Satisfiability, GPGPU, Model Counting, Treewidth, Tree Decomposition}
}
Document
Complications for Computational Experiments from Modern Processors

Authors: Johannes K. Fichte, Markus Hecher, Ciaran McCreesh, and Anas Shahab


Abstract
In this paper, we revisit the approach to empirical experiments for combinatorial solvers. We provide a brief survey on tools that can help to make empirical work easier. We illustrate origins of uncertainty in modern hardware and show how strong the influence of certain aspects of modern hardware and its experimental setup can be in an actual experimental evaluation. More specifically, there can be situations where (i) two different researchers run a reasonable-looking experiment comparing the same solvers and come to different conclusions and (ii) one researcher runs the same experiment twice on the same hardware and reaches different conclusions based upon how the hardware is configured and used. We investigate these situations from a hardware perspective. Furthermore, we provide an overview on standard measures, detailed explanations on effects, potential errors, and biased suggestions for useful tools. Alongside the tools, we discuss their feasibility as experiments often run on clusters to which the experimentalist has only limited access. Our work sheds light on a number of benchmarking-related issues which could be considered to be folklore or even myths.

Cite as

Johannes K. Fichte, Markus Hecher, Ciaran McCreesh, and Anas Shahab. Complications for Computational Experiments from Modern Processors. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 25:1-25:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{fichte_et_al:LIPIcs.CP.2021.25,
  author =	{Fichte, Johannes K. and Hecher, Markus and McCreesh, Ciaran and Shahab, Anas},
  title =	{{Complications for Computational Experiments from Modern Processors}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{25:1--25:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.25},
  URN =		{urn:nbn:de:0030-drops-153165},
  doi =		{10.4230/LIPIcs.CP.2021.25},
  annote =	{Keywords: Experimenting, Combinatorial Solving, Empirical Work}
}
Document
A Job Dispatcher for Large and Heterogeneous HPC Systems Running Modern Applications

Authors: Cristian Galleguillos, Zeynep Kiziltan, and Ricardo Soto


Abstract
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.

Cite as

Cristian Galleguillos, Zeynep Kiziltan, and Ricardo Soto. A Job Dispatcher for Large and Heterogeneous HPC Systems Running Modern Applications. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{galleguillos_et_al:LIPIcs.CP.2021.26,
  author =	{Galleguillos, Cristian and Kiziltan, Zeynep and Soto, Ricardo},
  title =	{{A Job Dispatcher for Large and Heterogeneous HPC Systems Running Modern Applications}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.26},
  URN =		{urn:nbn:de:0030-drops-153171},
  doi =		{10.4230/LIPIcs.CP.2021.26},
  annote =	{Keywords: Constraint programming, HPC systems, heterogeneous systems, large systems, on-line job dispatching, resource allocation}
}
Document
The Dungeon Variations Problem Using Constraint Programming

Authors: Gaël Glorian, Adrien Debesson, Sylvain Yvon-Paliot, and Laurent Simon


Abstract
The video games industry generates billions of dollars in sales every year. Video games can offer increasingly complex gaming experiences, with gigantic (but consistent) open worlds, thanks to larger and larger teams of developers and artists. In this paper, we propose a constraint-based approach for procedural dungeon generation in an open world/universe context, in order to provide players with consistent, open worlds with an excellent quality of storytelling. Thanks to a global description capturing all the possible rooms and situations of a given dungeon, our approach allows enumerating variations of this global pattern, which can then be presented to the player for more diversity. We formalise this problem in constraint programming by exploiting a graph abstraction of the dungeon pattern structure. Every path of the graph represents a possible variation matching a given set of constraints. We introduce a new propagator extending the "connected" graph constraint, which allows considering directed graphs with cycles. We show that thanks to this model and the proposed new propagator, it is possible to handle scenarios at the forefront of the game industry (AAA+ games). We demonstrate that our approach outperforms non-specialised solutions consisting of filtering only the relevant solutions a posteriori. We then conclude and offer several exciting perspectives raised by this approach to the Dungeon Variations Problem.

Cite as

Gaël Glorian, Adrien Debesson, Sylvain Yvon-Paliot, and Laurent Simon. The Dungeon Variations Problem Using Constraint Programming. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 27:1-27:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{glorian_et_al:LIPIcs.CP.2021.27,
  author =	{Glorian, Ga\"{e}l and Debesson, Adrien and Yvon-Paliot, Sylvain and Simon, Laurent},
  title =	{{The Dungeon Variations Problem Using Constraint Programming}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{27:1--27:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.27},
  URN =		{urn:nbn:de:0030-drops-153181},
  doi =		{10.4230/LIPIcs.CP.2021.27},
  annote =	{Keywords: constraint programming, video games, modelization, procedural generation}
}
Document
Refined Core Relaxation for Core-Guided MaxSAT Solving

Authors: Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo


Abstract
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.

Cite as

Hannes Ihalainen, Jeremias Berg, and Matti Järvisalo. Refined Core Relaxation for Core-Guided MaxSAT Solving. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 28:1-28:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.CP.2021.28,
  author =	{Ihalainen, Hannes and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Refined Core Relaxation for Core-Guided MaxSAT Solving}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{28:1--28:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.28},
  URN =		{urn:nbn:de:0030-drops-153197},
  doi =		{10.4230/LIPIcs.CP.2021.28},
  annote =	{Keywords: maximum satisfiability, MaxSAT, core-guided MaxSAT solving}
}
Document
A Linear Time Algorithm for the k-Cutset Constraint

Authors: Nicolas Isoart and Jean-Charles Régin


Abstract
In CP, the most efficient model solving the TSP is the Weighted Circuit Constraint (WCC) combined with the k-cutset constraint. The WCC is mainly based on the edges cost of a given graph whereas the k-cutset constraint is a structural constraint. Specifically, for each cutset in a graph, the k-cutset constraint imposes that the size of the cutset is greater than or equal to two. In addition, any solution contains an even number of elements from this cutset. Isoart and Régin introduced an algorithm for this constraint. Unfortunately, their approach leads to a time complexity growing with the size of the considered cutsets, i.e. with k. Thus, they introduced an algorithm with a quadratic complexity dealing with k lower or equal to three. In this paper, we introduce a linear time algorithm for any k based on a DFS checking the consistency of this constraint and performing its filtering. Experimental results show that the size of most of the k-cutsets is lower or equal than 3. In addition, since the time complexity is improved, our algorithm also improves the solving times.

Cite as

Nicolas Isoart and Jean-Charles Régin. A Linear Time Algorithm for the k-Cutset Constraint. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 29:1-29:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{isoart_et_al:LIPIcs.CP.2021.29,
  author =	{Isoart, Nicolas and R\'{e}gin, Jean-Charles},
  title =	{{A Linear Time Algorithm for the k-Cutset Constraint}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{29:1--29:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.29},
  URN =		{urn:nbn:de:0030-drops-153200},
  doi =		{10.4230/LIPIcs.CP.2021.29},
  annote =	{Keywords: k-Cutset, TSP, Linear algorithm, Constraint}
}
Document
A k-Opt Based Constraint for the TSP

Authors: Nicolas Isoart and Jean-Charles Régin


Abstract
The LKH algorithm based on k-opt is an extremely efficient algorithm solving the TSP. Given a non-optimal tour in a graph, the idea of k-opt is to iteratively swap k edges of this tour in order to find a shorter tour. However, the optimality of a tour cannot be proved with this method. In that case, exact solving methods such as CP can be used. The CP model is based on a graph variable with mandatory and optional edges. Through branch-and-bound and filtering algorithms, the set of mandatory edges will be modified. In this paper, we introduce a new constraint to the CP model named mandatory Hamiltonian path constraint searching for k-opt in the mandatory Hamiltonian paths. Experiments have shown that the mandatory Hamiltonian path constraint allows us to gain on average a factor of 3 on the solving time. In addition, we have been able to solve some instances that remain unsolved with the state of the art CP solver with a 1 week time out.

Cite as

Nicolas Isoart and Jean-Charles Régin. A k-Opt Based Constraint for the TSP. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 30:1-30:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{isoart_et_al:LIPIcs.CP.2021.30,
  author =	{Isoart, Nicolas and R\'{e}gin, Jean-Charles},
  title =	{{A k-Opt Based Constraint for the TSP}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{30:1--30:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.30},
  URN =		{urn:nbn:de:0030-drops-153212},
  doi =		{10.4230/LIPIcs.CP.2021.30},
  annote =	{Keywords: TSP, k-opt, 1-tree, Constraint}
}
Document
The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets

Authors: Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho


Abstract
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.

Cite as

Mikoláš Janota, António Morgado, José Fragoso Santos, and Vasco Manquinho. The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 31:1-31:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{janota_et_al:LIPIcs.CP.2021.31,
  author =	{Janota, Mikol\'{a}\v{s} and Morgado, Ant\'{o}nio and Fragoso Santos, Jos\'{e} and Manquinho, Vasco},
  title =	{{The Seesaw Algorithm: Function Optimization Using Implicit Hitting Sets}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.31},
  URN =		{urn:nbn:de:0030-drops-153220},
  doi =		{10.4230/LIPIcs.CP.2021.31},
  annote =	{Keywords: implicit hitting sets, minimal hitting set, MaxSAT, optimization}
}
Document
Reasoning Short Cuts in Infinite Domain Constraint Satisfaction: Algorithms and Lower Bounds for Backdoors

Authors: Peter Jonsson, Victor Lagerkvist, and Sebastian Ordyniak


Abstract
A backdoor in a finite-domain CSP instance is a set of variables where each possible instantiation moves the instance into a polynomial-time solvable class. Backdoors have found many applications in artificial intelligence and elsewhere, and the algorithmic problem of finding such backdoors has consequently been intensively studied. Sioutis and Janhunen (KI, 2019) have proposed a generalised backdoor concept suitable for infinite-domain CSP instances over binary constraints. We generalise their concept into a large class of CSPs that allow for higher-arity constraints. We show that this kind of infinite-domain backdoors have many of the positive computational properties that finite-domain backdoors have: the associated computational problems are fixed-parameter tractable whenever the underlying constraint language is finite. On the other hand, we show that infinite languages make the problems considerably harder.

Cite as

Peter Jonsson, Victor Lagerkvist, and Sebastian Ordyniak. Reasoning Short Cuts in Infinite Domain Constraint Satisfaction: Algorithms and Lower Bounds for Backdoors. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 32:1-32:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{jonsson_et_al:LIPIcs.CP.2021.32,
  author =	{Jonsson, Peter and Lagerkvist, Victor and Ordyniak, Sebastian},
  title =	{{Reasoning Short Cuts in Infinite Domain Constraint Satisfaction: Algorithms and Lower Bounds for Backdoors}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{32:1--32:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.32},
  URN =		{urn:nbn:de:0030-drops-153238},
  doi =		{10.4230/LIPIcs.CP.2021.32},
  annote =	{Keywords: Constraint Satisfaction Problems, Parameterised Complexity, Backdoors}
}
Document
Learning TSP Requires Rethinking Generalization

Authors: Chaitanya K. Joshi, Quentin Cappart, Louis-Martin Rousseau, and Thomas Laurent


Abstract
End-to-end training of neural network solvers for combinatorial optimization problems such as the Travelling Salesman Problem is intractable and inefficient beyond a few hundreds of nodes. While state-of-the-art Machine Learning approaches perform closely to classical solvers when trained on trivially small sizes, they are unable to generalize the learnt policy to larger instances of practical scales. Towards leveraging transfer learning to solve large-scale TSPs, this paper identifies inductive biases, model architectures and learning algorithms that promote generalization to instances larger than those seen in training. Our controlled experiments provide the first principled investigation into such zero-shot generalization, revealing that extrapolating beyond training data requires rethinking the neural combinatorial optimization pipeline, from network layers and learning paradigms to evaluation protocols.

Cite as

Chaitanya K. Joshi, Quentin Cappart, Louis-Martin Rousseau, and Thomas Laurent. Learning TSP Requires Rethinking Generalization. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 33:1-33:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{joshi_et_al:LIPIcs.CP.2021.33,
  author =	{Joshi, Chaitanya K. and Cappart, Quentin and Rousseau, Louis-Martin and Laurent, Thomas},
  title =	{{Learning TSP Requires Rethinking Generalization}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{33:1--33:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.33},
  URN =		{urn:nbn:de:0030-drops-153248},
  doi =		{10.4230/LIPIcs.CP.2021.33},
  annote =	{Keywords: Combinatorial Optimization, Travelling Salesman Problem, Graph Neural Networks, Deep Learning}
}
Document
SAT Modulo Symmetries for Graph Generation

Authors: Markus Kirchweger and Stefan Szeider


Abstract
We propose a novel constraint-based approach to graph generation. Our approach utilizes the interaction between a CDCL SAT solver and a special symmetry propagator where the SAT solver runs on an encoding of the desired graph property. The symmetry propagator checks partially generated graphs for minimality w.r.t. a lexicographic ordering during the solving process. This approach has several advantages over a static symmetry breaking: (i) symmetries are detected early in the generation process, (ii) symmetry breaking is seamlessly integrated into the CDCL procedure, and (iii) the propagator can perform a complete symmetry breaking without causing a prohibitively large initial encoding. We instantiate our approach by generating extremal graphs with certain restrictions in terms of girth and diameter. With our approach, we could confirm the Simon-Murty Conjecture (1979) on diameter-2-critical graphs for graphs up to 18 vertices.

Cite as

Markus Kirchweger and Stefan Szeider. SAT Modulo Symmetries for Graph Generation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 34:1-34:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.CP.2021.34,
  author =	{Kirchweger, Markus and Szeider, Stefan},
  title =	{{SAT Modulo Symmetries for Graph Generation}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{34:1--34:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.34},
  URN =		{urn:nbn:de:0030-drops-153257},
  doi =		{10.4230/LIPIcs.CP.2021.34},
  annote =	{Keywords: symmetry breaking, SAT encodings, graph generation, combinatorial search, extremal graphs, CDCL}
}
Document
Counterfactual Explanations via Inverse Constraint Programming

Authors: Anton Korikov and J. Christopher Beck


Abstract
It is increasingly recognized that automated decision making systems cannot be black boxes: users require insight into the reasons that decisions are made. Explainable AI (XAI) has developed a number of approaches to this challenge, including the framework of counterfactual explanations where an explanation takes the form of the minimal change to the world required for a user’s desired decisions to be made. Building on recent work, we show that for a user query specifying an assignment to a subset of variables, a counterfactual explanation can be found using inverse optimization. Thus, we develop inverse constraint programming (CP): to our knowledge, the first definition and treatment of inverse optimization in constraint programming. We modify a cutting plane algorithm for inverse mixed-integer programming (MIP), resulting in both pure and hybrid inverse CP algorithms. We evaluate the performance of these algorithms in generating counterfactual explanations for two combinatorial optimization problems: the 0-1 knapsack problem and single machine scheduling with release dates. Our numerical experiments show that a MIP-CP hybrid approach extended with a novel early stopping criteria can substantially out-perform a MIP approach particularly when CP is the state of the art for the underlying optimization problem.

Cite as

Anton Korikov and J. Christopher Beck. Counterfactual Explanations via Inverse Constraint Programming. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 35:1-35:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{korikov_et_al:LIPIcs.CP.2021.35,
  author =	{Korikov, Anton and Beck, J. Christopher},
  title =	{{Counterfactual Explanations via Inverse Constraint Programming}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{35:1--35:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.35},
  URN =		{urn:nbn:de:0030-drops-153261},
  doi =		{10.4230/LIPIcs.CP.2021.35},
  annote =	{Keywords: Explanation, Inverse Optimization, Scheduling}
}
Document
Utilizing Constraint Optimization for Industrial Machine Workload Balancing

Authors: Benjamin Kovács, Pierre Tassel, Wolfgang Kohlenbrein, Philipp Schrott-Kostwein, and Martin Gebser


Abstract
Efficient production scheduling is an important application area of constraint-based optimization techniques. Problem domains like flow- and job-shop scheduling have been extensive study targets, and solving approaches range from complete and local search to machine learning methods. In this paper, we devise and compare constraint-based optimization techniques for scheduling specialized manufacturing processes in the build-to-print business. The goal is to allocate production equipment such that customer orders are completed in time as good as possible, while respecting machine capacities and minimizing extra shifts required to resolve bottlenecks. To this end, we furnish several approaches for scheduling pending production tasks to one or more workdays for performing them. First, we propose a greedy custom algorithm that allows for quickly screening the effects of altering resource demands and availabilities. Moreover, we take advantage of such greedy solutions to parameterize and warm-start the optimization performed by integer linear programming (ILP) and constraint programming (CP) solvers on corresponding problem formulations. Our empirical evaluation is based on production data by Kostwein Holding GmbH, a worldwide supplier in the build-to-print business, and thus demonstrates the industrial applicability of our scheduling methods. We also present a user-friendly web interface for feeding the underlying solvers with customer order and equipment data, graphically displaying computed schedules, and facilitating the investigation of changed resource demands and availabilities, e.g., due to updating orders or including extra shifts.

Cite as

Benjamin Kovács, Pierre Tassel, Wolfgang Kohlenbrein, Philipp Schrott-Kostwein, and Martin Gebser. Utilizing Constraint Optimization for Industrial Machine Workload Balancing. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 36:1-36:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{kovacs_et_al:LIPIcs.CP.2021.36,
  author =	{Kov\'{a}cs, Benjamin and Tassel, Pierre and Kohlenbrein, Wolfgang and Schrott-Kostwein, Philipp and Gebser, Martin},
  title =	{{Utilizing Constraint Optimization for Industrial Machine Workload Balancing}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{36:1--36:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.36},
  URN =		{urn:nbn:de:0030-drops-153276},
  doi =		{10.4230/LIPIcs.CP.2021.36},
  annote =	{Keywords: application, production planning, production scheduling, linear programming, constraint programming, greedy algorithm, benchmarking}
}
Document
Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem

Authors: Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter


Abstract
We introduce the Oven Scheduling Problem (OSP), a new parallel batch scheduling problem that arises in the area of electronic component manufacturing. Jobs need to be scheduled to one of several ovens and may be processed simultaneously in one batch if they have compatible requirements. The scheduling of jobs must respect several constraints concerning eligibility and availability of ovens, release dates of jobs, setup times between batches as well as oven capacities. Running the ovens is highly energy-intensive and thus the main objective, besides finishing jobs on time, is to minimize the cumulative batch processing time across all ovens. This objective distinguishes the OSP from other batch processing problems which typically minimize objectives related to makespan, tardiness or lateness. We propose to solve this NP-hard scheduling problem via constraint programming (CP) and integer linear programming (ILP) and present corresponding CP- and ILP-models. For an experimental evaluation, we introduce a multi-parameter random instance generator to provide a diverse set of problem instances. Using state-of-the-art solvers, we evaluate the quality and compare the performance of our CP- and ILP-models, which could find optimal solutions for many instances. Furthermore, using our models we are able to provide upper bounds for the whole benchmark set including large-scale instances.

Cite as

Marie-Louise Lackner, Christoph Mrkvicka, Nysret Musliu, Daniel Walkiewicz, and Felix Winter. Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 37:1-37:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{lackner_et_al:LIPIcs.CP.2021.37,
  author =	{Lackner, Marie-Louise and Mrkvicka, Christoph and Musliu, Nysret and Walkiewicz, Daniel and Winter, Felix},
  title =	{{Minimizing Cumulative Batch Processing Time for an Industrial Oven Scheduling Problem}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{37:1--37:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.37},
  URN =		{urn:nbn:de:0030-drops-153286},
  doi =		{10.4230/LIPIcs.CP.2021.37},
  annote =	{Keywords: Oven Scheduling Problem, Parallel Batch Processing, Constraint Programming, Integer Linear Programming}
}
Document
Combining Clause Learning and Branch and Bound for MaxSAT

Authors: Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He


Abstract
Branch and Bound (BnB) is a powerful technique that has been successfully used to solve many combinatorial optimization problems. However, MaxSAT is a notorious exception because BnB MaxSAT solvers perform poorly on many instances encoding interesting real-world and academic optimization problems. This has formed a prevailing opinion in the community stating that BnB is not so useful for MaxSAT, except for random and some special crafted instances. In fact, there has been no advance allowing to significantly speed up BnB MaxSAT solvers in the past few years, as illustrated by the absence of BnB solvers in the annual MaxSAT Evaluation since 2017. Our work aims to change this situation and proposes a new BnB MaxSAT solver, called MaxCDCL, by combining clause learning and an efficient bounding procedure. The experimental results show that, contrary to the prevailing opinion, BnB can be competitive for MaxSAT. MaxCDCL is ranked among the top 5 solvers of the 15 solvers that participated in the 2020 MaxSAT Evaluation, solving a number of instances that other solvers cannot solve. Furthermore, MaxCDCL, when combined with the best existing solvers, solves the highest number of instances of the MaxSAT Evaluations.

Cite as

Chu-Min Li, Zhenxing Xu, Jordi Coll, Felip Manyà, Djamal Habet, and Kun He. Combining Clause Learning and Branch and Bound for MaxSAT. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 38:1-38:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CP.2021.38,
  author =	{Li, Chu-Min and Xu, Zhenxing and Coll, Jordi and Many\`{a}, Felip and Habet, Djamal and He, Kun},
  title =	{{Combining Clause Learning and Branch and Bound for MaxSAT}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{38:1--38:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.38},
  URN =		{urn:nbn:de:0030-drops-153291},
  doi =		{10.4230/LIPIcs.CP.2021.38},
  annote =	{Keywords: MaxSAT, Branch\&Bound, CDCL}
}
Document
Improving Local Search for Minimum Weighted Connected Dominating Set Problem by Inner-Layer Local Search

Authors: Bohan Li, Kai Wang, Yiyuan Wang, and Shaowei Cai


Abstract
The minimum weighted connected dominating set (MWCDS) problem is an important variant of connected dominating set problems with wide applications, especially in heterogenous networks and gene regulatory networks. In the paper, we develop a nested local search algorithm called NestedLS for solving MWCDS on classic benchmarks and massive graphs. In this local search framework, we propose two novel ideas to make it effective by utilizing previous search information. First, we design the restart based smoothing mechanism as a diversification method to escape from local optimal. Second, we propose a novel inner-layer local search method to enlarge the candidate removal set, which can be modelled as an optimized version of spanning tree problem. Moreover, inner-layer local search method is a general method for maintaining the connectivity constraint when dealing with massive graphs. Experimental results show that NestedLS outperforms state-of-the-art meta-heuristic algorithms on most instances.

Cite as

Bohan Li, Kai Wang, Yiyuan Wang, and Shaowei Cai. Improving Local Search for Minimum Weighted Connected Dominating Set Problem by Inner-Layer Local Search. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 39:1-39:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.CP.2021.39,
  author =	{Li, Bohan and Wang, Kai and Wang, Yiyuan and Cai, Shaowei},
  title =	{{Improving Local Search for Minimum Weighted Connected Dominating Set Problem by Inner-Layer Local Search}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{39:1--39:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.39},
  URN =		{urn:nbn:de:0030-drops-153304},
  doi =		{10.4230/LIPIcs.CP.2021.39},
  annote =	{Keywords: Operations Research, NP-hard Problem, Local Search, Weighted Connected Dominating Set Problem}
}
Document
Automatic Generation of Declarative Models For Differential Cryptanalysis

Authors: Luc Libralesso, François Delobel, Pascal Lafourcade, and Christine Solnon


Abstract
When designing a new symmetric block cipher, it is necessary to evaluate its robustness against differential attacks. This is done by computing Truncated Differential Characteristics (TDCs) that provide bounds on the complexity of these attacks. TDCs are often computed by using declarative approaches such as CP (Constraint Programming), SAT, or ILP (Integer Linear Programming). However, designing accurate and efficient models for these solvers is a difficult, error-prone and time-consuming task, and it requires advanced skills on both symmetric cryptography and solvers. In this paper, we describe a tool for automatically generating these models, called Tagada (Tool for Automatic Generation of Abstraction-based Differential Attacks). The input of Tagada is an operational description of the cipher by means of black-box operators and bipartite Directed Acyclic Graphs (DAGs). Given this description, we show how to automatically generate constraints that model operator semantics, and how to generate MiniZinc models. We experimentally evaluate our approach on two different kinds of differential attacks (e.g., single-key and related-key) and four different symmetric block ciphers (e.g., the AES (Advanced Encryption Standard), Craft, Midori, and Skinny). We show that our automatically generated models are competitive with state-of-the-art approaches. These automatically generated models constitute a new benchmark composed of eight optimization problems and eight enumeration problems, with instances of increasing size in each problem. We experimentally compare CP, SAT, and ILP solvers on this new benchmark.

Cite as

Luc Libralesso, François Delobel, Pascal Lafourcade, and Christine Solnon. Automatic Generation of Declarative Models For Differential Cryptanalysis. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 40:1-40:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{libralesso_et_al:LIPIcs.CP.2021.40,
  author =	{Libralesso, Luc and Delobel, Fran\c{c}ois and Lafourcade, Pascal and Solnon, Christine},
  title =	{{Automatic Generation of Declarative Models For Differential Cryptanalysis}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{40:1--40:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.40},
  URN =		{urn:nbn:de:0030-drops-153314},
  doi =		{10.4230/LIPIcs.CP.2021.40},
  annote =	{Keywords: Constraint Programming, SAT, ILP, Differential Cryptanalysis}
}
Document
A Bound-Independent Pruning Technique to Speeding up Tree-Based Complete Search Algorithms for Distributed Constraint Optimization Problems

Authors: Xiangshuang Liu, Ziyu Chen, Dingding Chen, and Junsong Gao


Abstract
Complete search algorithms are important methods for solving Distributed Constraint Optimization Problems (DCOPs), which generally utilize bounds to prune the search space. However, obtaining high-quality lower bounds is quite expensive since it requires each agent to collect more information aside from its local knowledge, which would cause tremendous traffic overheads. Instead of bothering for bounds, we propose a Bound-Independent Pruning (BIP) technique for existing tree-based complete search algorithms, which can independently reduce the search space only by exploiting local knowledge. Specifically, BIP enables each agent to determine a subspace containing the optimal solution only from its local constraints along with running contexts, which can be further exploited by any search strategies. Furthermore, we present an acceptability testing mechanism to tailor existing tree-based complete search algorithms to search the remaining space returned by BIP when they hold inconsistent contexts. Finally, we prove the correctness of our technique and the experimental results show that BIP can significantly speed up state-of-the-art tree-based complete search algorithms on various standard benchmarks.

Cite as

Xiangshuang Liu, Ziyu Chen, Dingding Chen, and Junsong Gao. A Bound-Independent Pruning Technique to Speeding up Tree-Based Complete Search Algorithms for Distributed Constraint Optimization Problems. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 41:1-41:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{liu_et_al:LIPIcs.CP.2021.41,
  author =	{Liu, Xiangshuang and Chen, Ziyu and Chen, Dingding and Gao, Junsong},
  title =	{{A Bound-Independent Pruning Technique to Speeding up Tree-Based Complete Search Algorithms for Distributed Constraint Optimization Problems}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{41:1--41:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.41},
  URN =		{urn:nbn:de:0030-drops-153324},
  doi =		{10.4230/LIPIcs.CP.2021.41},
  annote =	{Keywords: DCOP, complete algorithms, search}
}
Document
Data Driven VRP: A Neural Network Model to Learn Hidden Preferences for VRP

Authors: Jayanta Mandi, Rocsildes Canoy, Víctor Bucarey, and Tias Guns


Abstract
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.

Cite as

Jayanta Mandi, Rocsildes Canoy, Víctor Bucarey, and Tias Guns. Data Driven VRP: A Neural Network Model to Learn Hidden Preferences for VRP. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 42:1-42:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{mandi_et_al:LIPIcs.CP.2021.42,
  author =	{Mandi, Jayanta and Canoy, Rocsildes and Bucarey, V{\'\i}ctor and Guns, Tias},
  title =	{{Data Driven VRP: A Neural Network Model to Learn Hidden Preferences for VRP}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{42:1--42:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.42},
  URN =		{urn:nbn:de:0030-drops-153339},
  doi =		{10.4230/LIPIcs.CP.2021.42},
  annote =	{Keywords: Vehicle routing, Neural network, Preference learning}
}
Document
Statistical Comparison of Algorithm Performance Through Instance Selection

Authors: Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos


Abstract
Empirical performance evaluations, in competitions and scientific publications, play a major role in improving the state of the art in solving many automated reasoning problems, including SAT, CSP and Bayesian network structure learning (BNSL). To empirically demonstrate the merit of a new solver usually requires extensive experiments, with computational costs of CPU years. This not only makes it difficult for researchers with limited access to computational resources to test their ideas and publish their work, but also consumes large amounts of energy. We propose an approach for comparing the performance of two algorithms: by performing runs on carefully chosen instances, we obtain a probabilistic statement on which algorithm performs best, trading off between the computational cost of running algorithms and the confidence in the result. We describe a set of methods for this purpose and evaluate their efficacy on diverse datasets from SAT, CSP and BNSL. On all these datasets, most of our approaches were able to choose the correct algorithm with about 95% accuracy, while using less than a third of the CPU time required for a full comparison; the best methods reach this level of accuracy within less than 15% of the CPU time for a full comparison.

Cite as

Théo Matricon, Marie Anastacio, Nathanaël Fijalkow, Laurent Simon, and Holger H. Hoos. Statistical Comparison of Algorithm Performance Through Instance Selection. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 43:1-43:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{matricon_et_al:LIPIcs.CP.2021.43,
  author =	{Matricon, Th\'{e}o and Anastacio, Marie and Fijalkow, Nathana\"{e}l and Simon, Laurent and Hoos, Holger H.},
  title =	{{Statistical Comparison of Algorithm Performance Through Instance Selection}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{43:1--43:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.43},
  URN =		{urn:nbn:de:0030-drops-153346},
  doi =		{10.4230/LIPIcs.CP.2021.43},
  annote =	{Keywords: Performance assessment, early stopping, automated reasoning solvers}
}
Document
Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights

Authors: Andreas Niskanen, Jeremias Berg, and Matti Järvisalo


Abstract
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.

Cite as

Andreas Niskanen, Jeremias Berg, and Matti Järvisalo. Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 44:1-44:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{niskanen_et_al:LIPIcs.CP.2021.44,
  author =	{Niskanen, Andreas and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Enabling Incrementality in the Implicit Hitting Set Approach to MaxSAT Under Changing Weights}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{44:1--44:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.44},
  URN =		{urn:nbn:de:0030-drops-153354},
  doi =		{10.4230/LIPIcs.CP.2021.44},
  annote =	{Keywords: Constraint optimization, maximum satisfiability, MaxSAT, implicit hitting set approach}
}
Document
Solving the Non-Crossing MAPF with CP

Authors: Xiao Peng, Christine Solnon, and Olivier Simonin


Abstract
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.

Cite as

Xiao Peng, Christine Solnon, and Olivier Simonin. Solving the Non-Crossing MAPF with CP. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 45:1-45:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{peng_et_al:LIPIcs.CP.2021.45,
  author =	{Peng, Xiao and Solnon, Christine and Simonin, Olivier},
  title =	{{Solving the Non-Crossing MAPF with CP}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{45:1--45:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.45},
  URN =		{urn:nbn:de:0030-drops-153367},
  doi =		{10.4230/LIPIcs.CP.2021.45},
  annote =	{Keywords: Constraint Programming (CP), Multi-Agent Path Finding (MAPF), Assignment Problems}
}
Document
Positive and Negative Length-Bound Reachability Constraints

Authors: Luis Quesada and Kenneth N. Brown


Abstract
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.

Cite as

Luis Quesada and Kenneth N. Brown. Positive and Negative Length-Bound Reachability Constraints. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 46:1-46:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{quesada_et_al:LIPIcs.CP.2021.46,
  author =	{Quesada, Luis and Brown, Kenneth N.},
  title =	{{Positive and Negative Length-Bound Reachability Constraints}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{46:1--46:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.46},
  URN =		{urn:nbn:de:0030-drops-153372},
  doi =		{10.4230/LIPIcs.CP.2021.46},
  annote =	{Keywords: Reachability Constraints, Graph Connectivity, Constraint Programming}
}
Document
Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms

Authors: Alexander Semenov, Daniil Chivilikhin, Artem Pavlenko, Ilya Otpuschennikov, Vladimir Ulyantsev, and Alexey Ignatiev


Abstract
Propositional satisfiability (SAT) solvers are deemed to be among the most efficient reasoners, which have been successfully used in a wide range of practical applications. As this contrasts the well-known NP-completeness of SAT, a number of attempts have been made in the recent past to assess the hardness of propositional formulas in conjunctive normal form (CNF). The present paper proposes a CNF formula hardness measure which is close in conceptual meaning to the one based on Backdoor set notion: in both cases some subset B of variables in a CNF formula is used to define the hardness of the formula w.r.t. this set. In contrast to the backdoor measure, the new measure does not demand the polynomial decidability of CNF formulas obtained when substituting assignments of variables from B to the original formula. To estimate this measure the paper suggests an adaptive (ε,δ)-approximation probabilistic algorithm. The problem of looking for the subset of variables which provides the minimal hardness value is reduced to optimization of a pseudo-Boolean black-box function. We apply evolutionary algorithms to this problem and demonstrate applicability of proposed notions and techniques to tests from several families of unsatisfiable CNF formulas.

Cite as

Alexander Semenov, Daniil Chivilikhin, Artem Pavlenko, Ilya Otpuschennikov, Vladimir Ulyantsev, and Alexey Ignatiev. Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 47:1-47:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{semenov_et_al:LIPIcs.CP.2021.47,
  author =	{Semenov, Alexander and Chivilikhin, Daniil and Pavlenko, Artem and Otpuschennikov, Ilya and Ulyantsev, Vladimir and Ignatiev, Alexey},
  title =	{{Evaluating the Hardness of SAT Instances Using Evolutionary Optimization Algorithms}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{47:1--47:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.47},
  URN =		{urn:nbn:de:0030-drops-153381},
  doi =		{10.4230/LIPIcs.CP.2021.47},
  annote =	{Keywords: SAT solving, Boolean formula hardness, Backdoors, Evolutionary algorithms}
}
Document
Optimising Training for Service Delivery

Authors: Ilankaikone Senthooran, Pierre Le Bodic, and Peter J. Stuckey


Abstract
We study the problem of training a roster of engineers, who are scheduled to respond to service calls that require a set of skills, and where engineers and calls have different locations. Both training an engineer in a skill and sending an engineer to respond a non-local service call incur a cost. Alternatively, a local contractor can be hired. The problem consists in training engineers in skills so that the quality of service (i.e. response time) is maximised and costs are minimised. The problem is hard to solve in practice partly because (1) the value of training an engineer in one skill depends on other training decisions, (2) evaluating training decisions means evaluating the schedules that are now made possible by the new skills, and (3) these schedules must be computed over a long time horizon, otherwise training may not pay off. We show that a monolithic approach to this problem is not practical. Instead, we decompose it into three subproblems, modelled with MiniZinc. This allows us to pick the approach that works best for each subproblem (MIP or CP) and provide good solutions to the problem. Data is provided by a multinational company.

Cite as

Ilankaikone Senthooran, Pierre Le Bodic, and Peter J. Stuckey. Optimising Training for Service Delivery. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 48:1-48:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{senthooran_et_al:LIPIcs.CP.2021.48,
  author =	{Senthooran, Ilankaikone and Le Bodic, Pierre and Stuckey, Peter J.},
  title =	{{Optimising Training for Service Delivery}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{48:1--48:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.48},
  URN =		{urn:nbn:de:0030-drops-153395},
  doi =		{10.4230/LIPIcs.CP.2021.48},
  annote =	{Keywords: Scheduling, Task Allocation, Training Optimisation}
}
Document
Human-Centred Feasibility Restoration

Authors: Ilankaikone Senthooran, Matthias Klapperstueck, Gleb Belov, Tobias Czauderna, Kevin Leo, Mark Wallace, Michael Wybrow, and Maria Garcia de la Banda


Abstract
Decision systems for solving real-world combinatorial problems must be able to report infeasibility in such a way that users can understand the reasons behind it, and understand how to modify the problem to restore feasibility. Current methods mainly focus on reporting one or more subsets of the problem constraints that cause infeasibility. Methods that also show users how to restore feasibility tend to be less flexible and/or problem-dependent. We describe a problem-independent approach to feasibility restoration that combines existing techniques from the literature in novel ways to yield meaningful, useful, practical and flexible user support. We evaluate the resulting framework on two real-world applications.

Cite as

Ilankaikone Senthooran, Matthias Klapperstueck, Gleb Belov, Tobias Czauderna, Kevin Leo, Mark Wallace, Michael Wybrow, and Maria Garcia de la Banda. Human-Centred Feasibility Restoration. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 49:1-49:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{senthooran_et_al:LIPIcs.CP.2021.49,
  author =	{Senthooran, Ilankaikone and Klapperstueck, Matthias and Belov, Gleb and Czauderna, Tobias and Leo, Kevin and Wallace, Mark and Wybrow, Michael and de la Banda, Maria Garcia},
  title =	{{Human-Centred Feasibility Restoration}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{49:1--49:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.49},
  URN =		{urn:nbn:de:0030-drops-153408},
  doi =		{10.4230/LIPIcs.CP.2021.49},
  annote =	{Keywords: Combinatorial optimisation, modelling, human-centred, conflict resolution, feasibility restoration, explainable AI, soft constraints}
}
Document
SAT-Based Approach for Learning Optimal Decision Trees with Non-Binary Features

Authors: Pouya Shati, Eldan Cohen, and Sheila McIlraith


Abstract
Decision trees are a popular classification model in machine learning due to their interpretability and performance. Traditionally, decision-tree classifiers are constructed using greedy heuristic algorithms, however these algorithms do not provide guarantees on the quality of the resultant trees. Instead, a recent line of work has studied the use of exact optimization approaches for constructing optimal decision trees. Most of the recent approaches that employ exact optimization are designed for datasets with binary features. While numeric and categorical features can be transformed to binary features, this transformation can introduce a large number of binary features and may not be efficient in practice. In this work, we present a novel SAT-based encoding for decision trees that supports non-binary features and demonstrate how it can be used to solve two well-studied variants of the optimal decision tree problem. We perform an extensive empirical analysis that shows our approach obtains superior performance and is often an order of magnitude faster than the current state-of-the-art exact techniques on non-binary datasets.

Cite as

Pouya Shati, Eldan Cohen, and Sheila McIlraith. SAT-Based Approach for Learning Optimal Decision Trees with Non-Binary Features. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 50:1-50:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{shati_et_al:LIPIcs.CP.2021.50,
  author =	{Shati, Pouya and Cohen, Eldan and McIlraith, Sheila},
  title =	{{SAT-Based Approach for Learning Optimal Decision Trees with Non-Binary Features}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{50:1--50:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.50},
  URN =		{urn:nbn:de:0030-drops-153416},
  doi =		{10.4230/LIPIcs.CP.2021.50},
  annote =	{Keywords: Decision Tree, Classification, Numeric Data, Categorical Data, SAT, MaxSAT}
}
Document
Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Pavel Smirnov, Jeremias Berg, and Matti Järvisalo


Abstract
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.

Cite as

Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Pseudo-Boolean Optimization by Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{smirnov_et_al:LIPIcs.CP.2021.51,
  author =	{Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.51},
  URN =		{urn:nbn:de:0030-drops-153429},
  doi =		{10.4230/LIPIcs.CP.2021.51},
  annote =	{Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets}
}
Document
An Algorithm-Independent Measure of Progress for Linear Constraint Propagation

Authors: Boro Sofranac, Ambros Gleixner, and Sebastian Pokutta


Abstract
Propagation of linear constraints has become a crucial sub-routine in modern Mixed-Integer Programming (MIP) solvers. In practice, iterative algorithms with tolerance-based stopping criteria are used to avoid problems with slow or infinite convergence. However, these heuristic stopping criteria can pose difficulties for fairly comparing the efficiency of different implementations of iterative propagation algorithms in a real-world setting. Most significantly, the presence of unbounded variable domains in the problem formulation makes it difficult to quantify the relative size of reductions performed on them. In this work, we develop a method to measure - independently of the algorithmic design - the progress that a given iterative propagation procedure has made at a given point in time during its execution. Our measure makes it possible to study and better compare the behavior of bounds propagation algorithms for linear constraints. We apply the new measure to answer two questions of practical relevance: (i) We investigate to what extent heuristic stopping criteria can lead to premature termination on real-world MIP instances. (ii) We compare a GPU-parallel propagation algorithm against a sequential state-of-the-art implementation and show that the parallel version is even more competitive in a real-world setting than originally reported.

Cite as

Boro Sofranac, Ambros Gleixner, and Sebastian Pokutta. An Algorithm-Independent Measure of Progress for Linear Constraint Propagation. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 52:1-52:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{sofranac_et_al:LIPIcs.CP.2021.52,
  author =	{Sofranac, Boro and Gleixner, Ambros and Pokutta, Sebastian},
  title =	{{An Algorithm-Independent Measure of Progress for Linear Constraint Propagation}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{52:1--52:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.52},
  URN =		{urn:nbn:de:0030-drops-153430},
  doi =		{10.4230/LIPIcs.CP.2021.52},
  annote =	{Keywords: Bounds Propagation, Mixed Integer Programming}
}
Document
Differential Programming via OR Methods

Authors: Shannon Sweitzer and T. K. Satish Kumar


Abstract
Systems of ordinary differential equations (ODEs) and partial differential equations (PDEs) are extensively used in many fields of science, including physics, biochemistry, nonlinear control, and dynamical systems. On the one hand, analytical methods for solving systems of ODEs/PDEs mostly remain an art and are largely insufficient for complex systems. On the other hand, numerical approximation methods do not yield a viable analytical form of the solution that is often required for downstream tasks. In this paper, we present an approximate approach for solving systems of ODEs/PDEs analytically using solvers like Gurobi developed in Operations Research (OR). Our main idea is to represent entire functions as Bézier curves/surfaces with to-be-determined control points. The ODEs/PDEs as well as their boundary conditions can then be reformulated as constraints on these control points. In many cases, this reformulation yields quadratic programming problems (QPPs) that can be solved in polynomial time. It also allows us to reason about inequalities. We demonstrate the success of our approach on several interesting classes of ODEs/PDEs.

Cite as

Shannon Sweitzer and T. K. Satish Kumar. Differential Programming via OR Methods. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 53:1-53:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{sweitzer_et_al:LIPIcs.CP.2021.53,
  author =	{Sweitzer, Shannon and Kumar, T. K. Satish},
  title =	{{Differential Programming via OR Methods}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{53:1--53:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.53},
  URN =		{urn:nbn:de:0030-drops-153445},
  doi =		{10.4230/LIPIcs.CP.2021.53},
  annote =	{Keywords: Differential Programming, Operations Research, B\'{e}zier Curves}
}
Document
Learning Max-CSPs via Active Constraint Acquisition

Authors: Dimosthenis C. Tsouros and Kostas Stergiou


Abstract
Constraint acquisition can assist non-expert users to model their problems as constraint networks. In active constraint acquisition, this is achieved through an interaction between the learner, who posts examples, and the user who classifies them as solutions or not. Although there has been recent progress in active constraint acquisition, the focus has only been on learning satisfaction problems with hard constraints. In this paper, we deal with the problem of learning soft constraints in optimization problems via active constraint acquisition, specifically in the context of the Max-CSP. Towards this, we first introduce a new type of queries in the context of constraint acquisition, namely partial preference queries, and then we present a novel algorithm for learning soft constraints in Max-CSPs, using such queries. We also give some experimental results.

Cite as

Dimosthenis C. Tsouros and Kostas Stergiou. Learning Max-CSPs via Active Constraint Acquisition. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 54:1-54:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{tsouros_et_al:LIPIcs.CP.2021.54,
  author =	{Tsouros, Dimosthenis C. and Stergiou, Kostas},
  title =	{{Learning Max-CSPs via Active Constraint Acquisition}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{54:1--54:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.54},
  URN =		{urn:nbn:de:0030-drops-153452},
  doi =		{10.4230/LIPIcs.CP.2021.54},
  annote =	{Keywords: Constraint acquisition, modeling, learning}
}
Document
Parallelizing a SAT-Based Product Configurator

Authors: Nils Merlin Ullmann, Tomáš Balyo, and Michael Klein


Abstract
This paper presents how state-of-the-art parallel algorithms designed to solve the Satisfiability (SAT) problem can be applied in the domain of product configuration. During an interactive configuration process, a user selects features step-by-step to find a suitable configuration that fulfills his desires and the set of product constraints. A configuration system can be used to guide the user through the process by validating the selections and providing feedback. Each validation of a user selection is formulated as a SAT problem. Furthermore, an optimization problem is identified to find solutions with the minimum amount of changes compared to the previous configuration. Another additional constraint is deterministic computation, which is not trivial to achieve in well performing parallel SAT solvers. In the paper we propose five new deterministic parallel algorithms and experimentally compare them. Experiments show that reasonable speedups are achieved by using multiple threads over the sequential counterpart.

Cite as

Nils Merlin Ullmann, Tomáš Balyo, and Michael Klein. Parallelizing a SAT-Based Product Configurator. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 55:1-55:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ullmann_et_al:LIPIcs.CP.2021.55,
  author =	{Ullmann, Nils Merlin and Balyo, Tom\'{a}\v{s} and Klein, Michael},
  title =	{{Parallelizing a SAT-Based Product Configurator}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{55:1--55:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.55},
  URN =		{urn:nbn:de:0030-drops-153464},
  doi =		{10.4230/LIPIcs.CP.2021.55},
  annote =	{Keywords: Configuration, Satisfiability, Parallel}
}
Document
Solution Sampling with Random Table Constraints

Authors: Mathieu Vavrille, Charlotte Truchet, and Charles Prud'homme


Abstract
Constraint programming provides generic techniques to efficiently solve combinatorial problems. In this paper, we tackle the natural question of using constraint solvers to sample combinatorial problems in a generic way. We propose an algorithm, inspired from Meel’s ApproxMC algorithm on SAT, to add hashing constraints to a CP model in order to split the search space into small cells of solutions. By sampling the solutions in the restricted search space, we can randomly generate solutions without revamping the model of the problem. We ensure the randomness by introducing a new family of hashing constraints: randomly generated tables. We implemented this solving method using the constraint solver Choco-solver. The quality of the randomness and the running time of our approach are experimentally compared to a random branching strategy. We show that our approach improves the randomness while being in the same order of magnitude in terms of running time.

Cite as

Mathieu Vavrille, Charlotte Truchet, and Charles Prud'homme. Solution Sampling with Random Table Constraints. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 56:1-56:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{vavrille_et_al:LIPIcs.CP.2021.56,
  author =	{Vavrille, Mathieu and Truchet, Charlotte and Prud'homme, Charles},
  title =	{{Solution Sampling with Random Table Constraints}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{56:1--56:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.56},
  URN =		{urn:nbn:de:0030-drops-153477},
  doi =		{10.4230/LIPIcs.CP.2021.56},
  annote =	{Keywords: solutions, sampling, table constraint}
}
Document
Making Rigorous Linear Programming Practical for Program Analysis

Authors: Tengbin Wang, Liqian Chen, Taoqing Chen, Guangsheng Fan, and Ji Wang


Abstract
Linear programming is a key technique for analysis and verification of numerical properties in programs, neural networks, etc. In particular, in program analysis based on abstract interpretation, many numerical abstract domains (such as Template Constraint Matrix, constraint-only polyhedra, etc.) are designed on top of linear programming. However, most state-of-the-art linear programming solvers use floating-point arithmetic in their implementations, leading to an approximate result that may be unsound. On the other hand, the solvers implemented using exact arithmetic are too costly. To this end, this paper focuses on advancing rigorous linear programming techniques based on floating-point arithmetic for building sound and efficient program analysis. Particularly, as a supplement to existing techniques, we present a novel rigorous linear programming technique based on Fourier-Mozkin elimination. On this basis, we implement a tool, namely, RlpSolver, combining our technique with existing techniques to lift effectiveness of rigorous linear programming in the scene of analysis and verification. Experimental results show that our technique is complementary to existing techniques, and their combination (RlpSolver) can achieve a better trade-off between cost and precision via heuristic rules.

Cite as

Tengbin Wang, Liqian Chen, Taoqing Chen, Guangsheng Fan, and Ji Wang. Making Rigorous Linear Programming Practical for Program Analysis. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 57:1-57:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{wang_et_al:LIPIcs.CP.2021.57,
  author =	{Wang, Tengbin and Chen, Liqian and Chen, Taoqing and Fan, Guangsheng and Wang, Ji},
  title =	{{Making Rigorous Linear Programming Practical for Program Analysis}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{57:1--57:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.57},
  URN =		{urn:nbn:de:0030-drops-153486},
  doi =		{10.4230/LIPIcs.CP.2021.57},
  annote =	{Keywords: Linear programming, rigorous linear programming, abstract interpretation, program analysis, Fourier-Mozkin elimination}
}
Document
Engineering an Efficient PB-XOR Solver

Authors: Jiong Yang and Kuldeep S. Meel


Abstract
Despite the NP-completeness of Boolean satisfiability, modern SAT solvers are routinely able to handle large practical instances, and consequently have found wide ranging applications. The primary workhorse behind the success of SAT solvers is the widely acclaimed Conflict Driven Clause Learning (CDCL) paradigm, which was originally proposed in the context of Boolean formulas in CNF. The wide ranging applications of SAT solvers have highlighted that for several domains, CNF is not a natural representation and the reliance of modern SAT solvers on resolution proof system limit their ability to efficiently solve several families of constraints. Consequently, the past decade has witnessed the design of solvers with native support for constraints such as Pseudo-Boolean (PB) and CNF-XOR. The primary contribution of our work is an efficient solver engineered for PB-XOR formulas, i.e., formulas consisting of a conjunction of PB and XOR constraints. We first observe that a simple adaption of CNF-XOR architecture does not provide an improvement over baseline; our analysis highlights the need for careful engineering of the order of propagations. To this end, we propose three different tactics, all of which achieve significant performance improvements over the baseline. Our work is motivated by applications arising from binarized neural network verification where the verification of properties such as robustness, fairness, trojan attacks can be reduced to model counting queries; the state of the art model counters reduce counting to polynomially many SAT queries over the original formula conjuncted with randomly generated XOR constraints. To this end, we augment ApproxMC with LinPB and we call the resulting counter as ApproxMCPB. In an extensive empirical comparison over 1076 benchmarks, we observe that ApproxMCPB can solve 912 instances while the baseline version of ApproxMC4 (augmented with CryptoMiniSat) can solve only 802 instances.

Cite as

Jiong Yang and Kuldeep S. Meel. Engineering an Efficient PB-XOR Solver. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 58:1-58:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{yang_et_al:LIPIcs.CP.2021.58,
  author =	{Yang, Jiong and Meel, Kuldeep S.},
  title =	{{Engineering an Efficient PB-XOR Solver}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{58:1--58:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.58},
  URN =		{urn:nbn:de:0030-drops-153499},
  doi =		{10.4230/LIPIcs.CP.2021.58},
  annote =	{Keywords: PB-XOR Solving, Pseudo-Boolean, XOR, Gauss Jordan Elimination, SAT-Solving, Model Counting}
}
Document
Automated Random Testing of Numerical Constrained Types

Authors: Ghiles Ziat, Matthieu Dien, and Vincent Botbol


Abstract
We propose an automated testing framework based on constraint programming techniques. Our framework allows the developer to attach a numerical constraint to a type that restricts its set of possible values. We use this constraint as a partial specification of the program, our goal being to derive property-based tests on such annotated programs. To achieve this, we rely on the user-provided constraints on the types of a program: for each function f present in the program, that returns a constrained type, we generate a test. The tests consists of generating uniformly pseudo-random inputs and checking whether f’s output satisfies the constraint. We are able to automate this process by providing a set of generators for primitive types and generator combinators for composite types. To derive generators for constrained types, we present in this paper a technique that characterizes their inhabitants as the solution set of a numerical CSP. This is done by combining abstract interpretation and constraint solving techniques that allow us to efficiently and uniformly generate solutions of numerical CSP. We validated our approach by implementing it as a syntax extension for the OCaml language.

Cite as

Ghiles Ziat, Matthieu Dien, and Vincent Botbol. Automated Random Testing of Numerical Constrained Types. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 59:1-59:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{ziat_et_al:LIPIcs.CP.2021.59,
  author =	{Ziat, Ghiles and Dien, Matthieu and Botbol, Vincent},
  title =	{{Automated Random Testing of Numerical Constrained Types}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{59:1--59:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.59},
  URN =		{urn:nbn:de:0030-drops-153502},
  doi =		{10.4230/LIPIcs.CP.2021.59},
  annote =	{Keywords: Constraint Programming, Automated Random Testing, Abstract Domains, Constrained Types}
}
Document
The Effect of Asynchronous Execution and Message Latency on Max-Sum

Authors: Roie Zivan, Omer Perry, Ben Rachmut, and William Yeoh


Abstract
Max-sum is a version of belief propagation that was adapted for solving distributed constraint optimization problems (DCOPs). It has been studied theoretically and empirically, extended to versions that improve solution quality and converge rapidly, and is applicable to multiple distributed applications. The algorithm was presented both as a synchronous and an asynchronous algorithm, however, neither the differences in the performance of these two execution versions nor the implications of message latency on the two versions have been investigated to the best of our knowledge. We contribute to the body of knowledge on Max-sum by: (1) Establishing the theoretical differences between the two execution versions of the algorithm, focusing on the construction of beliefs; (2) Empirically evaluating the differences between the solutions generated by the two versions of the algorithm, with and without message latency; and (3) Establishing both theoretically and empirically the positive effect of damping on reducing the differences between the two versions. Our results indicate that in contrast to recent published results indicating the drastic effect that message latency has on distributed local search, damped Max-sum is robust to message latency.

Cite as

Roie Zivan, Omer Perry, Ben Rachmut, and William Yeoh. The Effect of Asynchronous Execution and Message Latency on Max-Sum. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 60:1-60:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{zivan_et_al:LIPIcs.CP.2021.60,
  author =	{Zivan, Roie and Perry, Omer and Rachmut, Ben and Yeoh, William},
  title =	{{The Effect of Asynchronous Execution and Message Latency on Max-Sum}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{60:1--60:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.60},
  URN =		{urn:nbn:de:0030-drops-153518},
  doi =		{10.4230/LIPIcs.CP.2021.60},
  annote =	{Keywords: Distributed constraints, Distributed problem solving}
}

Filters


Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail