<p>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.</p>

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

CC BY-SA 3.0
2013-06-26T15:25:04.600Z
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
CC BY-SA 3.0
2013-06-25T13:55:49.280Z
2013-06-25T13:55:49.280Z
Mikolas
<p>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.</p>

CC BY-SA 3.0
2014-09-17T12:21:40.733Z
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
CC BY-SA 3.0
2014-09-16T16:49:46.440Z
2014-09-16T16:49:46.440Z
daniel pehoushek
<p>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. </p>

<p>PHP${^m_n}$ where there are $m$ "pigeons" and $n$ "holes" is unsatisfiable (false) if $m&gt;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.</p>

<ul>
<li><a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.9531" rel="nofollow">Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle (1999)</a> by Kazuo Iwama , Shuichi Miyazaki</li>
</ul>

<p>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".</p>

CC BY-SA 3.0
2013-06-26T15:26:16.857Z
The same comment as the one on @Mikolas' answer applies here.
Jan Johannsen
CC BY-SA 3.0
2013-06-26T16:02:03.980Z
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
CC BY-SA 3.0
2014-05-26T14:24:15.417Z
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
CC BY-SA 3.0
2014-09-17T07:50:59.087Z
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
CC BY-SA 3.0
2013-06-26T15:12:03.350Z
2013-06-26T15:12:03.350Z
vzn
<p>It sounds like you are interested in <em>all-different constraints</em> (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.</p>

<p>All-different constraints can be decided by matching in low-order polynomial time.</p>

<ul>
<li>Jean-Charles Régin, <a href="http://www.aaai.org/Library/AAAI/1994/aaai94-055.php"><em>A filtering algorithm for constraints of difference in CSPs</em></a>, AAAI 1994, 362–367.</li>
<li>D. E. Knuth and A. Raghunathan, <em>The problem of compatible representatives</em>, SIAM J. Discrete Math. <strong>5</strong> 422–427, 1992.  doi:<a href="http://dx.doi.org/10.1137/0405033">10.1137/0405033</a></li>
</ul>

<p>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 <em>extended</em> resolution refutations.</p>

<ul>
<li>S. A. Cook, <em>A short proof of the pigeon hole principle using extended resolution</em>, SIGACT News <strong>8</strong> 28–32, 1976.  doi:<a href="http://dx.doi.org/10.1145/1008335.1008338">10.1145/1008335.1008338</a></li>
</ul>

<p>Recent work along these lines is Chapter 5 of <a href="http://www.lsi.upc.edu/~oliva/phdthesis.pdf">Sergi Oliva's thesis</a>, which formed the basis of a paper with Alberto Atserias at CCC 2013.</p>

<p>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?</p>

CC BY-SA 3.0
2013-06-26T12:53:06.257Z
Not sure if that's what Jan is looking for as he asks specifically for CNF.
Mikolas
CC BY-SA 3.0
2013-06-26T13:52:43.057Z
@Mikolas: could you clarify what it is you are concerned about?
András Salamon
CC BY-SA 3.0
2013-06-26T14:03:51.113Z
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
CC BY-SA 3.0
2013-06-27T20:30:42.017Z
@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
CC BY-SA 3.0
2013-06-26T09:43:44.223Z
2013-06-27T18:54:44.360Z
2013-06-27T18:54:44.360Z
András Salamon
<p>Is there a natural class $C$ of CNF formulas - preferably one that has previously been studied in the literature - with the following properties:</p>

<ul>
<li>$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. </li>
<li>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. </li>
<li>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. </li>
</ul>

<p>$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.</p>

<p>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 <em>all-different constraints</em> 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. </p>

CC BY-SA 3.0
2013-06-24T17:34:52.410Z
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
CC BY-SA 3.0
2013-06-25T20:21:44.220Z
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
CC BY-SA 3.0
2013-06-26T15:16:46.870Z
@Kaveh, you are right, but one can probably never rule out artificial examples. I have tried to clarify the question a bit.
Jan Johannsen
CC BY-SA 3.0
2013-06-26T16:04:08.487Z
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
CC BY-SA 3.0
2013-06-26T16:20:36.027Z
András, whar does hereditary mean in this context? I will have to look at all-different constraints, but at first glance it seems to be rather narrow. Can a restriction yield an encoding of all-different if the original formula wasn't already one?
Jan Johannsen
CC BY-SA 3.0
2013-06-26T18:11:01.140Z
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
CC BY-SA 3.0
2013-06-26T19:00:18.523Z
Constraint programming has been (facetiously) defined as the study of the all-different constraint.  So it seems pretty natural and class-like from my perspective.  A clearer definition of "natural" and "class" might be helpful here.
András Salamon
CC BY-SA 3.0
2013-06-27T20:26:00.353Z
Hereditary means the class of clause hypergraphs (vertices are literals, edges are clauses) is closed under removal of literals (and any clauses involving a removed literal).
András Salamon
CC BY-SA 3.0
2014-06-04T18:47:42.273Z
You might be interested in the following problem. Given a 3SAT instance, is there a satisfying assignment such that each clause is satisfied at least twice? This can be solved in polynomial time using 2SAT, but a resolution proof of unsatisfiability could still be long.
Russell Easterly
<sat><proof-complexity>
An easy case of SAT that is not easy for tree resolution
Jan Johannsen
# An easy case of SAT that is not easy for tree resolution

(Asked by: username_0 on 2013-06-24)

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.

**Tags:** sat, proof-complexity

> **Comments:**
> **username_1**: 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.)  
> **username_2**: 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.  
> **username_0**: @username_1, you are right, but one can probably never rule out artificial examples. I have tried to clarify the question a bit.  
> **username_3**: 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?  
> **username_0**: András, whar does hereditary mean in this context? I will have to look at all-different constraints, but at first glance it seems to be rather narrow. Can a restriction yield an encoding of all-different if the original formula wasn't already one?  
> **username_1**: 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.  
> **username_3**: Constraint programming has been (facetiously) defined as the study of the all-different constraint.  So it seems pretty natural and class-like from my perspective.  A clearer definition of "natural" and "class" might be helpful here.  
> **username_3**: Hereditary means the class of clause hypergraphs (vertices are literals, edges are clauses) is closed under removal of literals (and any clauses involving a removed literal).  
> **username_4**: You might be interested in the following problem. Given a 3SAT instance, is there a satisfying assignment such that each clause is satisfied at least twice? This can be solved in polynomial time using 2SAT, but a resolution proof of unsatisfiability could still be long.  

---

## 4 answers

### Answer by username_3 on 2013-06-26. Score: 10 | Accepted answer

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.

* Jean-Charles Régin, [*A filtering algorithm for constraints of difference in CSPs*](http://www.aaai.org/Library/AAAI/1994/aaai94-055.php), AAAI 1994, 362–367.
* D. E. Knuth and A. Raghunathan, *The problem of compatible representatives*, SIAM J. Discrete Math. **5** 422–427, 1992. doi:[10.1137/0405033](http://dx.doi.org/10.1137/0405033)

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](http://dx.doi.org/10.1145/1008335.1008338)

Recent work along these lines is Chapter 5 of [Sergi Oliva's thesis](http://www.lsi.upc.edu/~oliva/phdthesis.pdf), 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?

> **Comments:**
> **username_5**: Not sure if that's what Jan is looking for as he asks specifically for CNF.  
> **username_3**: @username_5: could you clarify what it is you are concerned about?  
> **username_5**: 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!)  
> **username_2**: @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.  

---

### Answer by username_5 on 2013-06-25. Score: 1

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.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_6 on 2014-09-16. Score: 0

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.

> **Comments:**
> **username_0**: 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.  

---

### Answer by username_2 on 2013-06-26. Score: -1

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.

* [Tree-Like Resolution Is Superpolynomially Slower Than DAG-Like Resolution for the Pigeonhole Principle (1999)](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.45.9531) by Kazuo Iwama , Shuichi Miyazaki

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

> **Comments:**
> **username_0**: The same comment as the one on @username_5' answer applies here.  
> **username_2**: 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.  
> **username_0**: 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.  
> **username_0**: 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!  

---

