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

Question

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.

Answer 1

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, 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

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?

Answer 2

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.

Answer 3

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.

Answer 4

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