Zobrazeno 1 - 10
of 28
pro vyhledávání: '"Friedrich Slivovsky"'
Autor:
Leroy Chew, Friedrich Slivovsky
Publikováno v:
Logical Methods in Computer Science, Vol Volume 20, Issue 1 (2024)
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:
https://doaj.org/article/65f49f315e454d73aeea8f4e3455088a
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 11:261-272
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226
SAT
SAT
Davis-Putnam resolution is one of the fundamental theoretical decision procedures for both propositional logic and quantified Boolean formulas.
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::036aab56afdcd4b3527c456bb35404c7
https://doi.org/10.1007/978-3-030-80223-3_4
https://doi.org/10.1007/978-3-030-80223-3_4
Autor:
Stefan Mengel, Friedrich Slivovsky
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226
SAT
24th International Conference Theory and Applications of Satisfiability Testing (SAT 2021)
24th International Conference Theory and Applications of Satisfiability Testing (SAT 2021), Jul 2021, Barcelona, Spain. pp.399-416, ⟨10.1007/978-3-030-80223-3_28⟩
SAT
24th International Conference Theory and Applications of Satisfiability Testing (SAT 2021)
24th International Conference Theory and Applications of Satisfiability Testing (SAT 2021), Jul 2021, Barcelona, Spain. pp.399-416, ⟨10.1007/978-3-030-80223-3_28⟩
We introduce and investigate symbolic proof systems for Quantified Boolean Formulas (QBF) operating on Ordered Binary Decision Diagrams (OBDDs). These systems capture QBF solvers that perform symbolic quantifier elimination, and as such admit short p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::66e0483b6152878b33d6267306876de0
https://doi.org/10.1007/978-3-030-80223-3_28
https://doi.org/10.1007/978-3-030-80223-3_28
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2021 ISBN: 9783030802226
SAT
SAT
We propose a new decision procedure for dependency quantified Boolean formulas (DQBFs) that uses interpolation-based definition extraction to compute Skolem functions in a counter-example guided inductive synthesis (CEGIS) loop. In each iteration, a
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::317b55b0b96195e2317d17db98bc0d68
https://doi.org/10.1007/978-3-030-80223-3_34
https://doi.org/10.1007/978-3-030-80223-3_34
Publikováno v:
KR
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
Autor:
Friedrich Slivovsky, Stefan Szeider
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2020 ISBN: 9783030518240
SAT
SAT
The propositional model counting problem (#SAT) is known to be fixed-parameter-tractable (FPT) when parameterized by the width k of a given tree decomposition of the incidence graph. The running time of the fastest known FPT algorithm contains the ex
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::7968e395fb0529d2e0bf932fca45ae5b
https://doi.org/10.1007/978-3-030-51825-7_19
https://doi.org/10.1007/978-3-030-51825-7_19
Autor:
Friedrich Slivovsky
Publikováno v:
Computer Aided Verification ISBN: 9783030532871
CAV (1)
CAV (1)
We present a new semantic gate extraction technique for propositional formulas based on interpolation. While known gate detection methods are incomplete and rely on pattern matching or simple semantic conditions, this approach can detect any definiti
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::de044304cd0c2d070876566b4add17b8
https://doi.org/10.1007/978-3-030-53288-8_24
https://doi.org/10.1007/978-3-030-53288-8_24
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2020 ISBN: 9783030518240
SAT
SAT
We introduce new proof systems for quantified Boolean formulas (QBFs) by enhancing Q-resolution systems with rules which exploit local and global symmetries. The rules are based on homomorphisms that admit non-injective mappings between literals. Thi
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::31c5b08e9588a08008fe618db8a520b0
https://doi.org/10.1007/978-3-030-51825-7_29
https://doi.org/10.1007/978-3-030-51825-7_29
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030242572
SAT
SAT
We present the first practical implementation of the reflexive resolution-path dependency scheme in a QBF solver. Unlike in DepQBF, which uses the less general standard dependency scheme, we do not compute the dependency relation upfront, but instead
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::44e4f366e0c8385cbc04fe683a9e1c50
https://doi.org/10.1007/978-3-030-24258-9_22
https://doi.org/10.1007/978-3-030-24258-9_22