Skip to main content
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 ...
Emil Jeřábek's user avatar
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. ...
Jakob Nordstrom's user avatar
5 votes
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 ...
Emil Jeřábek's user avatar
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
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
  • 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 ...
Emil Jeřábek's user avatar
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.
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