// ************************************************************************** // // eses eses // eses eses // eses eseses esesese eses Embedded Systems Group // ese ese ese ese ese // ese eseseses eseseses ese Department of Computer Science // eses eses ese eses // eses eseses eseseses eses University of Kaiserslautern // eses eses // // ************************************************************************** // // Suppose there are h holes and p pigeons to put in the holes. Every // pigeon should be in a hole and no more than one pigeon is in one // hole. Consider the case h=N and p=N+1. In [GrZa03], it is proved // that BDDs have lower bound 1.63^n for pigeonhole n, while there // are polynomial resolution proofs. // // ************************************************************************** macro N=5; module PigeonHole( [N+1][N]bool p_in_h) { nothing; } satisfies { s: assert not( // -- all pigeons are in a hole ------------- ( forall(i=0..N) exists(j=0..N-1) p_in_h[i][j] ) & // -- in every hole, there is a pigeon ------------- ( forall(j=0..N-1) exists(i=0..N) p_in_h[i][j] ) & // -- if pigeon i is in hole j, then no other pigeon // -- is in hole j ( forall(i=0..N) forall(j=0..N-1) (p_in_h[i][j] -> forall(k=0..N-1) ((k!=i) -> !p_in_h[k][j])) ) ); }