Search Results

Documents authored by Marquis, Pierre

Document
DOI: 10.4230/LIPIcs.SAT.2024.21
Dynamic Blocked Clause Elimination for Projected Model Counting

Authors: Jean-Marie Lagniez, Pierre Marquis, and Armin Biere

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
In this paper, we explore the application of blocked clause elimination for projected model counting. This is the problem of determining the number of models ‖∃ X . Σ‖ of a propositional formula Σ after eliminating a given set X of variables existentially. Although blocked clause elimination is a well-known technique for SAT solving, its direct application to model counting is challenging as in general it changes the number of models. However, we demonstrate, by focusing on projected variables during the blocked clause search, that blocked clause elimination can be leveraged while preserving the correct model count. To take advantage of blocked clause elimination in an efficient way during model counting, a novel data structure and associated algorithms are introduced. Our proposed approach is implemented in the model counter d4. Our experiments demonstrate the computational benefits of our new method of blocked clause elimination for projected model counting.
Cite as

Jean-Marie Lagniez, Pierre Marquis, and Armin Biere. Dynamic Blocked Clause Elimination for Projected Model Counting. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{lagniez_et_al:LIPIcs.SAT.2024.21,
  author =	{Lagniez, Jean-Marie and Marquis, Pierre and Biere, Armin},
  title =	{{Dynamic Blocked Clause Elimination for Projected Model Counting}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{21:1--21:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.21},
  URN =		{urn:nbn:de:0030-drops-205430},
  doi =		{10.4230/LIPIcs.SAT.2024.21},
  annote =	{Keywords: Projected model counting, blocked clause elimination, propositional logic}
}
Document
DOI: 10.4230/DagRep.7.9.62
Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381)

Authors: Adnan Darwiche, Pierre Marquis, Dan Suciu, and Stefan Szeider

Published in: Dagstuhl Reports, Volume 7, Issue 9 (2018)

Abstract
Knowledge compilation (KC) is a research topic which aims to investigate the possibility of circumventing the computational intractability of hard tasks, by preprocessing part of the available information, common to a number of instances. Pioneered almost three decades ago, KC is nowadays a very active research field, transversal to several areas within computer science. Among others, KC intersects knowledge representation, constraint satisfaction, algorithms, complexity theory, machine learning, and databases. The results obtained so far take various forms, from theory (compilability settings, definition of target languages for KC, complexity results, succinctness results, etc.) to more practical results (development and evaluation of compilers and other preprocessors, applications to diagnosis, planning, automatic configuration, etc.). Recently, KC has been positioned as providing a systematic method for solving problems beyond NP, and also found applications in machine learning. The goal of this Dagstuhl Seminar was to advance both aspects of KC, and to pave the way for a fruitful cross-fertilization between the topics, from theory to practice. The program included a mixture of long and short presentations, with discussions. Several long talks with a tutorial flavor introduced the participants to the variety of aspects in knowledge compilation and the diversity of techniques used. System presentations as well as an open problem session were also included in the program.
Cite as

Adnan Darwiche, Pierre Marquis, Dan Suciu, and Stefan Szeider. Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381). In Dagstuhl Reports, Volume 7, Issue 9, pp. 62-85, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@Article{darwiche_et_al:DagRep.7.9.62,
  author =	{Darwiche, Adnan and Marquis, Pierre and Suciu, Dan and Szeider, Stefan},
  title =	{{Recent Trends in Knowledge Compilation (Dagstuhl Seminar 17381)}},
  pages =	{62--85},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2018},
  volume =	{7},
  number =	{9},
  editor =	{Darwiche, Adnan and Marquis, Pierre and Suciu, Dan and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.7.9.62},
  URN =		{urn:nbn:de:0030-drops-85896},
  doi =		{10.4230/DagRep.7.9.62},
  annote =	{Keywords: Knowledge compilation, Constraints, Preprocessing, Probabilistic databases, Model counting}
}
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