3 Search Results for "Markus, Manfred"


Document
SAT-Based Generation of Planar Graphs

Authors: Markus Kirchweger, Manfred Scheucher, and Stefan Szeider

Published in: LIPIcs, Volume 271, 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)


Abstract
To test a graph’s planarity in SAT-based graph generation we develop SAT encodings with dynamic symmetry breaking as facilitated in the SAT modulo Symmetry (SMS) framework. We implement and compare encodings based on three planarity criteria. In particular, we consider two eager encodings utilizing order-based and universal-set-based planarity criteria, and a lazy encoding based on Kuratowski’s theorem. The performance and scalability of these encodings are compared on two prominent problems from combinatorics: the computation of planar Turán numbers and the Earth-Moon problem. We further showcase the power of SMS equipped with a planarity encoding by verifying and extending several integer sequences from the Online Encyclopedia of Integer Sequences (OEIS) related to planar graph enumeration. Furthermore, we extend the SMS framework to directed graphs which might be of independent interest.

Cite as

Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. SAT-Based Generation of Planar Graphs. In 26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 271, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2023.14,
  author =	{Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
  title =	{{SAT-Based Generation of Planar Graphs}},
  booktitle =	{26th International Conference on Theory and Applications of Satisfiability Testing (SAT 2023)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-286-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{271},
  editor =	{Mahajan, Meena and Slivovsky, Friedrich},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2023.14},
  URN =		{urn:nbn:de:0030-drops-184767},
  doi =		{10.4230/LIPIcs.SAT.2023.14},
  annote =	{Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, planarity test, universal point set, order dimension, Schnyder’s theorem, Kuratowski’s theorem, Tur\'{a}n’s theorem, Earth-Moon problem}
}
Document
A SAT Attack on Rota’s Basis Conjecture

Authors: Markus Kirchweger, Manfred Scheucher, and Stefan Szeider

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)


Abstract
The SAT modulo Symmetries (SMS) is a recently introduced framework for dynamic symmetry breaking in SAT instances. It combines a CDCL SAT solver with an external lexicographic minimality checking algorithm. We extend SMS from graphs to matroids and use it to progress on Rota’s Basis Conjecture (1989), which states that one can always decompose a collection of r disjoint bases of a rank r matroid into r disjoint rainbow bases. Through SMS, we establish that the conjecture holds for all matroids of rank 4 and certain special cases of matroids of rank 5. Furthermore, we extend SMS with the facility to produce DRAT proofs. External tools can then be used to verify the validity of additional axioms produced by the lexicographic minimality check. As a byproduct, we have utilized our framework to enumerate matroids modulo isomorphism and to support the investigation of various other problems on matroids.

Cite as

Markus Kirchweger, Manfred Scheucher, and Stefan Szeider. A SAT Attack on Rota’s Basis Conjecture. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 4:1-4:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@InProceedings{kirchweger_et_al:LIPIcs.SAT.2022.4,
  author =	{Kirchweger, Markus and Scheucher, Manfred and Szeider, Stefan},
  title =	{{A SAT Attack on Rota’s Basis Conjecture}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{4:1--4:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.4},
  URN =		{urn:nbn:de:0030-drops-166780},
  doi =		{10.4230/LIPIcs.SAT.2022.4},
  annote =	{Keywords: SAT modulo Symmetry (SMS), dynamic symmetry breaking, Rota’s basis conjecture, matroid}
}
Document
Joseph Wright's English Dialect Dictionary (1898-1905) Computerised: architecture and retrieval routine

Authors: Manfred Markus

Published in: Dagstuhl Seminar Proceedings, Volume 6491, Digital Historical Corpora- Architecture, Annotation, and Retrieval (2007)


Abstract
The Innsbruck government-funded project SPEED (Spoken English in Early Dialects), scheduled for 2006 to 2009, has the aim of digitising and evaluating the famous English Dialect Dictionary by Joseph Wright (1898-1906). This paper topicalises the value of the electronic version of the dictionary and problems of its complex architecture, as well as the retrieval routine aimed at. The paper is an elaborated version of the Powerpoint presentation delivered at the conference. First of all, I try to prove the great value of Wright's dictionary from the point of view of English studies. On the other hand, given the mixed nature of the participants of the Dagstuhl conference, the paper tackles interface problems typically arising when printed texts are computerised, problems ranging from "normalisation" to aspects of parsing and of the design of the query mask.

Cite as

Manfred Markus. Joseph Wright's English Dialect Dictionary (1898-1905) Computerised: architecture and retrieval routine. In Digital Historical Corpora- Architecture, Annotation, and Retrieval. Dagstuhl Seminar Proceedings, Volume 6491, pp. 1-11, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2007)


Copy BibTex To Clipboard

@InProceedings{markus:DagSemProc.06491.11,
  author =	{Markus, Manfred},
  title =	{{Joseph Wright's English Dialect Dictionary (1898-1905) Computerised: architecture and retrieval routine}},
  booktitle =	{Digital Historical Corpora- Architecture, Annotation, and Retrieval},
  pages =	{1--11},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2007},
  volume =	{6491},
  editor =	{Lou Burnard and Milena Dobreva and Norbert Fuhr and Anke L\"{u}deling},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.06491.11},
  URN =		{urn:nbn:de:0030-drops-10523},
  doi =		{10.4230/DagSemProc.06491.11},
  annote =	{Keywords: Corpus linguistics, dialectology, spoken English, history of English, lexicography, computer philology, normalisation, web design}
}
  • Refine by Author
  • 2 Kirchweger, Markus
  • 2 Scheucher, Manfred
  • 2 Szeider, Stefan
  • 1 Markus, Manfred

  • Refine by Classification
  • 2 Hardware → Theorem proving and SAT solving
  • 2 Mathematics of computing → Solvers
  • 1 Mathematics of computing → Graph enumeration
  • 1 Mathematics of computing → Matroids and greedoids
  • 1 Theory of computation → Automated reasoning

  • Refine by Keyword
  • 2 SAT modulo Symmetry (SMS)
  • 2 dynamic symmetry breaking
  • 1 Corpus linguistics
  • 1 Earth-Moon problem
  • 1 Kuratowski’s theorem
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 1 2007
  • 1 2022
  • 1 2023

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