next up previous
Next: Parity Problem Up: Some SAT Benchmarks Visualised Previous: Inductive Interference

Pigeon Hole Problem

SAT encoding of the problem of how 11 pigeons can be placed in 10 holes, from the DIMACS benchmark suite, problem hole10.cnf. The differences in each image show how a given interpretation may effect the overall interpretation of the structure in a problem instance.

Figure 7: Pigeon Hole Problem, Cooccurrence of Variables
\begin{figure}\epsfig{figure=images/hole10_vco,width=\textwidth} \end{figure}

Figure 8: Pigeon Hole Problem, Cooccurrence of Literals
\begin{figure}\epsfig{figure=images/hole10_lco,width=\textwidth} \end{figure}

Figure 9: Pigeon Hole Problem, Basic Implicative Interpretation
\begin{figure}\epsfig{figure=images/hole10_imp,width=\textwidth} \end{figure}



Last modified: 2004-03-17
Andrew Slater