2 Search Results for "Saffidine, Abdallah"

Document
DOI: 10.4230/LIPIcs.SAT.2022.31
QBF Programming with the Modeling Language Bule

Authors: Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine

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

Abstract
We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.
Cite as

Jean Christoph Jung, Valentin Mayer-Eichberger, and Abdallah Saffidine. QBF Programming with the Modeling Language Bule. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 31:1-31:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@InProceedings{jung_et_al:LIPIcs.SAT.2022.31,
  author =	{Jung, Jean Christoph and Mayer-Eichberger, Valentin and Saffidine, Abdallah},
  title =	{{QBF Programming with the Modeling Language Bule}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{31:1--31:14},
  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.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.31},
  URN =		{urn:nbn:de:0030-drops-167058},
  doi =		{10.4230/LIPIcs.SAT.2022.31},
  annote =	{Keywords: Modeling, QBF Programming, CNF Encodings}
}
Document
DOI: 10.4230/LIPIcs.ICALP.2017.90
The Parameterized Complexity of Positional Games

Authors: Édouard Bonnet, Serge Gaspers, Antonin Lambilliotte, Stefan Rümmele, and Abdallah Saffidine

Published in: LIPIcs, Volume 80, 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)

Abstract
We study the parameterized complexity of several positional games. Our main result is that Short Generalized Hex is W[1]-complete parameterized by the number of moves. This solves an open problem from Downey and Fellows’ influential list of open problems from 1999. Previously, the problem was thought of as a natural candidate for AW[*]-completeness. Our main tool is a new fragment of first-order logic where universally quantified variables only occur in inequalities. We show that model-checking on arbitrary relational structures for a formula in this fragment is W[1]-complete when parameterized by formula size. We also consider a general framework where a positional game is represented as a hypergraph and two players alternately pick vertices. In a Maker-Maker game, the first player to have picked all the vertices of some hyperedge wins the game. In a Maker-Breaker game, the first player wins if she picks all the vertices of some hyperedge, and the second player wins otherwise. In an Enforcer-Avoider game, the first player wins if the second player picks all the vertices of some hyperedge, and the second player wins otherwise. Short Maker-Maker, Short Maker-Breaker, and Short Enforcer-Avoider are respectively AW[*]-, W[1]-, and co-W[1]-complete parameterized by the number of moves. This suggests a rough parameterized complexity categorization into positional games that are complete for the first level of the W-hierarchy when the winning condition only depends on which vertices one player has been able to pick, but AW[*]-complete when it depends on which vertices both players have picked. However, some positional games with highly structured board and winning configurations are fixed-parameter tractable. We give another example of such a game, Short k-Connect, which is fixed-parameter tractable when parameterized by the number of moves.
Cite as

Édouard Bonnet, Serge Gaspers, Antonin Lambilliotte, Stefan Rümmele, and Abdallah Saffidine. The Parameterized Complexity of Positional Games. In 44th International Colloquium on Automata, Languages, and Programming (ICALP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 80, pp. 90:1-90:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bonnet_et_al:LIPIcs.ICALP.2017.90,
  author =	{Bonnet, \'{E}douard and Gaspers, Serge and Lambilliotte, Antonin and R\"{u}mmele, Stefan and Saffidine, Abdallah},
  title =	{{The Parameterized Complexity of Positional Games}},
  booktitle =	{44th International Colloquium on Automata, Languages, and Programming (ICALP 2017)},
  pages =	{90:1--90:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-041-5},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{80},
  editor =	{Chatzigiannakis, Ioannis and Indyk, Piotr and Kuhn, Fabian and Muscholl, Anca},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.ICALP.2017.90},
  URN =		{urn:nbn:de:0030-drops-74941},
  doi =		{10.4230/LIPIcs.ICALP.2017.90},
  annote =	{Keywords: Hex, Maker-Maker games, Maker-Breaker games, Enforcer-Avoider games, parameterized complexity theory}
}
  • Refine by Author
  • 2 Saffidine, Abdallah
  • 1 Bonnet, Édouard
  • 1 Gaspers, Serge
  • 1 Jung, Jean Christoph
  • 1 Lambilliotte, Antonin
  • Show More...

  • Refine by Classification
  • 1 Hardware → Theorem proving and SAT solving
  • 1 Theory of computation → Constraint and logic programming

  • Refine by Keyword
  • 1 CNF Encodings
  • 1 Enforcer-Avoider games
  • 1 Hex
  • 1 Maker-Breaker games
  • 1 Maker-Maker games
  • Show More...

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2017
  • 1 2022

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