8 votes

What kind of resolution is CDCL corresponding to?

CDCL with restarts is more or less equivalent to general resolution, see Pipatsrisawat & Darwiche. CDCL without restarts is more difficult to pin down. It sits somewhere between regular and ...
Emil Jeřábek's user avatar
6 votes

Axioms of Minimum Size Resolution Refutations

With the caveat that I am posting this quickly in a sleep-deprived state, I think the answer is "no" to all three questions. Take the pigeonhole principle formulas PHP^m_n for m pigeons and n holes. ...
Jakob Nordstrom's user avatar
2 votes

resolution based theorem prover for temporal logic

Your translation goes into Presburger arithmetic, which is decidable. You could take your translated formula, do quantifier elimination on it, and then hand it over to a proof-producing SMT solver. ...
Neel Krishnaswami's user avatar
2 votes

Direct Proof that the Pigeonhole Principle is Hard for Regular Resolution

It’s amazing that your question matches the papers I have recently read. For Tseitin formulas, there are papers that obtain regular resolution lower bounds from corresponding read-once branching ...
Jxb's user avatar
  • 315
2 votes

Methods for Determining the minimal Width of Resolution Refutations for CNF Formulas

Partially answering question (2), the Prover-Delayer game of Atserias and Dalmau can be interpreted as a more general "dag-like query complexity" specialized to CNFs. See e.g. GGKS'18. And ...
notautogenerated's user avatar
1 vote

Eliminating tautological axioms in tree-like $k$-DNF resolution

Since I could not find a proof in the literature, I wrote a short note containing the proof.
Jan Johannsen's user avatar
1 vote

Resolution vs Nondeterministic Search Problems

If I understood correctly the question, the so-called Buss-Pudlak game provides a simple transformation from a proof system to such a decision tree (see Buss-Pudlak '94 http://math.cas.cz/%7Epudlak/...
Iddo Tzameret's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible