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)...
- 2,164
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 ...
- 16.9k
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
- 286
Top 50 recent answers are included