Search Results

Documents authored by Bogaerts, Bart

Document
DOI: 10.4230/LIPIcs.CP.2024.4
Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Authors: Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande

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

Abstract
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.
Cite as

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berg_et_al:LIPIcs.CP.2024.4,
  author =	{Berg, Jeremias and Bogaerts, Bart and Nordstr\"{o}m, Jakob and Oertel, Andy and Paxian, Tobias and Vandesande, Dieter},
  title =	{{Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{4:1--4:28},
  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.4},
  URN =		{urn:nbn:de:0030-drops-206895},
  doi =		{10.4230/LIPIcs.CP.2024.4},
  annote =	{Keywords: proof logging, certifying algorithms, MaxSAT, solution-improving search, SAT-UNSAT, maximum satisfiability, combinatorial optimization, certification, pseudo-Boolean}
}
Document
DOI: 10.4230/LIPIcs.CP.2023.11
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}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2022.15
Expressiveness of SHACL Features

Authors: Bart Bogaerts, Maxime Jakubowski, and Jan Van den Bussche

Published in: LIPIcs, Volume 220, 25th International Conference on Database Theory (ICDT 2022)

Abstract
SHACL is a W3C-proposed schema language for expressing structural constraints on RDF graphs. Recent work on formalizing this language has revealed a striking relationship to description logics. SHACL expressions can use four fundamental features that are not so common in description logics. These features are zero-or-one path expressions; equality tests; disjointness tests; and closure constraints. Moreover, SHACL is peculiar in allowing only a restricted form of expressions (so-called targets) on the left-hand side of inclusion constraints. The goal of this paper is to obtain a clear picture of the impact and expressiveness of these features and restrictions. We show that each of the four features is primitive: using the feature, one can express boolean queries that are not expressible without using the feature. We also show that the restriction that SHACL imposes on allowed targets is inessential, as long as closure constraints are not used.
Cite as

Bart Bogaerts, Maxime Jakubowski, and Jan Van den Bussche. Expressiveness of SHACL Features. In 25th International Conference on Database Theory (ICDT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 220, pp. 15:1-15:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{bogaerts_et_al:LIPIcs.ICDT.2022.15,
  author =	{Bogaerts, Bart and Jakubowski, Maxime and Van den Bussche, Jan},
  title =	{{Expressiveness of SHACL Features}},
  booktitle =	{25th International Conference on Database Theory (ICDT 2022)},
  pages =	{15:1--15:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-223-5},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{220},
  editor =	{Olteanu, Dan and Vortmeier, Nils},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2022.15},
  URN =		{urn:nbn:de:0030-drops-158890},
  doi =		{10.4230/LIPIcs.ICDT.2022.15},
  annote =	{Keywords: Expressive power, schema languages}
}
Document
DOI: 10.4230/LIPIcs.ICDT.2020.4
Executable First-Order Queries in the Logic of Information Flows

Authors: Heba Aamer, Bart Bogaerts, Dimitri Surinx, Eugenia Ternovska, and Jan Van den Bussche

Published in: LIPIcs, Volume 155, 23rd International Conference on Database Theory (ICDT 2020)

Abstract
The logic of information flows (LIF) has recently been proposed as a general framework in the field of knowledge representation. In this framework, tasks of a procedural nature can still be modeled in a declarative, logic-based fashion. In this paper, we focus on the task of query processing under limited access patterns, a well-studied problem in the database literature. We show that LIF is well-suited for modeling this task. Toward this goal, we introduce a variant of LIF called "forward" LIF, in a first-order setting. We define FLIF^io, a syntactical fragment of forward LIF, and show that it corresponds exactly to the "executable" fragment of first-order logic defined by Nash and Ludäscher. The definition of FLIF^io involves a classification of the free variables of an expression into "input" and "output" variables. Our result hinges on inertia and determinacy laws for forward LIF expressions, which are interesting in their own right. These laws are formulated in terms of the input and output variables.
Cite as

Heba Aamer, Bart Bogaerts, Dimitri Surinx, Eugenia Ternovska, and Jan Van den Bussche. Executable First-Order Queries in the Logic of Information Flows. In 23rd International Conference on Database Theory (ICDT 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 155, pp. 4:1-4:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aamer_et_al:LIPIcs.ICDT.2020.4,
  author =	{Aamer, Heba and Bogaerts, Bart and Surinx, Dimitri and Ternovska, Eugenia and Van den Bussche, Jan},
  title =	{{Executable First-Order Queries in the Logic of Information Flows}},
  booktitle =	{23rd International Conference on Database Theory (ICDT 2020)},
  pages =	{4:1--4:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-139-9},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{155},
  editor =	{Lutz, Carsten and Jung, Jean Christoph},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICDT.2020.4},
  URN =		{urn:nbn:de:0030-drops-119284},
  doi =		{10.4230/LIPIcs.ICDT.2020.4},
  annote =	{Keywords: Logic of Information Flows, Limited access pattern, Executable first-order logic}
}
Document
DOI: 10.4230/OASIcs.ICLP.2016.14
A Compositional Typed Higher-Order Logic with Definitions

Authors: Ingmar Dasseville, Matthias van der Hallen, Bart Bogaerts, Gerda Janssens, and Marc Denecker

Published in: OASIcs, Volume 52, Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)

Abstract
Expressive KR languages are built by integrating different language constructs, or extending a language with new language constructs. This process is difficult if non-truth-functional or non-monotonic constructs are involved. What is needed is a compositional principle. This paper presents a compositional principle for defining logics by modular composition of logical constructs, and applies it to build a higher order logic integrating typed lambda calculus and rule sets under a well-founded or stable semantics. Logical constructs are formalized as triples of a syntactical rule, a semantical rule, and a typing rule. The paper describes how syntax, typing and semantics of the logic are composed from the set of its language constructs. The base semantical concept is the infon: mappings from structures to values in these structures. Semantical operators of language constructs operate on infons and allow to construct the infons of compound expressions from the infons of its subexpressions. This conforms to Frege's principle of compositionality.
Cite as

Ingmar Dasseville, Matthias van der Hallen, Bart Bogaerts, Gerda Janssens, and Marc Denecker. A Compositional Typed Higher-Order Logic with Definitions. In Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016). Open Access Series in Informatics (OASIcs), Volume 52, pp. 14:1-14:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{dasseville_et_al:OASIcs.ICLP.2016.14,
  author =	{Dasseville, Ingmar and van der Hallen, Matthias and Bogaerts, Bart and Janssens, Gerda and Denecker, Marc},
  title =	{{A Compositional Typed Higher-Order Logic with Definitions}},
  booktitle =	{Technical Communications of the 32nd International Conference on Logic Programming (ICLP 2016)},
  pages =	{14:1--14:13},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-007-1},
  ISSN =	{2190-6807},
  year =	{2016},
  volume =	{52},
  editor =	{Carro, Manuel and King, Andy and Saeedloei, Neda and De Vos, Marina},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2016.14},
  URN =		{urn:nbn:de:0030-drops-67447},
  doi =		{10.4230/OASIcs.ICLP.2016.14},
  annote =	{Keywords: Logic, Semantics, Compositionality}
}
Document
DOI: 10.4230/LIPIcs.ICLP.2012.14
Modeling Machine Learning and Data Mining Problems with FO(·)

Authors: Hendrik Blockeel, Bart Bogaerts, Maurice Bruynooghe, Broes De Cat, Stef De Pooter, Marc Denecker, Anthony Labarre, Jan Ramon, and Sicco Verwer

Published in: LIPIcs, Volume 17, Technical Communications of the 28th International Conference on Logic Programming (ICLP'12) (2012)

Abstract
This paper reports on the use of the FO(·) language and the IDP framework for modeling and solving some machine learning and data mining tasks. The core component of a model in the IDP framework is an FO(·) theory consisting of formulas in first order logic and definitions; the latter are basically logic programs where clause bodies can have arbitrary first order formulas. Hence, it is a small step for a well-versed computer scientist to start modeling. We describe some models resulting from the collaboration between IDP experts and domain experts solving machine learning and data mining tasks. A first task is in the domain of stemmatology, a domain of philology concerned with the relationship between surviving variant versions of text. A second task is about a somewhat similar problem within biology where phylogenetic trees are used to represent the evolution of species. A third and final task is about learning a minimal automaton consistent with a given set of strings. For each task, we introduce the problem, present the IDP code and report on some experiments.
Cite as

Hendrik Blockeel, Bart Bogaerts, Maurice Bruynooghe, Broes De Cat, Stef De Pooter, Marc Denecker, Anthony Labarre, Jan Ramon, and Sicco Verwer. Modeling Machine Learning and Data Mining Problems with FO(·). In Technical Communications of the 28th International Conference on Logic Programming (ICLP'12). Leibniz International Proceedings in Informatics (LIPIcs), Volume 17, pp. 14-25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{blockeel_et_al:LIPIcs.ICLP.2012.14,
  author =	{Blockeel, Hendrik and Bogaerts, Bart and Bruynooghe, Maurice and De Cat, Broes and De Pooter, Stef and Denecker, Marc and Labarre, Anthony and Ramon, Jan and Verwer, Sicco},
  title =	{{Modeling Machine Learning and Data Mining Problems with FO(·)}},
  booktitle =	{Technical Communications of the 28th International Conference on Logic Programming (ICLP'12)},
  pages =	{14--25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-43-9},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{17},
  editor =	{Dovier, Agostino and Santos Costa, V{\'\i}tor},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ICLP.2012.14},
  URN =		{urn:nbn:de:0030-drops-36049},
  doi =		{10.4230/LIPIcs.ICLP.2012.14},
  annote =	{Keywords: Knowledge representation and reasoning, declarative modeling, logic programming, knowledge base systems, FO(·), IDP framework, stemmatology, phylogene}
}
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-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact