最小手数で宣教師と人食いの川渡り2 （人数をまとめない）を制約論理プログラム iZ-Cを使って解きます。
最小手数で宣教師と人食いの川渡り2 （人数をまとめない）を制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_missio 18
gcc -Wall -O3 -I. -L. -o river_missio river_missio.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Wed Dec 23 08:18:28 2020
QR: 0, 0, 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}, {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}, {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}, {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..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}
Step 18, Solution 1
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 0 [ ,m,m,m, , ,d] [b, , , ,d,d, ]
6: 0, 0, 0, 0, 0, 1, 0 [b,m,m,m,d, ,d] [ , , , , ,d, ]
7: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
8: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
9: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
10: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
11: 1, 0, 1, 1, 1, 0, 1 [ ,m, , , ,d, ] [b, ,m,m,d, ,d]
12: 0, 0, 0, 1, 1, 0, 0 [b,m,m, , ,d,d] [ , , ,m,d, , ]
13: 1, 1, 1, 1, 1, 0, 0 [ , , , , ,d,d] [b,m,m,m,d, , ]
14: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
15: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
16: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
17: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]
Step 16, Solution 2
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 0 [ ,m,m,m, , ,d] [b, , , ,d,d, ]
6: 0, 0, 0, 0, 0, 1, 0 [b,m,m,m,d, ,d] [ , , , , ,d, ]
7: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
8: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
9: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
10: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
11: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
12: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
13: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
14: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
15: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]
Step 14, Solution 3
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
6: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
7: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
8: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
9: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
10: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
11: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
12: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
13: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]
Step 12, Solution 4
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
4: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
5: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
6: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
7: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
8: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
9: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
10: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
11: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]
Nb Fails = 63771
Nb Choice Points = 127637
Heap Size = 7168
Elapsed Time = 0.402291 s
Wed Dec 23 08:18:28 2020
---------------------------------------------------------------------------
/**************************************************************************
* 宣教師と人食いの川渡り2 （人数をまとめない）
**************************************************************************/
#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, missionary1, missionary2, missionary3, deamon1, deamon2, deamon3};
/**************************************************************************/
/**************************************************************************/
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, missionary = 1_3, deamon = 4_6\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, missionary = 1_3, deamon = 4_6\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 = 7;
QR_PD_END = (1 << DIM) - 1;
int order[7] ={1, 2, 4, 8, 16, 32, 64};
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 < 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);
//enum {boart, missionary1, missionary2, missionary3, deamon1, deamon2, deamon3};
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);
CSint *mission_pos0_num = cs_OccurDomain(0, &QR[DIM*i + missionary1], 3);
CSint *mission_pos1_num = cs_OccurDomain(1, &QR[DIM*i + missionary1], 3);
CSint *deamon_pos0_num = cs_OccurDomain(0, &QR[DIM*i + deamon1], 3);
CSint *deamon_pos1_num = cs_OccurDomain(1, &QR[DIM*i + deamon1], 3);
boart_pos[i] = QR[DIM*i + boart];
cs_NEQ(cs_Add(cs_ReifEQ(mission_pos0_num, 0), cs_ReifGe(mission_pos0_num, deamon_pos0_num)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(mission_pos1_num, 0), cs_ReifGe(mission_pos1_num, deamon_pos1_num)), 0);
}
//exit(1);
for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(boart_pos[i], boart_pos[i-1]);
CSint *mv_missionary1 = cs_Sub(QR[DIM*i + missionary1], QR[DIM*(i-1) + missionary1]);
CSint *mv_missionary2 = cs_Sub(QR[DIM*i + missionary2], QR[DIM*(i-1) + missionary2]);
CSint *mv_missionary3 = cs_Sub(QR[DIM*i + missionary3], QR[DIM*(i-1) + missionary3]);
CSint *mv_deamon1 = cs_Sub(QR[DIM*i + deamon1], QR[DIM*(i-1) + deamon1]);
CSint *mv_deamon2 = cs_Sub(QR[DIM*i + deamon2], QR[DIM*(i-1) + deamon2]);
CSint *mv_deamon3 = cs_Sub(QR[DIM*i + deamon3], QR[DIM*(i-1) + deamon3]);
CSint *inc_mission_pos0_num = cs_Sub(cs_OccurDomain(0, &QR[DIM*i + missionary1], 3),
cs_OccurDomain(0, &QR[DIM*(i-1) + missionary1], 3));
CSint *inc_mission_pos1_num = cs_Sub(cs_OccurDomain(1, &QR[DIM*i + missionary1], 3),
cs_OccurDomain(1, &QR[DIM*(i-1) + missionary1], 3));
CSint *inc_deamon_pos0_num = cs_Sub(cs_OccurDomain(0, &QR[DIM*i + deamon1], 3),
cs_OccurDomain(0, &QR[DIM*(i-1) + deamon1], 3));
CSint *inc_deamon_pos1_num = cs_Sub(cs_OccurDomain(1, &QR[DIM*i + deamon1], 3),
cs_OccurDomain(1, &QR[DIM*(i-1) + deamon1], 3));
CSint *inc_md_pos0_num = cs_Add(inc_mission_pos0_num, inc_deamon_pos0_num);
CSint *inc_md_pos1_num = cs_Add(inc_mission_pos1_num, inc_deamon_pos1_num);
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(mv_boart, 0)), 0);
cs_LE(cs_VAdd(6, cs_Abs(mv_missionary1), cs_Abs(mv_missionary2), cs_Abs(mv_missionary3),
cs_Abs(mv_deamon1), cs_Abs(mv_deamon2), cs_Abs(mv_deamon3)), 2);
cs_NEQ(cs_Add(cs_ReifLE(inc_md_pos1_num, 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(inc_md_pos1_num, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(inc_md_pos1_num, 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifLE(inc_md_pos0_num, 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(inc_md_pos0_num, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(inc_md_pos0_num, 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_GE(cs_Mul(inc_mission_pos0_num, inc_deamon_pos0_num), 0);
cs_GE(cs_Mul(inc_mission_pos1_num, inc_deamon_pos1_num), 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);
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;
}
