Exploració per tema "Proof complexity"
Ara es mostren els items 1-13 de 13
-
Circular (yet sound) proofs in propositional logic
(Association for Computing Machinery (ACM), 2023-07)
Article
Accés obertProofs in propositional logic are typically presented as trees of derived formulas or, alternatively, as directed acyclic graphs of derived formulas. This distinction between tree-like vs. dag-like structure is particularly ... -
Clique is hard on average for regular resolution
(Association for Computing Machinery (ACM), 2018)
Text en actes de congrés
Accés obertWe prove that for k ≪4√n regular resolution requires length nΩ(k) to establish that an Erdős–Rényi graph with appropriately chosen edge density does not contain a k-clique. This lower bound is optimal up to the multiplicative ... -
Feasible interpolation for polynomial calculus and sums-of-squares
(Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020)
Text en actes de congrés
Accés obertWe prove that both Polynomial Calculus and Sums-of-Squares proof systems admit a strong form of feasible interpolation property for sets of polynomial equality constraints. Precisely, given two sets P(x, z) and Q(y, z) of ... -
Feasibly constructive proofs of succinct weak circuit lower bounds
(2020-02)
Article
Accés obertWe ask for feasibly constructive proofs of known circuit lower bounds for explicit functions on bit strings of length n. In 1995 Razborov showed that many can be proved in PV1, a bounded arithmetic formalizing polynomial ... -
Lower bounds for DNF-refutations of a relativized weak pigeonhole principle
(2015-06-01)
Article
Accés obertThe relativized weak pigeonhole principle states that if at least 2n out of n(2) pigeons fly into n holes, then some hole must be doubly occupied. We prove that every DNF-refutation of the CNF encoding of this principle ... -
Narrow proofs may be maximally long
(2016-07-03)
Article
Accés obertWe prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n(Omega(w)). This shows that the simple counting argument that any formula refutable ... -
Narrow proofs may be maximally long
(Institute of Electrical and Electronics Engineers (IEEE), 2014)
Text en actes de congrés
Accés obertWe prove that there are 3-CNF formulas over n variables that can be refuted in resolution in width w but require resolution proofs of size n¿(w). This shows that the simple counting argument that any formula refutable in ... -
Partially definable forcing and bounded arithmetic
(2015-02-01)
Article
Accés obertWe describe a method of forcing against weak theories of arithmetic and its applications in propositional proof complexity. -
Proof complexity for the maximum satisfiability problem and its use in SAT refutations
(Oxford University Press, 2022-10)
Article
Accés obertMaxSAT, the optimization version of the well-known SAT problem, has attracted a lot of research interest in the past decade. Motivated by the many important applications and inspired by the success of modern SAT solvers, ... -
Proof complexity meets algebra
(Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017)
Text en actes de congrés
Accés obertWe analyse how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional and semi-algebraic proof systems, the classical constructions ... -
Proof complexity meets algebra
(2018-12-01)
Article
Accés obertWe analyze how the standard reductions between constraint satisfaction problems affect their proof complexity. We show that, for the most studied propositional, algebraic, and semialgebraic proof systems, the classical ... -
Resolution lower bounds for refutation statements
(Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019)
Text en actes de congrés
Accés obertFor any unsatisfiable CNF formula we give an exponential lower bound on the size of resolutionrefutations of a propositional statement that the formula has a resolution refutation. We describethree applications. (1) An ... -
Size-degree trade-offs for Sums-of-Squares and Positivstellensatz proofs
(Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019)
Text en actes de congrés
Accés obertWe show that if a system of degree-k polynomial constraints on n Boolean variables has a Sums-of-Squares (SOS) proof of unsatisfiability with at most s many monomials, then it also has one whose degree is of the order of ...
