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
4 votes

Can CDCL Algorithm Derived Conflict Clauses Always Be Obtained Through Resolution from an Unsatisfiable CNF Formula?

Yes, anything learned by conflict analysis in conflict-driven clause learning can be derived by resolution from the original formula. The technically slightly more precise claim is that any newly ...
Jakob Nordstrom's user avatar

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