// **************************************************************************
//
//    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])) )
        );
}