8
votes
Accepted
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 ...
- 16.9k
6
votes
Accepted
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. ...
- 504
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. ...
- 32.4k
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 ...
- 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 ...
- 216
1
vote
Accepted
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.
- 4,631
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/...
- 1,899
Only top scored, non community-wiki answers of a minimum length are eligible