# An easy case of SAT that is not easy for tree resolution

Is there a natural class $C$ of CNF formulas - preferably one that has previously been studied in the literature - with the following properties:

• $C$ is an easy case of SAT, like e.g. Horn or 2-CNF, i.e., membership in $C$ can be tested in polynomial time, and formulas $F\in C$ can be tested for satisfiability in polynomial time.
• Unsatisfiable formulas $F\in C$ are not known to have short (polynomial size) tree-like resolution refutations. Even better would be: there are unsatisfiable formulas in $C$ for which a super-polynomial lower bound for tree-like resolution is known.
• On the other hand, unsatisfiable formulas in $C$ are known to have short proofs in some stronger proof system, e.g. in dag-like resolution or some even stronger system.

$C$ should not be too sparse, i.e., contain many formulas with $n$ variables, for every (or at least for most values of) $n\in \mathbb{N}$. It should also be non-trivial, in the sense of containing satisfiable as well as unsatisfiable formulas.

The following approach to solving an arbitrary CNF formula $F$ should be meaningful: find a partial assignment $\alpha$ s.t. the residual formula $F\alpha$ is in $C$, and then apply the polynomial time algorithm for formulas in $C$ to $F\alpha$. Therefore I would like other answers besides the all-different constraints from the currently accepted answer, as I think it is rare that an arbitrary formula will become an all-different constraint after applying a restriction.

• Jan, I think it is still possible to give artificial examples, e.g. PHP union Horn. I am not sure how one can rule out such examples formally. Do you want some class which has a name and been studied? (ps: if you explain why you are looking for such a class that might help with what additional requirements the class should satisfy.) – Kaveh Jun 24 '13 at 17:34
• not sure about the last sentence. pigeonhole problems can have both true and false formulas, right? usually it is just the true formulas, not sure where the false formulas are in a paper, has anyone else seen it? a natural false pigeonhole formula would be one that attempts to assign $n+1$ pigeons to $n$ holes. – vzn Jun 25 '13 at 20:21
• @Kaveh, you are right, but one can probably never rule out artificial examples. I have tried to clarify the question a bit. – Jan Johannsen Jun 26 '13 at 15:16
• The desired condition in your last edit essentially asks for a hereditary class. Note that the direct encoding of all-different yields a hereditary class of SAT instances. Perhaps you could clarify why the main example we have (as suggested by three comments/answers) is not suitable? – András Salamon Jun 26 '13 at 16:04
• I think what Jan wants is a natural class of formulas, not a family of formulas. The difficulty is both "natural" and "class" are informal concepts. I guess one condition one can put for being a class is to require some level of expressiveness or closure so families of formulas like PHP do not count as a class. And for naturalness I think if the class has been studied previously or has a name then it is likely to be a natural one. – Kaveh Jun 26 '13 at 18:11

It sounds like you are interested in all-different constraints (and your last sentence is on the right track). These are non-trivial instances of the pigeonhole principle, where the number of pigeons is not necessarily greater than the number of holes, and in addition some pigeons may be barred from some of the holes.

All-different constraints can be decided by matching in low-order polynomial time.

When all-different constraints are expressed (using one of several encodings) as SAT instances, then conflict-driven clause learning usually quickly finds a solution if it exists. However, pure resolution for the PHP has to build a superpolynomially large set of clauses to show that the instance is unsatisfiable. This bound clearly holds for this more general problem. On the other hand, recall that Cook's encoding of the PHP allows polynomial-sized extended resolution refutations.

• S. A. Cook, A short proof of the pigeon hole principle using extended resolution, SIGACT News 8 28–32, 1976. doi:10.1145/1008335.1008338

Recent work along these lines is Chapter 5 of Sergi Oliva's thesis, which formed the basis of a paper with Alberto Atserias at CCC 2013.

I expect you are aware of Cook's classic result, so perhaps you meant to restrict the power of the proof system in your third condition?

• Not sure if that's what Jan is looking for as he asks specifically for CNF. – Mikolas Jun 26 '13 at 12:53
• @Mikolas: could you clarify what it is you are concerned about? – András Salamon Jun 26 '13 at 13:52
• I meant that if I have some result about all-different constraints, then it's not clear how this result translates to CNF. As I understand the questions, Jan wanted CNFs hard for tree-res but easy for something else (eg. dag-res). It's not clear to me also why PHP would be an example for this because PHP is exponential for dag-res as well. (BTW the referenced thesis looks neat!) – Mikolas Jun 26 '13 at 14:03
• @mikolas as I understand the question, if satisfiable/unsatisfiable instances of the family can be recognized in P time, but it is hard for tree or DAG resolution, that is what is sought. now am not sure this is pointed out in any papers, but afaik (anyone know more?), PHP sat/unsat instances can be recognized in P time. – vzn Jun 27 '13 at 20:30

I'm not sure why one would require also sat formulas but there are some articles on the separation between General and Tree resolution eg [1]. It sounds to me that this is what you want.

[1] Ben-Sasson, Eli, Russell Impagliazzo, and Avi Wigderson. "Near optimal separation of tree-like and general resolution." Combinatorica 24.4 (2004): 585-603.

• I am well aware of these separations between tree-like and dag-like resolution, but this gives just one family of formulas. This is precisely the sort of artificial example I was trying to avoid. – Jan Johannsen Jun 26 '13 at 15:25

You may be interested in SAT formulas with small (logarythmic) "bandwidth" or "treewidth". These formulas are recursively partitionable in such a way that the communication boundary between partitions is small, and therefore an enumerative dynamic programming approach can be used to solve them. The topic was popular in the nineties. I once counted exactly the number of hamiltonian cycles in a small treewidth graph of 24,000 vertices, so #P problems with small treewidth are solvable too. Bodlaender is a major reference.

• I think that at least formulas of constant tree-width have short tree-like resolution refutations. So I don't think this class meets the requirements of the question. – Jan Johannsen Sep 17 '14 at 12:21

this following paper seems close to what is requested in some ways (if it does not fit maybe JJ can clarify why). the question wants to rule out PHP (pigeonhole) instances based on the lack of both true/false formulas, but (as cited in the other answers) PHP is one of the most well-studied cases/instance generators from the theory side and has always been a generator for both satisfiable/unsatisfiable formulas although the satisfiable formulas are less emphasized/studied.

PHP${^m_n}$ where there are $m$ "pigeons" and $n$ "holes" is unsatisfiable (false) if $m>n$ and satisfiable if $m \leq n$. am not immediately familiar with papers that study both cases but think they exist (would like to hear of any). and some results/analyses that study only the unsatisfiable cases are naturally extended to include the satisfiable case.

another approach would be to go in a more empirical angle and just generate random instances (presumably around the easy-hard-easy 50% satisfiable transition point) and filter them to fit the criteria stated. one would require implementations of tree resolution/DAG resolution or "stronger systems".

• The same comment as the one on @Mikolas' answer applies here. – Jan Johannsen Jun 26 '13 at 15:26
• dont understand your comment, need more info. am following mikolas comment "As I understand the questions, Jan wanted CNFs hard for tree-res but easy for something else (eg. dag-res)." what do you mean by "this gives just one family of formulas"? your question is asking for a family of formulas. – vzn Jun 26 '13 at 16:02
• No, my question is asking for a class of formulas. The difference to me is that these formula families have at most one formula per number of variables, whereas a proper class should have many formulas for every number of variables, among those satisfiable and unsatisfiable ones. – Jan Johannsen May 26 '14 at 14:24
• I have already explained in several places (cf. the comment here and on other answers and on the question) why this is not what I'm looking for!! In particular, read the last paragraph of the question! – Jan Johannsen Sep 17 '14 at 7:50