Zobrazeno 1 - 10
of 30
pro vyhledávání: '"Peitl, Tomáš"'
We obtain the smallest unsatisfiable formulas in subclasses of $k$-CNF (exactly $k$ distinct literals per clause) with bounded variable or literal occurrences. Smaller unsatisfiable formulas of this type translate into stronger inapproximability resu
Externí odkaz:
http://arxiv.org/abs/2405.16149
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 ca
Externí odkaz:
http://arxiv.org/abs/2306.10427
Autor:
Peitl, Tomáš, Szeider, Stefan
Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other po
Externí odkaz:
http://arxiv.org/abs/2206.15225
Publikováno v:
In Artificial Intelligence November 2024 336
Publikováno v:
ACM Transactions on Computation Theory, Volume 16, Issue 2, Article No. 6 (March 2024)
We prove the first genuine QBF proof size lower bounds for the proof system Merge Resolution (MRes [Olaf Beyersdorff et al., 2020]), a refutational proof system for prenex quantified Boolean formulas (QBF) with a CNF matrix. Unlike most QBF resolutio
Externí odkaz:
http://arxiv.org/abs/2012.06779
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Autor:
Peitl, Tomáš, Szeider, Stefan
Publikováno v:
In Discrete Applied Mathematics 15 October 2023 337:173-184
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.
Publikováno v:
Journal of Automated Reasoning; Mar2024, Vol. 68 Issue 1, p1-31, 31p
Akademický článek
Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.
K zobrazení výsledku je třeba se přihlásit.