New answers tagged proof-complexity
5
votes
Accepted
Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?
It is indeed and here is the reference for it if needed:
Pipatsrisawat, K., & Darwiche, A. (2011). On the power of clause-learning SAT solvers as resolution engines. Artificial intelligence, 175(2)...
8
votes
Do we currently know a polynomial-size Frege proof for Tseitin formulas?
Tseitin tautologies are unsatisfiable systems of linear equations over $\mathbb F_2$, and as such they can be refuted just by summing all the equations together (possibly after reconstructing the ...
8
votes
Accepted
Do we currently know a polynomial-size Frege proof for Tseitin formulas?
Section 6 of the following paper has a sketch:
Alasdair Urquhart. Hard examples for resolution. Journal of the ACM,
34(1):209–219, 1987. DOI: https://doi.org/10.1145/7531.8928
Top 50 recent answers are included
Related Tags
proof-complexity × 79cc.complexity-theory × 40
lo.logic × 24
reference-request × 17
sat × 15
proof-theory × 7
resolution × 7
complexity-classes × 4
descriptive-complexity × 4
graph-theory × 3
np × 3
automated-theorem-proving × 3
first-order-logic × 3
np-hardness × 2
computability × 2
polynomials × 2
open-problem × 2
algebraic-complexity × 2
boolean-formulas × 2
sum-of-squares × 2
proof-search × 2
feasible-interpolation × 2
ds.algorithms × 1
graph-algorithms × 1
fl.formal-languages × 1