Author name cluster

Tomáš Peitl

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

9 papers

1 author row

AAAI Conference 2026 Conference Paper

Graph Choosability via SAT: Beyond the Nullstellensatz

Markus Kirchweger
Tomáš Peitl
David Seka
Stefan Szeider

List coloring extends graph coloring by assigning each vertex a list of allowed colors. A graph is k-choosable if it can be properly colored for any choice of lists with k colors each. Deciding k-choosability is π²ₚ-complete, bipartite graphs have unbounded list chromatic number, and planar graphs (famously 4-colorable) are all 5-choosable but not all 4-choosable. To search for graphs of given choosability, we extend SAT Modulo Symmetries (SMS) with custom propagators for list coloring pruning techniques and propose a quantified Boolean (QBF) encoding for choosability. We employ a hybrid approach: pen-and-paper reasoning to optimize our formulas followed by automated case distinction by QBF solvers and SMS. Our methods yield two significant results: (1) a 27-vertex planar graph that is 4-choosable yet cannot be proven so using the combinatorial Nullstellensatz widely applied in previous work (we show this is a smallest graph with that property), and (2) the smallest graph exhibiting a gap between chromatic and list chromatic numbers for chromatic number 3.

PDF Details DOI

AAAI Conference 2025 Conference Paper

Breaking Symmetries in Quantified Graph Search: A Comparative Study

Mikoláš Janota
Markus Kirchweger
Tomáš Peitl
Stefan Szeider

Graph generation and enumeration problems often require handling equivalent graphs---those that differ only in vertex labeling. We study how to extend SAT Modulo Symmetries (SMS), a framework for eliminating such redundant graphs, to handle more complex constraints. While SMS was originally designed for constraints in propositional logic (in NP), we now extend it to handle quantified Boolean formulas (QBF), allowing for more expressive specifications like non-3-colorability (a coNP-complete property). We develop two approaches: a static QBF encoding and a dynamic method integrating SMS into QBF solvers. Our analysis reveals that while specialized approaches can be faster, QBF-based methods offer easier implementation and formal verification capabilities.

PDF Details DOI

AIJ Journal 2024 Journal Article

QCDCL with cube learning or pure literal elimination – What is best?

Benjamin Böhm
Tomáš Peitl
Olaf Beyersdorff

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving variants via proof complexity techniques. Our results show that almost all of the QCDCL variants are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.

Details DOI

IJCAI Conference 2023 Conference Paper

Co-Certificate Learning with SAT Modulo Symmetries

Markus Kirchweger
Tomáš Peitl
Stefan Szeider

We present a new SAT-based method for generating all graphs up to isomorphism that satisfy a given co-NP property. Our method extends the SAT Modulo Symmetry (SMS) framework with a technique that we call co-certificate learning. If SMS generates a candidate graph that violates the given co-NP property, we obtain a certificate for this violation, i. e. , `co-certificate' for the co-NP property. The co-certificate gives rise to a clause that the SAT solver, serving as SMS's backend, learns as part of its CDCL procedure. We demonstrate that SMS plus co-certificate learning is a powerful method that allows us to improve the best-known lower bound on the size of Kochen-Specker vector systems, a problem that is central to the foundations of quantum mechanics and has been studied for over half a century. Our approach is orders of magnitude faster and scales significantly better than a recently proposed SAT-based method.

PDF Details DOI

IJCAI Conference 2022 Conference Paper

QCDCL with Cube Learning or Pure Literal Elimination - What is Best?

Benjamin Böhm
Tomáš Peitl
Olaf Beyersdorff

Quantified conflict-driven clause learning (QCDCL) is one of the main approaches for solving quantified Boolean formulas (QBF). We formalise and investigate several versions of QCDCL that include cube learning and/or pure-literal elimination, and formally compare the resulting solving models via proof complexity techniques. Our results show that almost all of the QCDCL models are exponentially incomparable with respect to proof size (and hence solver running time), pointing towards different orthogonal ways how to practically implement QCDCL.

PDF Details DOI

JAIR Journal 2021 Journal Article

Finding the Hardest Formulas for Resolution

Tomáš Peitl
Stefan Szeider

A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. In this paper we introduce resolution hardness numbers; they give for m=1,2,... the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest for- mulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

PDF Details DOI

IJCAI Conference 2021 Conference Paper

Finding the Hardest Formulas for Resolution (Extended Abstract)

Tomáš Peitl
Stefan Szeider

A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. We introduce resolution hardness numbers; they give for m=1, 2, .. . the length of a shortest proof of a hardest formula on m clauses. We compute the first ten resolution hardness numbers, along with the corresponding hardest formulas. To achieve this, we devise a candidate filtering and symmetry breaking search scheme for limiting the number of potential candidates for hardest formulas, and an efficient SAT encoding for computing a shortest resolution proof of a given candidate formula.

PDF Details DOI

KR Conference 2020 Conference Paper

Fixed-Parameter Tractability of Dependency QBF with Structural Parameters

Robert Ganian
Tomáš Peitl
Friedrich Slivovsky
Stefan Szeider

We study dependency quantified Boolean formulas (DQBF), an extension of QBF in which dependencies of existential variables are listed explicitly rather than being implicit in the order of quantifiers. DQBF evaluation is a canonical NEXPTIME-complete problem, a complexity class containing many prominent problems that arise in Knowledge Representation and Reasoning. One approach for solving such hard problems is to identify and exploit structural properties captured by numerical parameters such that bounding these parameters gives rise to an efficient algorithm. This idea is captured by the notion of fixed-parameter tractability (FPT). We initiate the study of DQBF through the lens of fixed-parameter tractability and show that the evaluation problem becomes FPT under two natural parameterizations: the treewidth of the primal graph of the DQBF instance combined with a restriction on the interactions between the dependency sets, and also the treedepth of the primal graph augmented by edges representing dependency sets.

PDF Details DOI

JAIR Journal 2019 Journal Article

Dependency Learning for QBF

Tomáš Peitl
Friedrich Slivovsky
Stefan Szeider

Quantified Boolean Formulas (QBFs) can be used to succinctly encode problems from domains such as formal verification, planning, and synthesis. One of the main approaches to QBF solving is Quantified Conflict Driven Clause Learning (QCDCL). By default, QCDCL assigns variables in the order of their appearance in the quantifier prefix so as to account for dependencies among variables. Dependency schemes can be used to relax this restriction and exploit independence among variables in certain cases, but only at the cost of nontrivial interferences with the proof system underlying QCDCL. We introduce dependency learning, a new technique for exploiting variable independence within QCDCL that allows solvers to learn variable dependencies on the fly. The resulting version of QCDCL enjoys improved propagation and increased flexibility in choosing variables for branching while retaining ordinary (long-distance) Q-resolution as its underlying proof system. We show that dependency learning can achieve exponential speedups over ordinary QCDCL. Experiments on standard benchmark sets demonstrate the effectiveness of this technique.

PDF Details DOI