We know that DPLL based SAT-solvers fail to answer correctly on unsatisfiable instances of $\mathrm{PHP}$ (pigeon hole principle), e.g. on "there is a injective mapping from $n+1$ to $n$":

$$\mathrm{PHP^{n+1}_{n}} := \left(\bigwedge_{i\in[n+1]} \ \bigvee_{j\in[n]} \ p_{i,j}\right) \wedge \left(\bigwedge_{i\neq i'\in[n+1]} \ \bigwedge_{j\in[n]} \ (\lnot p_{i,j} \vee \lnot p_{i',j})\right)$$

I am looking for results about how they perform on satisfiable instances of $\mathrm{PHP}$, e.g. on "there is a injective mapping from $n$ to $n$".

Do they find a satisfying assignment quickly on such instances?

  • 1
    $\begingroup$ By "fail to answer correctly" do you mean "run out of resources on sufficiently large values of n" ? $\endgroup$
    – Vijay D
    Jul 22, 2012 at 8:44
  • $\begingroup$ @Kaveh Are you allowing repetition of clauses and/or repetition of variables in the same clause? Thanks $\endgroup$
    – Tayfun Pay
    Jul 22, 2012 at 18:26
  • $\begingroup$ @VijayD, I mean the algorithm does not return a correct answer in polynomial time for large enough $n$. I am hoping that one can provably show that a DPLL-based algorithm would work in polynomial time on this family. $\endgroup$
    – Kaveh
    Jul 22, 2012 at 20:26
  • $\begingroup$ @Geekster, I am not sure what you mean. I have a particular family of formulas. Are you asking if there is repetition in that formula? $\endgroup$
    – Kaveh
    Jul 22, 2012 at 20:28

1 Answer 1


On satisfiable instances of $PHP$, DPLL based SAT solvers will furnish a satisfying assignment in linear time.

To see why, observe how the CNF encoding of an unsatisfiable instance of $PHP$ with $n$ holes and $n + 1$ pigeons is sintactically identical to an instance of $k = n$ Graph Coloring, where the input graph is a clique of $n + 1$ vertices.

Similarly, the CNF encoding of a satisfiable instance of $PHP$ with $n$ holes and $n$ pigeons is sintactically identical to an instance of $k = n$ Graph Coloring, where the input graph is a clique of $n$ vertices.

Now, coloring a clique of $n$ vertices with $n$ colors is straightforward: scan the vertices, and assign to each of them one of the remaining colors (already assigned colors are automatically ruled out by the clique-ness of the graph, using unit propagation). Whatever of the remaining colors you choose, it will be good and will lead you to a satisfying assignment.

From the DPLL solver point of view: each time it will try to guess the boolean value of a variable $v_i$, such value will be right (whatever it is), because there will certainly be a satisfying assignment in which variable $v_i$ has the guessed value. Unit propagation will do the rest of the job, by guiding the solver along the satisfying path (in other words: by preventing it to guess wrong values).

The search then proceeds one variable after the other, linearly, each time making the correct guess.

  • $\begingroup$ Thank you, this is what I was expecting. By the way, do you know a reference that states this (i.e. "DPLL algorithm solves the satisfiable instances of PHP/GC in linear time")? $\endgroup$
    – Kaveh
    Jul 23, 2012 at 19:23
  • 1
    $\begingroup$ You are welcome. I don't know any reference that states this, I've just derived it by myself through some raw reasoning. It should not be difficult to formally prove it, by relying on the fact that every SAT solver uses some reasonable heuristic both in picking the next variable and in guessing its boolean value. It must be observed, in fact, that there exists at least one unreasonable heuristic that prevents us to reach a solution in linear time (such an unreasonable heuristic would be to set to false every variable, until possible). While with a reasonable heuristic, linear time is ensured. $\endgroup$ Jul 23, 2012 at 20:31
  • $\begingroup$ I agree. I am hoping that someone might have stated this somewhere so I can cite when I need. I would like to wait a few more days and if no one gives a reference I will accept this answer. Thanks again. :) $\endgroup$
    – Kaveh
    Jul 23, 2012 at 20:31
  • $\begingroup$ My pleasure ;-) Cheers! $\endgroup$ Jul 23, 2012 at 20:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.