Zobrazeno 1 - 10
of 38
pro vyhledávání: '"CHEW, LEROY"'
Parity reasoning is challenging for Conflict-Driven Clause Learning (CDCL) SAT solvers. This has been observed even for simple formulas encoding two contradictory parity constraints with different variable orders (Chew and Heule 2020). We provide an
Externí odkaz:
http://arxiv.org/abs/2402.00542
Autor:
Chew, Leroy, Slivovsky, Friedrich
Publikováno v:
Logical Methods in Computer Science, Volume 20, Issue 1 (February 13, 2024) lmcs:10146
We pioneer a new technique that allows us to prove a multitude of previously open simulations in QBF proof complexity. In particular, we show that extended QBF Frege p-simulates clausal proof systems such as IR-Calculus, IRM-Calculus, Long-Distance Q
Externí odkaz:
http://arxiv.org/abs/2210.07085
Ramsey Theory deals with avoiding certain patterns. When constructing an instance that avoids one pattern, it is observed that other patterns emerge. For example, repetition emerges when avoiding arithmetic progression (Van der Waerden numbers), whil
Externí odkaz:
http://arxiv.org/abs/2012.12582
Autor:
Chew, Leroy Nicholas
Quantified Boolean Formulas (QBF) and their proof complexity are not as well understood as propositional formulas, yet remain an area of interest due to their relation to QBF solving. Proof systems for QBF provide a theoretical underpinning for the p
Externí odkaz:
https://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.723199
Publikováno v:
Logical Methods in Computer Science, Volume 13, Issue 2 (June 8, 2017) lmcs:2198
In sharp contrast to classical proof complexity we are currently short of lower bound techniques for QBF proof systems. In this paper we establish the feasible interpolation technique for all resolution-based QBF systems, whether modelling CDCL or ex
Externí odkaz:
http://arxiv.org/abs/1611.01328
We examine the existing Resolution systems for quantified Boolean formulas (QBF) and answer the question which of these calculi can be lifted to the more powerful Dependency QBFs (DQBF). An interesting picture emerges: While for QBF we have the stric
Externí odkaz:
http://arxiv.org/abs/1604.08058
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:
Beyersdorff, Olaf, Chew, Leroy
In this paper we compare two proof systems for minimal entailment: a tableau system OTAB and a sequent calculus MLK, both developed by Olivetti (1992). Our main result shows that OTAB-proofs can be efficiently translated into MLK-proofs, i.e; MLK p-s
Externí odkaz:
http://arxiv.org/abs/1405.1565
Publikováno v:
In Journal of Computer and System Sciences September 2019 104:82-101
Publikováno v:
In Information and Computation October 2018 262 Part 1:141-161