Search Results

Documents authored by Brault-Baron, Johann

Document
DOI: 10.4230/LIPIcs.STACS.2015.143
Understanding Model Counting for beta-acyclic CNF-formulas

Authors: Johann Brault-Baron, Florent Capelli, and Stefan Mengel

Published in: LIPIcs, Volume 30, 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)

Abstract
We show that SAT on beta-acyclic CNF-formulas can be solved in polynomial time. In contrast to previous algorithms for other structurally restricted classes of formulas, our algorithm does not proceed by dynamic programming. Instead, it works along an elimination order, solving a weighted version of constraint satisfaction. We give evidence that this deviation from more standard algorithms is no coincidence by showing that it is outside of the framework recently proposed by Saether et al. (SAT 2014) which subsumes all other structural tractability results for #SAT known so far.
Cite as

Johann Brault-Baron, Florent Capelli, and Stefan Mengel. Understanding Model Counting for beta-acyclic CNF-formulas. In 32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 30, pp. 143-156, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)

Copy BibTex To Clipboard

@InProceedings{braultbaron_et_al:LIPIcs.STACS.2015.143,
  author =	{Brault-Baron, Johann and Capelli, Florent and Mengel, Stefan},
  title =	{{Understanding Model Counting for beta-acyclic CNF-formulas}},
  booktitle =	{32nd International Symposium on Theoretical Aspects of Computer Science (STACS 2015)},
  pages =	{143--156},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-78-1},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{30},
  editor =	{Mayr, Ernst W. and Ollinger, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.STACS.2015.143},
  URN =		{urn:nbn:de:0030-drops-49106},
  doi =		{10.4230/LIPIcs.STACS.2015.143},
  annote =	{Keywords: model counting, hypergraph acyclicity, structural tractability}
}
Document
DOI: 10.4230/LIPIcs.CSL.2012.137
A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic

Authors: Johann Brault-Baron

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
It is known that the data complexity of a Conjunctive Query (CQ) is determined *only* by the way its variables are shared between atoms, reflected by its hypergraph. In particular, Yannakakis [Yannakakis VLDB'81,Beeri/Fagin/Maier/Yannakakis JACM'83] proved that a CQ is decidable in linear time when it is alpha-acyclic, i.e. its hypergraph is alpha-acyclic; Bagan et al. [Bagan/Durand/Grandjean CSL'07] even state: * Any CQ is decidable in linear time iff it is alpha-acyclic. (under certain hypotheses) (By linear time, we mean a query on a structure S can be decided in time O(|S|)) A natural question is: since the complexity of a *Negative* Conjunctive Query (NCQ), a conjunctive query where *all* atoms are negated, also only depends on its hypergraph, can we find a similar dichotomy in this case? To answer this question, we revisit a result of Ordyniak et al. --- that states that satisfiability of a beta-acyclic CNF formula is decidable in polynomial time --- by proving that some part of their procedure can be done in linear time. This implies, under an algorithmic hypothesis that is likely true: (precisely: one cannot decide whether a graph is triangle-free in time O(n²log n) where n is the number of vertices.) * Any NCQ is decidable in quasi-linear time iff it is beta-acyclic. (By quasi-linear time, we mean a query on a structure S can be decided in time O(|S|log|S|)) We extend the easiness result to 'Signed' Conjunctive Query (SCQ) where 'some' atoms are negated. This has great interest since using some negated atoms is natural in the frameworks of databases and CSP. Furthermore, it implies straightforwardly the following: * Any beta-acyclic existential first-order query is decidable in quasi-linear time.
Cite as

Johann Brault-Baron. A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic. In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 137-151, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{braultbaron:LIPIcs.CSL.2012.137,
  author =	{Brault-Baron, Johann},
  title =	{{A Negative Conjunctive Query is Easy if and only if it is Beta-Acyclic}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{137--151},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.137},
  URN =		{urn:nbn:de:0030-drops-36697},
  doi =		{10.4230/LIPIcs.CSL.2012.137},
  annote =	{Keywords: conjunctive query, hypergraph, beta-acyclicity, data complexity, Davis-Putnam procedure}
}
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