3 Search Results for "Kullmann, Oliver"

Document
DOI: 10.4230/LIPIcs.ITCS.2024.48
Proving Unsatisfiability with Hitting Formulas

Authors: Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals

Published in: LIPIcs, Volume 287, 15th Innovations in Theoretical Computer Science Conference (ITCS 2024)

Abstract
A hitting formula is a set of Boolean clauses such that any two of the clauses cannot be simultaneously falsified. Hitting formulas have been studied in many different contexts at least since [Iwama, 1989] and, based on experimental evidence, Peitl and Szeider [Tomás Peitl and Stefan Szeider, 2022] conjectured that unsatisfiable hitting formulas are among the hardest for resolution. Using the fact that hitting formulas are easy to check for satisfiability we make them the foundation of a new static proof system {{rmHitting}}: a refutation of a CNF in {{rmHitting}} is an unsatisfiable hitting formula such that each of its clauses is a weakening of a clause of the refuted CNF. Comparing this system to resolution and other proof systems is equivalent to studying the hardness of hitting formulas. Our first result is that {{rmHitting}} is quasi-polynomially simulated by tree-like resolution, which means that hitting formulas cannot be exponentially hard for resolution and partially refutes the conjecture of Peitl and Szeider. We show that tree-like resolution and {{rmHitting}} are quasi-polynomially separated, while for resolution, this question remains open. For a system that is only quasi-polynomially stronger than tree-like resolution, {{rmHitting}} is surprisingly difficult to polynomially simulate in another proof system. Using the ideas of Raz-Shpilka’s polynomial identity testing for noncommutative circuits [Raz and Shpilka, 2005] we show that {{rmHitting}} is p-simulated by {{rmExtended {{rmFrege}}}}, but we conjecture that much more efficient simulations exist. As a byproduct, we show that a number of static (semi)algebraic systems are verifiable in deterministic polynomial time. We consider multiple extensions of {{rmHitting}}, and in particular a proof system {{{rmHitting}}(⊕)} related to the {{{rmRes}}(⊕)} proof system for which no superpolynomial-size lower bounds are known. {{{rmHitting}}(⊕)} p-simulates the tree-like version of {{{rmRes}}(⊕)} and is at least quasi-polynomially stronger. We show that formulas expressing the non-existence of perfect matchings in the graphs K_{n,n+2} are exponentially hard for {{{rmHitting}}(⊕)} via a reduction to the partition bound for communication complexity. See the full version of the paper for the proofs. They are omitted in this Extended Abstract.
Cite as

Yuval Filmus, Edward A. Hirsch, Artur Riazanov, Alexander Smal, and Marc Vinyals. Proving Unsatisfiability with Hitting Formulas. In 15th Innovations in Theoretical Computer Science Conference (ITCS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 287, pp. 48:1-48:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{filmus_et_al:LIPIcs.ITCS.2024.48,
  author =	{Filmus, Yuval and Hirsch, Edward A. and Riazanov, Artur and Smal, Alexander and Vinyals, Marc},
  title =	{{Proving Unsatisfiability with Hitting Formulas}},
  booktitle =	{15th Innovations in Theoretical Computer Science Conference (ITCS 2024)},
  pages =	{48:1--48:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-309-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{287},
  editor =	{Guruswami, Venkatesan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITCS.2024.48},
  URN =		{urn:nbn:de:0030-drops-195762},
  doi =		{10.4230/LIPIcs.ITCS.2024.48},
  annote =	{Keywords: hitting formulas, polynomial identity testing, query complexity}
}
Document
DOI: 10.4230/DagRep.2.11.87
SAT Interactions (Dagstuhl Seminar 12471)

Authors: Nadia Creignou, Nicola Galesi, Oliver Kullmann, and Heribert Vollmer

Published in: Dagstuhl Reports, Volume 2, Issue 11 (2013)

Abstract
This report documents the programme and outcomes of Dagstuhl Seminar 12471 "SAT Interactions". The seminar brought together researchers from different areas from theoretical computer science as well as the area of SAT solvers. A key objective of the seminar has been to initiate or consolidate discussions among the different groups for a fresh attack on one of the most important problems in theoretical computer science and mathematics.
Cite as

Nadia Creignou, Nicola Galesi, Oliver Kullmann, and Heribert Vollmer. SAT Interactions (Dagstuhl Seminar 12471). In Dagstuhl Reports, Volume 2, Issue 11, pp. 87-101, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)

Copy BibTex To Clipboard

@Article{creignou_et_al:DagRep.2.11.87,
  author =	{Creignou, Nadia and Galesi, Nicola and Kullmann, Oliver and Vollmer, Heribert},
  title =	{{SAT Interactions (Dagstuhl Seminar 12471)}},
  pages =	{87--101},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2013},
  volume =	{2},
  number =	{11},
  editor =	{Creignou, Nadia and Galesi, Nicola and Kullmann, Oliver and Vollmer, Heribert},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.2.11.87},
  URN =		{urn:nbn:de:0030-drops-39786},
  doi =		{10.4230/DagRep.2.11.87},
  annote =	{Keywords: satisfiability problem, computational complexity, P-NP question, proof complexity, combinatorics, SAT-solvers, quantified Boolean formulas}
}
Document
DOI: 10.4230/DagSemProc.06401.4
Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities

Authors: Oliver Kullmann

Published in: Dagstuhl Seminar Proceedings, Volume 6401, Complexity of Constraints (2006)

Abstract
Generalised CNFs are considered using such literals, which exclude exactly one possible value from the domain of the variable. First we consider poly-time SAT decision (and fixed-parameter tractability) exploiting matching theory. Then we consider irredundant generalised CNFs, and characterise some extremal minimally unsatisfiable CNFs.
Cite as

Oliver Kullmann. Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities. In Complexity of Constraints. Dagstuhl Seminar Proceedings, Volume 6401, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2006)

Copy BibTex To Clipboard

@InProceedings{kullmann:DagSemProc.06401.4,
  author =	{Kullmann, Oliver},
  title =	{{Constraint satisfaction problems in clausal form: Autarkies, minimal unsatisfiability, and applications to hypergraph inequalities}},
  booktitle =	{Complexity of Constraints},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2006},
  volume =	{6401},
  editor =	{Nadia Creignou and Phokion Kolaitis and Heribert Vollmer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06401.4},
  URN =		{urn:nbn:de:0030-drops-8030},
  doi =		{10.4230/DagSemProc.06401.4},
  annote =	{Keywords: Signed CNF, autarkies, minimal unsatisfiable, hypergraph colouring, block designs}
}
  • Refine by Author
  • 2 Kullmann, Oliver
  • 1 Creignou, Nadia
  • 1 Filmus, Yuval
  • 1 Galesi, Nicola
  • 1 Hirsch, Edward A.
  • Show More...

  • Refine by Classification
  • 1 Theory of computation → Proof complexity

  • Refine by Keyword
  • 1 P-NP question
  • 1 SAT-solvers
  • 1 Signed CNF
  • 1 autarkies
  • 1 block designs
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2006
  • 1 2013
  • 1 2024

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 Imprint Privacy Contact