#define LBM 0 			// Index of mathematicians on left bank
#define LBP 1			// Index of physicsts on left bank
#define RBM 2			// Index of mathematicians on right bank
#define RBP 3			// Index of physicsts on right bank
#define ALL 4
#define SEATS 3
#define N (ALL+1)*(ALL+1)*(ALL+1)*(ALL+1)		// Plenty big

int state[N][4];
int best_so_far;

2lp_main()
{
	best_so_far = N+2;			// Upper bound on crossings
	
	create_new_state(0,ALL,ALL,0,0);	// Initial state
	
	find_all {				// Keep searching for solutions
		and(int crss=0;crss < N-1;crss++) {	// Central loop
			try_crossings(crss);		// Generate next state
			if goal(crss+1); 
			then {
				best_so_far = crss + 1;	// Shortest trip
				break;		// Exit loop successfully
			}
		}	// Re-enter loop to find next solution
	}
}

goal(int next) 
{

	next%2 == 1; 			// Boat must be on the right bank
	state[next][RBM] == ALL; 	// Mathematicians across
	state[next][RBP] == ALL; 	// Physicists across
	output(next);			// To be written below
}

try_crossings(int crss)
{ 
int lbm,lbp,rbm,rbp;
int maths,phys;

	// Enter current state in identifiers lbm,lbp,rbm,rbp
	read_current_state(crss,lbm,lbp,rbm,rbp); 

	if crss%2 == 0;		// Boat on left bank
	then {
		maths = lbm;
		phys = lbp;
	}
	else {
		maths = rbm;
		phys = rbp;
	}
	// Select mathematicians
	or(int m=maths;m>=0;m--)
		// Select physicists
		or(int p=phys;p>=0;p--) {
			if crss%2==1;			// Boat on right bank ?
			then crss + 2 <= best_so_far;	// Prune by bound
			m+p >= 1; 		// Send at least one person	
			m+p <= SEATS;		// but dont send too many 
			if crss%2 == 0; 	// Boat on left bank ? 
			then create_new_state(crss+1,lbm-m,lbp-p,rbm+m,rbp+p);
			else create_new_state(crss+1,lbm+m,lbp+p,rbm-m,rbp-p);
		}
}

read_current_state(int crss, int & lbm, & lbp, & rbm, & rbp)
{
	lbm = state[crss][LBM];
	lbp = state[crss][LBP];
	rbm = state[crss][RBM];
	rbp = state[crss][RBP];
}

create_new_state(int crssplus1,nextlbm,nextlbp,nextrbm,nextrbp)
{
	if nextlbm >= 1;		// LBP musn't outnumber
	then nextlbp <= nextlbm;	// LBM

	if nextrbm >= 1;		// RBP musn't outnumber 
	then nextrbp <= nextrbm;	// RBM
			  
	state[crssplus1][LBM] = nextlbm; 
	state[crssplus1][LBP] = nextlbp; 
	state[crssplus1][RBM] = nextrbm;  
	state[crssplus1][RBP] = nextrbp;
	
	and(int i=crssplus1%2;i<crssplus1;i=i+2) 
		c_or(int j=0;j<4;j++) 		// Check state not repeated
			state[i][j] != state[crssplus1][j];
}

output(int crss) 
{
	printf("Solution found with %d crossings\n",crss);
	and(int i=0;i<=crss;i++){
		printf("state # %d is: ",i);
		and(int j=0; j<4; j++)
			printf("%d ",state[i][j]);
		printf("\n");
	}
	printf("\n");
}