最小手数で宣教師と人食いの川渡りを制約論理プログラム iZ-Cを使って解きます。
最小手数で宣教師と人食いの川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_missio_num 14
gcc -Wall -O3 -I. -L. -o river_missio_num river_missio_num.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Sun Dec 20 10:58:17 2020
QR: 0, 3, 3, 0, 0, 1, {1..3}, {1..3}, {0..2}, {0..2}, 0, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..2}, {0..2}, {1..3}, {1..3}, 1, 0, 0, 3, 3
QR_PD: 60, {21..59, 61..701}, {0..59, 61..1020}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {320..1001}, 961
Step 12, Solution 1
boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4
0: 0, 3, 3, 0, 0
1: 1, 2, 2, 1, 1
2: 0, 3, 2, 0, 1
3: 1, 3, 0, 0, 3
4: 0, 3, 1, 0, 2
5: 1, 1, 1, 2, 2
6: 0, 2, 2, 1, 1
7: 1, 0, 2, 3, 1
8: 0, 0, 3, 3, 0
9: 1, 0, 1, 3, 2
10: 0, 0, 2, 3, 1
11: 1, 0, 0, 3, 3
Nb Fails = 44
Nb Choice Points = 79
Heap Size = 4096
Elapsed Time = 0.001232 s
Sun Dec 20 10:58:17 2020
---------------------------------------------------------------------------
/**************************************************************************
* 宣教師と人食いの川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"
int DIM, MAX_STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
//int boart = 0, missionary = 1_3, deamon = 4_6;
enum {boart=0, missionary0, deamon0, missionary1, deamon1};
/**************************************************************************/
/**************************************************************************/
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);
}
/**************************************************************************/
/**************************************************************************/
CSint *is_GE_LE(CSint *Val, int n1, int n2){
CSint *a1 = cs_ReifGE(Val, n1);
CSint *a2 = cs_ReifLE(Val, n2);
return cs_ReifEQ(cs_Add(a1, a2), 2);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;
//cs_printf("%A\n", allvars, MAX_STP);
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[7] ={"bmmmddd"};
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("boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4\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("boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4\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;
DIM = 5;
int order[5] ={1};
for(i = 1; i < 5; i++) order[i] = order[i-1]*4;
QR_PD_END = 1 + 3*order[3] + 3*order[4];
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
MAX_STP = atoi(argv[1]);
QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
for(i = 0; i < MAX_STP; i++){
QR[DIM*i + boart] = cs_createCSint(0, 1);
QR[DIM*i + missionary0] = cs_createCSint(0, 3);
QR[DIM*i + deamon0] = cs_createCSint(0, 3);
QR[DIM*i + missionary1] = cs_createCSint(0, 3);
QR[DIM*i + deamon1] = cs_createCSint(0, 3);
}
// cs_EQ(cs_Sigma(&QR[0], 3), 0);
// cs_EQ(cs_Sigma(&QR[DIM * (MAX_STP -1)], DIM), DIM);
cs_EQ(QR[DIM*0 + boart], 0);
cs_EQ(QR[DIM*0 + missionary0], 3);
cs_EQ(QR[DIM*0 + deamon0], 3);
cs_EQ(QR[DIM*0 + missionary1], 0);
cs_EQ(QR[DIM*0 + deamon1], 0);
//enum {boart, missionary0, deamon0, missionary1, deamon1};
QR_PD = (CSint **)malloc(MAX_STP * sizeof(CSint *));
CSint **boart_pos = (CSint **)malloc(MAX_STP * sizeof(CSint *));
for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM * i], &order[0], DIM);
boart_pos[i] = QR[DIM*i + boart];
cs_NEQ(cs_Add(cs_ReifEQ(QR[DIM*i + missionary0], 0),
cs_ReifGe(QR[DIM*i + missionary0], QR[DIM*i + deamon0])), 0);
cs_NEQ(cs_Add(cs_ReifEQ(QR[DIM*i + missionary1], 0),
cs_ReifGe(QR[DIM*i + missionary1], QR[DIM*i + deamon1])), 0);
cs_EQ(cs_Add(QR[DIM*i + missionary0], QR[DIM*i + missionary1]), 3);
cs_EQ(cs_Add(QR[DIM*i + deamon0], QR[DIM*i + deamon1]), 3);
}
cs_EQ(QR_PD[MAX_STP - 1], QR_PD_END);
//exit(1);
for(i = 1; i < MAX_STP; i++){
cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(QR_PD[i], QR_PD_END)), 0);
}
for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(boart_pos[i], boart_pos[i -1]);
//cs_printf("%D\n", mv_boart);
CSint *m0_inc = cs_Sub(QR[DIM*i + missionary0], QR[DIM*(i-1) + missionary0]);
CSint *m1_inc = cs_Sub(QR[DIM*i + missionary1], QR[DIM*(i-1) + missionary1]);
CSint *d0_inc = cs_Sub(QR[DIM*i + deamon0], QR[DIM*(i-1) + deamon0]);
CSint *d1_inc = cs_Sub(QR[DIM*i + deamon1], QR[DIM*(i-1) + deamon1]);
CSint *md0_inc = cs_Sub(cs_Sigma(&QR[DIM*i + missionary0], 2),
cs_Sigma(&QR[DIM*(i-1) + missionary0], 2));
CSint *md1_inc = cs_Sub(cs_Sigma(&QR[DIM*i + missionary1], 2),
cs_Sigma(&QR[DIM*(i-1) + missionary1], 2));
cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(QR_PD[i-1], QR_PD_END), cs_ReifNEQ(cs_Abs(mv_boart), 0)), 0);
cs_LE(cs_Abs(m0_inc), 2); cs_LE(cs_Abs(m1_inc), 2);
cs_LE(cs_Abs(d0_inc), 2); cs_LE(cs_Abs(d1_inc), 2);
cs_GE(cs_Mul*1, 0); cs_GE(cs_Mul*2, 0);
cs_EQ(cs_Add(md0_inc, md1_inc), 0); cs_LE(cs_Abs(md0_inc), 2); cs_LE(cs_Abs(md1_inc), 2);
cs_NEQ(cs_Add(cs_ReifLE(md1_inc , 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(md1_inc , 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(md1_inc , 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifLE(md0_inc , 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(md0_inc , 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(md0_inc , 0), cs_ReifEQ(mv_boart, 1)), 0);
}
// 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);
// for(i = 0; i < MAX_STP; i++){ cs_printf("%A\n", &QR[DIM*i], DIM); }
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_minimize(&QR[0], DIM * MAX_STP, cs_findFreeVarNbConstraints, 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;
}
