Zobrazeno 1 - 10
of 14
pro vyhledávání: '"Tomáš Peitl"'
Autor:
Stefan Szeider, Tomáš Peitl
Publikováno v:
Journal of Artificial Intelligence Research. 72:69-97
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 for
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::0c21b45a7118bfcfe1d7909392300b1f
https://doi.org/10.1613/jair.1.12589
https://doi.org/10.1613/jair.1.12589
Autor:
Tomáš Peitl, Stefan Szeider
Publikováno v:
IJCAI
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 clau
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::f73c1821d72c36faddc69b314ed0f3a9
https://doi.org/10.24963/ijcai.2021/657
https://doi.org/10.24963/ijcai.2021/657
Publikováno v:
Journal on Satisfiability, Boolean Modeling and Computation. 11:261-272
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::e457b4ce70a1f775055ca8bd404a01f8
https://doi.org/10.3233/sat190124
https://doi.org/10.3233/sat190124
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
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
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::24e96c5b847d9c327c227a0f5b6df50e
https://doi.org/10.24963/kr.2020/40
https://doi.org/10.24963/kr.2020/40
Publikováno v:
Theory and Applications of Satisfiability Testing – SAT 2020 ISBN: 9783030518240
SAT
SAT
We suggest a general framework to study dependency schemes for dependency quantified Boolean formulas (DQBF). As our main contribution, we exhibit a new tautology-free DQBF dependency scheme that generalises the reflexive resolution path dependency s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::cccaa7c86b6f828509c1e61f9ba54f4f
https://doi.org/10.1007/978-3-030-51825-7_28
https://doi.org/10.1007/978-3-030-51825-7_28
Autor:
Tomáš Peitl, Stefan Szeider
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030584740
CP
CP
A CNF formula is harder than another CNF formula with the same number of clauses if it requires a longer resolution proof. The resolution hardness numbers give for \(m=1,2,\dots \) the length of a shortest proof of a hardest formula on m clauses. We
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a27ce67f86e9514031ed0e7e152fece4
https://doi.org/10.1007/978-3-030-58475-7_30
https://doi.org/10.1007/978-3-030-58475-7_30
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
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030242572
SAT
SAT
Q-resolution is perhaps the most well-studied proof system for Quantified Boolean Formulas (QBFs). Its proof complexity is by now well understood, and several general proof size lower bound techniques have been developed. The situation is quite diffe
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::5158a2cef46001861ecbc3e7e78b9f06
https://doi.org/10.1007/978-3-030-24258-9_23
https://doi.org/10.1007/978-3-030-24258-9_23
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783319983332
CP
CP
Quantified Boolean Formulas (QBFs) are a generalization of propositional formulae that admits succinct encodings of verification and synthesis problems. Given that modern QBF solvers are based on different architectures with complementary performance
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::38bc362cb9392e65128473888ca928a2
https://doi.org/10.1007/978-3-319-98334-9_13
https://doi.org/10.1007/978-3-319-98334-9_13