66 Search Results for "Michel, Laurent"

Volume

LIPIcs, Volume 210

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

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

Editors: Laurent D. Michel

Document
DOI: 10.4230/LIPIcs.CP.2022.17
DUELMIPs: Optimizing SDN Functionality and Security

Authors: Timothy Curry, Gabriel De Pace, Benjamin Fuller, Laurent Michel, and Yan (Lindsay) Sun

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
Software defined networks (SDNs) define a programmable network fabric that can be reconfigured to respect global networks properties. Securing against adversaries who try to exploit the network is an objective that conflicts with providing functionality. This paper proposes a two-stage mixed-integer programming framework. The first stage automates routing decisions for the flows to be carried by the network while maximizing readability and ease of use for network engineers. The second stage is meant to quickly respond to security breaches to automatically decide on network counter-measures to block the detected adversary. Both stages are computationally challenging and the security stage leverages large neighborhood search to quickly deliver effective response strategies. The approach is evaluated on synthetic networks of various sizes and shown to be effective for both its functional and security objectives.
Cite as

Timothy Curry, Gabriel De Pace, Benjamin Fuller, Laurent Michel, and Yan (Lindsay) Sun. DUELMIPs: Optimizing SDN Functionality and Security. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 17:1-17:18, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{curry_et_al:LIPIcs.CP.2022.17,
  author =	{Curry, Timothy and De Pace, Gabriel and Fuller, Benjamin and Michel, Laurent and Sun, Yan (Lindsay)},
  title =	{{DUELMIPs: Optimizing SDN Functionality and Security}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{17:1--17:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.17},
  URN =		{urn:nbn:de:0030-drops-166468},
  doi =		{10.4230/LIPIcs.CP.2022.17},
  annote =	{Keywords: Network security, mixed integer programming, large neighborhood search}
}
Document
DOI: 10.4230/LIPIcs.CP.2022.24
Heuristics for MDD Propagation in HADDOCK

Authors: Rebecca Gentzel, Laurent Michel, and Willem-Jan van Hoeve

Published in: LIPIcs, Volume 235, 28th International Conference on Principles and Practice of Constraint Programming (CP 2022)

Abstract
Haddock, introduced in [R. Gentzel et al., 2020], is a declarative language and architecture for the specification and the implementation of multi-valued decision diagrams. It relies on a labeled transition system to specify and compose individual constraints into a propagator with filtering capabilities that automatically deliver the expected level of filtering. Yet, the operational potency of the filtering algorithms strongly correlate with heuristics for carrying out refinements of the diagrams. This paper considers how to empower Haddock users with the ability to unobtrusively specify various such heuristics and derive the computational benefits of exerting fine-grained control over the refinement process.
Cite as

Rebecca Gentzel, Laurent Michel, and Willem-Jan van Hoeve. Heuristics for MDD Propagation in HADDOCK. In 28th International Conference on Principles and Practice of Constraint Programming (CP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 235, pp. 24:1-24:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{gentzel_et_al:LIPIcs.CP.2022.24,
  author =	{Gentzel, Rebecca and Michel, Laurent and van Hoeve, Willem-Jan},
  title =	{{Heuristics for MDD Propagation in HADDOCK}},
  booktitle =	{28th International Conference on Principles and Practice of Constraint Programming (CP 2022)},
  pages =	{24:1--24:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-240-2},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{235},
  editor =	{Solnon, Christine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2022.24},
  URN =		{urn:nbn:de:0030-drops-166534},
  doi =		{10.4230/LIPIcs.CP.2022.24},
  annote =	{Keywords: Decision Diagrams}
}
Document
Complete Volume
DOI: 10.4230/LIPIcs.CP.2021
LIPIcs, Volume 210, CP 2021, Complete Volume

Authors: Laurent D. Michel

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
LIPIcs, Volume 210, CP 2021, Complete Volume
Cite as

Laurent D. Michel. LIPIcs, Volume 210, CP 2021, Complete Volume. In 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
DOI: 10.4230/LIPIcs.CP.2021.0
Front Matter, Table of Contents, Preface, Conference Organization

Authors: Laurent D. Michel

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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

Laurent D. Michel. Front Matter, Table of Contents, Preface, Conference Organization. In 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
DOI: 10.4230/LIPIcs.CP.2021.1
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

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.2
Constrained-Based Differential Privacy (Invited Talk)

Authors: Ferdinando Fioretto

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.3
Learning in Local Branching (Invited Talk)

Authors: Defeng Liu and Andrea Lodi

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.4
Filtering Isomorphic Models by Invariants (Short Paper)

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

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.5
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

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.6
Unit Propagation with Stable Watches (Short Paper)

Authors: Markus Iser and Tomáš Balyo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.7
Towards Better Heuristics for Solving Bounded Model Checking Problems (Short Paper)

Authors: Anissa Kheireddine, Etienne Renault, and Souheib Baarir

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.8
Integrating Tree Decompositions into Decision Heuristics of Propositional Model Counters (Short Paper)

Authors: Tuukka Korhonen and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.9
Failure Based Variable Ordering Heuristics for Solving CSPs (Short Paper)

Authors: Hongbo Li, Minghao Yin, and Zhanshan Li

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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
DOI: 10.4230/LIPIcs.CP.2021.10
Generating Magical Performances with Constraint Programming (Short Paper)

Authors: Guilherme de Azevedo Silveira

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

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}
}
  • Refine by Author
  • 4 Järvisalo, Matti
  • 3 Berg, Jeremias
  • 2 Antuori, Valentin
  • 2 Balyo, Tomáš
  • 2 Cai, Shaowei
  • Show More...

  • Refine by Classification
  • 26 Theory of computation → Constraint and logic programming
  • 7 Computing methodologies → Planning and scheduling
  • 7 Mathematics of computing → Combinatorial optimization
  • 5 Computing methodologies → Machine learning
  • 4 Computing methodologies → Artificial intelligence
  • Show More...

  • Refine by Keyword
  • 7 Constraint Programming
  • 5 MaxSAT
  • 4 constraint programming
  • 3 Constraint
  • 3 SAT
  • Show More...

  • Refine by Type
  • 65 document
  • 1 volume

  • Refine by Publication Year
  • 63 2021
  • 2 2022
  • 1 2016

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
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact