Search Results

Documents authored by Devriendt, Jo


Artifact
Dataset
ML-KULeuven/SAT25_PB_reductions_experiments

Authors: Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns


Abstract

Cite as

Orestis Lomis, Jo Devriendt, Hendrik Bierlee, Tias Guns. ML-KULeuven/SAT25_PB_reductions_experiments (Dataset, Experimental Results). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@misc{dagstuhl-artifact-24089,
   title = {{ML-KULeuven/SAT25\underlinePB\underlinereductions\underlineexperiments}}, 
   author = {Lomis, Orestis and Devriendt, Jo and Bierlee, Hendrik and Guns, Tias},
   note = {Dataset, This research was partly funded by the European Research Council (ERC) under the EU Horizon 2020 research and innovation programme (Grant No 101002802, CHAT-Opt)., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:650c2f9b37926504a59a11a6dbf319620b311dc3;origin=https://github.com/ML-KULeuven/SAT25_PB_reductions_experiments;visit=swh:1:snp:c9843bb9ce4bf323c83b69edd5820bdb654e19be;anchor=swh:1:rev:d5b602b4b96833a077bd379b2803314349cb8548}{\texttt{swh:1:dir:650c2f9b37926504a59a11a6dbf319620b311dc3}} (visited on 2025-08-07)},
   url = {https://github.com/ML-KULeuven/SAT25_PB_reductions_experiments},
   doi = {10.4230/artifacts.24089},
}
Document
Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis

Authors: Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns

Published in: LIPIcs, Volume 341, 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)


Abstract
Recent pseudo-Boolean (PB) solvers leverage the cutting planes proof system to perform SAT-style conflict analysis during search. This process learns implied PB constraints, which can prune later parts of the search tree and is crucial to a PB solver’s performance. A key step in PB conflict analysis is the reduction of a reason constraint, which caused a variable propagation that contributed to the conflict. While necessary, reduction generally makes the reason constraint less strong. Consequently, different approaches to reduction have been proposed, broadly categorised as division- or saturation-based, with the aim of preserving the strength of the reason constraint as much as possible. This paper proposes two novel techniques in each reduction category. We theoretically show how each technique yields reason constraints which are at least as strong as those obtained from existing reduction methods. We then evaluate the empirical effectiveness of the reduction techniques on hard knapsack instances and the most recent PB'24 competition benchmarks.

Cite as

Orestis Lomis, Jo Devriendt, Hendrik Bierlee, and Tias Guns. Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis. In 28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 341, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)


Copy BibTex To Clipboard

@InProceedings{lomis_et_al:LIPIcs.SAT.2025.21,
  author =	{Lomis, Orestis and Devriendt, Jo and Bierlee, Hendrik and Guns, Tias},
  title =	{{Improving Reduction Techniques in Pseudo-Boolean Conflict Analysis}},
  booktitle =	{28th International Conference on Theory and Applications of Satisfiability Testing (SAT 2025)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-381-2},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{341},
  editor =	{Berg, Jeremias and Nordstr\"{o}m, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2025.21},
  URN =		{urn:nbn:de:0030-drops-237551},
  doi =		{10.4230/LIPIcs.SAT.2025.21},
  annote =	{Keywords: Constraint Programming, Pseudo-Boolean Reasoning, Conflict Analysis}
}
Document
Mutational Fuzz Testing for Constraint Modeling Systems

Authors: Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)


Abstract
Constraint programming (CP) modeling languages, like MiniZinc, Essence and CPMpy, play a crucial role in making CP technology accessible to non-experts. Both solver-independent modeling frameworks and solvers themselves are complex pieces of software that can contain bugs, which undermines their usefulness. Mutational fuzz testing is a way to test complex systems by stochastically mutating input and verifying preserved properties of the mutated output. We investigate different mutations and verification methods that can be used on the constraint specifications directly. This includes methods proposed in the context of SMT problem specifications, as well as new methods related to global constraints, optimization, and solution counting/preservation. Our results show that such a fuzz testing approach improves the overall code coverage of a modeling system compared to only unit testing, and is able to find bugs in the whole toolchain, from the modeling language transformations themselves to the underlying solvers.

Cite as

Wout Vanroose, Ignace Bleukx, Jo Devriendt, Dimos Tsouros, Hélène Verhaeghe, and Tias Guns. Mutational Fuzz Testing for Constraint Modeling Systems. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 29:1-29:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)


Copy BibTex To Clipboard

@InProceedings{vanroose_et_al:LIPIcs.CP.2024.29,
  author =	{Vanroose, Wout and Bleukx, Ignace and Devriendt, Jo and Tsouros, Dimos and Verhaeghe, H\'{e}l\`{e}ne and Guns, Tias},
  title =	{{Mutational Fuzz Testing for Constraint Modeling Systems}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{29:1--29:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.29},
  URN =		{urn:nbn:de:0030-drops-207149},
  doi =		{10.4230/LIPIcs.CP.2024.29},
  annote =	{Keywords: fuzz testing, Constraint modeling language, bugs, mutational testing, modeling, constraint reformulation}
}
Document
Simplifying Step-Wise Explanation Sequences

Authors: Ignace Bleukx, Jo Devriendt, Emilio Gamba, Bart Bogaerts, and Tias Guns

Published in: LIPIcs, Volume 280, 29th International Conference on Principles and Practice of Constraint Programming (CP 2023)


Abstract
Explaining constraint programs is useful for debugging an unsatisfiable program, to understand why a given solution is optimal, or to understand how to find a unique solution. A recently proposed framework for explaining constraint programs works well to explain the unique solution to a problem step by step. It can also be used to step-wise explain why a model is unsatisfiable, but this may create redundant steps and introduce superfluous information into the explanation sequence. This paper proposes methods to simplify a (step-wise) explanation sequence, to generate simple steps that together form a short, interpretable sequence. We propose an algorithm to greedily construct an initial sequence and two filtering algorithms that eliminate redundant steps and unnecessarily complex parts of explanation sequences. Experiments on diverse benchmark instances show that our techniques can significantly simplify step-wise explanation sequences.

Cite as

Ignace Bleukx, Jo Devriendt, Emilio Gamba, Bart Bogaerts, and Tias Guns. Simplifying Step-Wise Explanation Sequences. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 11:1-11:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{bleukx_et_al:LIPIcs.CP.2023.11,
  author =	{Bleukx, Ignace and Devriendt, Jo and Gamba, Emilio and Bogaerts, Bart and Guns, Tias},
  title =	{{Simplifying Step-Wise Explanation Sequences}},
  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
  pages =	{11:1--11:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-300-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{280},
  editor =	{Yap, Roland H. C.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2023.11},
  URN =		{urn:nbn:de:0030-drops-190489},
  doi =		{10.4230/LIPIcs.CP.2023.11},
  annote =	{Keywords: explanation, deduction, constraint programming, propagation}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail