最小手数で農夫 山羊 狼 キャベツ の川渡りを制約論理プログラム iZ-Cを使って解きます。
最小手数で農夫 山羊 狼 キャベツ の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river 10
make: 'all' に対して行うべき事はありません.
Wed Dec 9 06:27:19 2020
QR: 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}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}
QR_PD: 0, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}
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]
Nb Fails = 30
Nb Choice Points = 65
Heap Size = 2048
Elapsed Time = 0.001843 s
Wed Dec 9 06:27:19 2020
---------------------------------------------------------------------------
/**************************************************************************
* 農夫 山羊 狼 キャベツ の川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"
int DIM, MAX_STP, STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
//int farmer = 0, goat = 1, wolf = 2, cabbage = 3;
enum {farmer, goat, wolf, cabbage};
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe1), 0);
cs_NEQ(cs_Add(cs_ReifEQ(cond, 1), exe2), 0);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;
if(val == QR_PD_END) return TRUE;
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void print_sub(int selct, int chk_num){
char alph[4] ={"fgwc"};
int j;
for(j = 0; j < DIM; j++) printf("%c%c",
cs_getValue(QR[DIM * selct + j]) == chk_num ? alph[j] : ' ', j < DIM-1 ? ',':']');
}
/**************************************************************************/
/**************************************************************************/
void printSolution1(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cs_Index(&QR_PD[0], MAX_STP, QR_PD_END));
printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf("farmer = 0, goat = 1, wolf = 2, cabbage = 3\n");
for(i = 0; i < step; i++){
printf("%3d: ", i);
cs_printf("%A ", &QR[DIM * i], DIM);
putchar('['); print_sub(i, 0);
printf(" ["); print_sub(i, 1);
printf("\n");
}
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;
printf("\nStep %d, Solution %d\n", nbVars / DIM, ++NbSolutions);
printf("farmer = 0, goat = 1, wolf = 2, cabbage = 3\n");
for(i = 0; i < nbVars / DIM; i++){
printf("%3d: ", i);
cs_printf("%A ", &QR[DIM * i], DIM);
putchar('['); print_sub(i, 0);
printf(" ["); print_sub(i, 1);
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;
QR_PD_END = (1<<DIM) -1;
MAX_STP = atoi(argv[1]);
QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
QR_PD= (CSint **)malloc(MAX_STP * sizeof(CSint *));
for(i = 0; i < DIM * MAX_STP; i++){
QR[i] = cs_createCSint(0, 1);
}
cs_EQ(cs_Sigma(&QR[0], DIM), 0);
// cs_EQ(cs_Sigma(&QR[DIM * (MAX_STP -1)], DIM), DIM);
for(i = 0; i < MAX_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]));
}
int order[4] ={1, 2, 4, 8};
for(i = 0; i < MAX_STP; i++){
int j = DIM * i;
// farmer = 0, goat = 1, wolf = 2, cabbage = 3;
CSint *j_fm = QR[j + farmer];
CSint *Add_w_g = cs_Add(QR[j + wolf], QR[j + goat]);
CSint *Add_g_c = cs_Add(QR[j + goat], QR[j + cabbage]);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 0), cs_ReifNEQ(Add_w_g, 2)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 1), cs_ReifNEQ(Add_w_g, 0)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 0), cs_ReifNEQ(Add_g_c, 2)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 1), cs_ReifNEQ(Add_g_c, 0)), 0);
QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);
}
for(i = 1; i < MAX_STP; i++){
cond_imp(cs_ReifEQ(QR_PD[i-1], QR_PD_END),
cs_ReifEQ(QR_PD[i], QR_PD_END), cs_ReifEq(QR_PD[i], QR_PD[i]));
}
// cs_AllNeq(&QR_PD[0], MAX_STP);
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, NULL);
cs_printf("QR: %A\n", QR, DIM * MAX_STP);
cs_printf("QR_PD: %A\n", QR_PD, MAX_STP);
CSint *cost = cs_Index(&QR_PD[0], MAX_STP, QR_PD_END);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVar, printSolution);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVarNbConstraints, printSolution);
cs_minimize(&QR[0], DIM * MAX_STP, cs_findFreeVar, cost, printSolution1);
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;
}
