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

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

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

<p>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 <em>clique-ness</em> 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.</p>

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

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

CC BY-SA 3.0
2012-07-23T19:23:18.913Z
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")?
Kaveh
CC BY-SA 3.0
2012-07-23T20:31:33.917Z
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.
Giorgio Camerani
CC BY-SA 3.0
2012-07-23T20:31:52.913Z
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. :)
Kaveh
CC BY-SA 3.0
2012-07-23T20:36:48.157Z
My pleasure ;-) Cheers!
Giorgio Camerani
CC BY-SA 3.0
2012-07-23T12:59:12.430Z
2012-07-23T20:02:49.943Z
2012-07-23T20:02:49.943Z
Giorgio Camerani
<p>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$":</p>

<p>$$\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)$$</p>

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

<p>Do they find a satisfying assignment quickly on such instances?</p>

CC BY-SA 3.0
2012-07-22T08:44:06.837Z
By "fail to answer correctly" do you mean "run out of resources on sufficiently large values of n" ?
Vijay D
CC BY-SA 3.0
2012-07-22T18:26:43.133Z
@Kaveh Are you allowing repetition of clauses and/or repetition of variables in the same clause? Thanks
Tayfun Pay
CC BY-SA 3.0
2012-07-22T20:26:32.500Z
@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.
Kaveh
CC BY-SA 3.0
2012-07-22T20:28:29.860Z
@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?
Kaveh
<cc.complexity-theory><lo.logic><proof-complexity>
How efficient are DPLL-based SAT-solvers on satisfiable instances of PHP?
Kaveh
# How efficient are DPLL-based SAT-solvers on satisfiable instances of PHP?

(Asked by: username_0 on 2012-07-22)

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?

**Tags:** cc.complexity-theory, lo.logic, proof-complexity
> **Comments:**
> **username_1**: By "fail to answer correctly" do you mean "run out of resources on sufficiently large values of n" ?  
> **username_2**: @Kaveh Are you allowing repetition of clauses and/or repetition of variables in the same clause? Thanks  
> **username_0**: @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.  
> **username_0**: @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?  

---

## 1 answers

### Answer by username_3 on 2012-07-23. Score: 14 | Accepted answer

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.

> **Comments:**
> **username_0**: 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")?  
> **username_3**: 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.  
> **username_0**: 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. :)  
> **username_3**: My pleasure ;-) Cheers!  

---

