3 Search Results for "Paparrizou, Anastasia"

Document
DOI: 10.4230/LIPIcs.SAT.2024.11
On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF

Authors: Alexis de Colnet

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

Abstract
Top-down compilers of CNF formulas to circuits in decision-DNNF (Decomposable Negation Normal Form) have proved to be useful for model counting. These compilers rely on a common set of techniques including DPLL-style exploration of the set of models, caching of residual formulas, and connected components detection. Differences between compilers lie in the variable selection heuristics and in the additional processing techniques they may use. We investigate, from a theoretical perspective, the ability of top-down compilation algorithms to find small decision-DNNF circuits for two different variable selection strategies. Both strategies are guided by a graph of the CNF formula and are inspired by what is done in practice. The first uses a dynamic graph-partitioning approach while the second works with a static tree decomposition. We show that the dynamic approach performs significantly better than the static approach for some formulas, and that the opposite also holds for other formulas. Our lower bounds are proved despite loose settings where the compilation algorithm is only forced to follow its designed variable selection strategy and where everything else, including the many opportunities for tie-breaking, can be handled non-deterministically.
Cite as

Alexis de Colnet. On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 11:1-11:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{decolnet:LIPIcs.SAT.2024.11,
  author =	{de Colnet, Alexis},
  title =	{{On the Relative Efficiency of Dynamic and Static Top-Down Compilation to Decision-DNNF}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{11:1--11:21},
  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.11},
  URN =		{urn:nbn:de:0030-drops-205339},
  doi =		{10.4230/LIPIcs.SAT.2024.11},
  annote =	{Keywords: Knowledge compilation, top-down compilation, decision-DNNF Circuits}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.14
On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning

Authors: Michael Sioutis, Anastasia Paparrizou, and Tomi Janhunen

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
A singleton-style consistency is a local consistency that verifies if each base relation (atom) of each constraint of a qualitative constraint network (QCN) can serve as a support with respect to the closure of that network under a (naturally) weaker local consistency. This local consistency is essential for tackling fundamental reasoning problems associated with QCNs, such as the satisfiability checking or the minimal labeling problem, but can suffer from redundant constraint checks, especially when those checks occur far from where the pruning usually takes place. In this paper, we propose singleton-style consistencies that are applied just on the neighbourhood of a singleton-checked constraint instead of the whole network. We make a theoretical comparison with existing consistencies and consequently prove some properties of the new ones. In addition, we propose algorithms to enforce our consistencies, as well as parsimonious variants thereof, that are more efficient in practice than the state of the art. We make an experimental evaluation with random and structured QCNs of Interval Algebra in the phase transition region to demonstrate the potential of our approach.
Cite as

Michael Sioutis, Anastasia Paparrizou, and Tomi Janhunen. On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{sioutis_et_al:LIPIcs.TIME.2019.14,
  author =	{Sioutis, Michael and Paparrizou, Anastasia and Janhunen, Tomi},
  title =	{{On the Utility of Neighbourhood Singleton-Style Consistencies for Qualitative Constraint-Based Spatial and Temporal Reasoning}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{14:1--14:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.14},
  URN =		{urn:nbn:de:0030-drops-113727},
  doi =		{10.4230/LIPIcs.TIME.2019.14},
  annote =	{Keywords: Qualitative constraints, spatial and temporal reasoning, singleton-style consistencies, neighbourhood, minimal labeling problem}
}
Document
DOI: 10.4230/LIPIcs.TIME.2017.19
Collective Singleton-Based Consistency for Qualitative Constraint Networks

Authors: Michael Sioutis, Anastasia Paparrizou, and Jean-François Condotta

Published in: LIPIcs, Volume 90, 24th International Symposium on Temporal Representation and Reasoning (TIME 2017)

Abstract
Partial singleton closure under weak composition, or partial singleton (weak) path-consistency for short, is essential for approximating satisfiability of qualitative constraints networks. Briefly put, partial singleton path-consistency ensures that each base relation of each of the constraints of a qualitative constraint network can define a singleton relation in the corresponding partial closure of that network under weak composition, or in its corresponding partially (weak) path-consistent subnetwork for short. In particular, partial singleton path-consistency has been shown to play a crucial role in tackling the minimal labeling problem of a qualitative constraint network, which is the problem of finding the strongest implied constraints of that network. In this paper, we propose a stronger local consistency that couples partial singleton path-consistency with the idea of collectively deleting certain unfeasible base relations by exploiting singleton checks. We then propose an efficient algorithm for enforcing this consistency that, given a qualitative constraint network, performs fewer constraint checks than the respective algorithm for enforcing partial singleton path-consistency in that network. We formally prove certain properties of our new local consistency, and motivate its usefulness through demonstrative examples and a preliminary experimental evaluation with qualitative constraint networks of Interval Algebra.
Cite as

Michael Sioutis, Anastasia Paparrizou, and Jean-François Condotta. Collective Singleton-Based Consistency for Qualitative Constraint Networks. In 24th International Symposium on Temporal Representation and Reasoning (TIME 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 90, pp. 19:1-19:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{sioutis_et_al:LIPIcs.TIME.2017.19,
  author =	{Sioutis, Michael and Paparrizou, Anastasia and Condotta, Jean-Fran\c{c}ois},
  title =	{{Collective Singleton-Based Consistency for Qualitative Constraint Networks}},
  booktitle =	{24th International Symposium on Temporal Representation and Reasoning (TIME 2017)},
  pages =	{19:1--19:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-052-1},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{90},
  editor =	{Schewe, Sven and Schneider, Thomas and Wijsen, Jef},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2017.19},
  URN =		{urn:nbn:de:0030-drops-79237},
  doi =		{10.4230/LIPIcs.TIME.2017.19},
  annote =	{Keywords: Qualitative constraint network, qualitative spatial and temporal reasoning, partial singleton path-consistency, local consistency, minimal labeling pr}
}
  • Refine by Author
  • 2 Paparrizou, Anastasia
  • 2 Sioutis, Michael
  • 1 Condotta, Jean-François
  • 1 Janhunen, Tomi
  • 1 de Colnet, Alexis

  • Refine by Classification
  • 1 Computing methodologies → Spatial and physical reasoning
  • 1 Computing methodologies → Temporal reasoning
  • 1 Theory of computation → Constraint and logic programming
  • 1 Theory of computation → Dynamic programming

  • Refine by Keyword
  • 1 Knowledge compilation
  • 1 Qualitative constraint network
  • 1 Qualitative constraints
  • 1 decision-DNNF Circuits
  • 1 local consistency
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2017
  • 1 2019
  • 1 2024

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact