農夫 山羊 狼 キャベツ の川渡りを制約論理プログラム iZ-Cを使って解きます。

農夫 山羊 狼 キャベツ の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
time ./river 8
Fri Jul 17 06:13:43 2020
0, 0, 0, 0, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, 1, 1, 1, 1

Step 8, Solution 1
farmer = 0, goat = 1, wolf = 2, cabbage = 3
0: 0, 0, 0, 0 [f,g,w,c,] [ , , , ,]
1: 1, 1, 0, 0 [ , ,w,c,] [f,g, , ,]
2: 0, 1, 0, 0 [f, ,w,c,] [ ,g, , ,]
3: 1, 1, 0, 1 [ , ,w, ,] [f,g, ,c,]
4: 0, 0, 0, 1 [f,g,w, ,] [ , , ,c,]
5: 1, 0, 1, 1 [ ,g, , ,] [f, ,w,c,]
6: 0, 0, 1, 1 [f,g, , ,] [ , ,w,c,]
7: 1, 1, 1, 1 [ , , , ,] [f,g,w,c,]

Step 8, Solution 2
farmer = 0, goat = 1, wolf = 2, cabbage = 3
0: 0, 0, 0, 0 [f,g,w,c,] [ , , , ,]
1: 1, 1, 0, 0 [ , ,w,c,] [f,g, , ,]
2: 0, 1, 0, 0 [f, ,w,c,] [ ,g, , ,]
3: 1, 1, 1, 0 [ , , ,c,] [f,g,w, ,]
4: 0, 0, 1, 0 [f,g, ,c,] [ , ,w, ,]
5: 1, 0, 1, 1 [ ,g, , ,] [f, ,w,c,]
6: 0, 0, 1, 1 [f,g, , ,] [ , ,w,c,]
7: 1, 1, 1, 1 [ , , , ,] [f,g,w,c,]

Nb Fails = 98
Nb Choice Points = 198
Heap Size = 2048
Elapsed Time = 0.00266 s
Fri Jul 17 06:13:43 2020

real 0m0.005s
user 0m0.004s
sys 0m0.001s
---------------------------------------------------------------------------
/**************************************************************************
* 農夫 山羊 狼 キャベツ の川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, STP;
CSint **QR, **same_QR;
//int farmer = 0, goat = 1, wolf = 2, cabbage = 3;
enum {farmer, goat, wolf, cabbage};
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
char alph[4] ={"fgwc"};
int i, j;

printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
printf("farmer = 0, goat = 1, wolf = 2, cabbage = 3\n");
for(i = 0; i < STP; i++){
printf("%3d: ", i);
cs_printf("%A ", &QR[DIM * i], DIM);
putchar('[');
for(j = 0; j < DIM; j++) printf("%c,", cs_getValue(QR[DIM * i + j]) == 0 ? alph[j] : ' ');
putchar(']');

printf(" [");
for(j = 0; j < DIM; j++) printf("%c,", cs_getValue(QR[DIM * i + j]) == 1 ? alph[j] : ' ');
printf("]\n");
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;

cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
DIM = 4;
STP = atoi(argv[1]);

QR = (CSint **)malloc(DIM * STP * sizeof(CSint *));
same_QR = (CSint **)malloc(DIM * STP*STP/2 * sizeof(CSint *));

for(i = 0; i < DIM * STP; i++){
QR[i] = cs_createCSint(0, 1);
}

cs_EQ(cs_Sigma(&QR[0], DIM), 0);
cs_EQ(cs_Sigma(&QR[DIM * (STP -1)], DIM), 4);

for(i = 0; i < STP - 1; i++){
int j = DIM * i, jn = DIM * (i + 1);
cs_Le(cs_VAdd(3,
cs_ReifNeq(QR[j + goat], QR[jn + goat]),
cs_ReifNeq(QR[j + wolf], QR[jn + wolf]),
cs_ReifNeq(QR[j + cabbage], QR[jn + cabbage])),
cs_ReifNeq(QR[j + farmer], QR[jn + farmer]));
}
for(i = 0; i < STP; i++){
int j = DIM * i;
// farmer = 0, goat = 1, wolf = 2, cabbage = 3;
cs_NEQ(cs_Add(
cs_ReifNeq(QR[j + wolf], QR[j + goat]),
cs_ReifEq(QR[j + farmer], QR[j + goat])),
0);

cs_NEQ(cs_Add(
cs_ReifNeq(QR[j + cabbage], QR[j + goat]),
cs_ReifEq(QR[j + farmer], QR[j + goat])),
0);
}

int n = 0;
for (i = 0; i < STP - 1; i++){
for (int j = i + 1; j < STP; j++){
for (int k = 0; k < DIM; k++){
same_QR[DIM * n + k] = cs_ReifEq(QR[DIM * i + k], QR[DIM * j + k]);
}
cs_NEQ(cs_OccurDomain(0, &same_QR[DIM * n++], DIM), 0);
}
}

cs_printf("%A\n", QR, DIM * STP);

cs_findAll(&QR[0], DIM * STP, cs_findFreeVarNbConstraints, printSolution);

cs_printStats();
printf("Elapsed Time = %g s\n", (double) (clock() - t0) / CLOCKS_PER_SEC);
time(&nowtime); printf("%s", ctime(&nowtime));
cs_end();
return EXIT_SUCCESS;
}