Valentin Mayer-Eichberger

SAT Conference 2022 Conference Paper

QBF Programming with the Modeling Language Bule

• Jean Christoph Jung
• Valentin Mayer-Eichberger
• Abdallah Saffidine

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.

SAT Conference 2020 Conference Paper

Positional Games and QBF: The Corrective Encoding

• Valentin Mayer-Eichberger
• Abdallah Saffidine

Abstract Positional games are a mathematical class of two-player games comprising Tic-tac-toe and its generalizations. We propose a novel encoding of these games into Quantified Boolean Formulas (QBFs) such that a game instance admits a winning strategy for first player if and only if the corresponding formula is true. Our approach improves over previous QBF encodings of games in multiple ways. First, it is generic and lets us encode other positional games, such as Hex. Second, structural properties of positional games together with a careful treatment of illegal moves let us generate more compact instances that can be solved faster by state-of-the-art QBF solvers. We establish the latter fact through extensive experiments. Finally, the compactness of our new encoding makes it feasible to translate realistic game problems. We identify a few such problems of historical significance and put them forward to the QBF community as milestones of increasing difficulty.

IJCAI Conference 2016 Conference Paper

Modelling Satisfiability Problems: Theory and Practice

• Valentin Mayer-Eichberger

Boolean Satisfiability (SAT) solvers are a mature technology to solve hard combinatorial problems. The input to a SAT solver is the problem translated to propositional logic in conjunctive normal form (CNF). This thesis studies such translations and aims to make SAT solvers more accessible to non-encoding experts.

AAAI Conference 2015 Conference Paper

Just-in-Time Hierarchical Constraint Decomposition

• Valentin Mayer-Eichberger