# Tag Info

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 ...
• 17.8k
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. ...
Accepted

### Horn clause on cnf

Yes, any unsatisfiable Horn CNF has a tree-like resolution refutation with a linear number of clauses. Consider the standard poly-time Horn-SAT algorithm, which works as follows. First, set all ...
• 17.8k

### 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 ...

### 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.6k

### 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 ...
• 316
1 vote
Accepted

### Max number of k-clauses such that no two clauses can be resolved?

For any $0<k\le n$, the maximal size of such a set of clauses is $$\binom nk2^{k-1},$$ i.e., $1/2$ of the number of all $k$-clauses. (I’m assuming a clause cannot contain any variable both ...
• 17.8k
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,630
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,889

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