最小時間で4艘の舟運びを制約論理プログラム iZ-Cを使って解きます。
025_最小時間で4艘の舟運びを制約論理プログラム iZ-Cを使って解きます。
----------------------------------------------------------------------------
make && ./river_boart 18
gcc -Wall -O3 -I. -L. -o river_boart river_boart.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Mon Jan 4 15:56:24 2021
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}, {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..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}
Step 12, Solution 1, cost 88
TIME 0, 16, 8, 8, 16, 4, 8, 2, 4, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 0, 1, 1, 0 [ ,1, , ,4] [c, ,2,3, ]
6: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
7: 1, 1, 1, 0, 0 [ , , ,3,4] [c,1,2, , ]
8: 0, 1, 0, 0, 0 [c, ,2,3,4] [ ,1, , , ]
9: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
10: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
11: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 10, Solution 2, cost 86
TIME 0, 16, 8, 8, 16, 4, 8, 16, 2, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 0, 1, 1, 0 [ ,1, , ,4] [c, ,2,3, ]
6: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
7: 1, 1, 1, 0, 1 [ , , ,3, ] [c,1,2, ,4]
8: 0, 0, 1, 0, 1 [c,1, ,3, ] [ , ,2, ,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 10, Solution 3, cost 80
TIME 0, 16, 8, 8, 16, 2, 8, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 1, 0, 1, 0 [ , ,2, ,4] [c,1, ,3, ]
6: 0, 1, 0, 0, 0 [c, ,2,3,4] [ ,1, , , ]
7: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
8: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 8, Solution 4, cost 70
TIME 0, 16, 8, 8, 16, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
7: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 10, Solution 5, cost 60
TIME 0, 16, 8, 8, 4, 2, 8, 4, 2, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 1, 0, 0, 1 [c, ,2,3, ] [ ,1, , ,4]
7: 1, 1, 1, 0, 1 [ , , ,3, ] [c,1,2, ,4]
8: 0, 0, 1, 0, 1 [c,1, ,3, ] [ , ,2, ,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 8, Solution 6, cost 54
TIME 0, 16, 8, 8, 4, 2, 8, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 1, 0, 0, 1 [c, ,2,3, ] [ ,1, , ,4]
7: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 7, cost 40
TIME 0, 16, 8, 8, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 8, cost 38
TIME 0, 16, 8, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 9, cost 36
TIME 0, 16, 4, 8, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 1, 0, 1 [ ,1, ,3, ] [c, ,2, ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 10, cost 34
TIME 0, 16, 4, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 1, 0, 1 [ ,1, ,3, ] [c, ,2, ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 11, cost 32
TIME 0, 16, 2, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 1, 0, 0, 1 [ , ,2,3, ] [c,1, , ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Step 6, Solution 12, cost 30
TIME 0, 4, 2, 16, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 1, 1, 0, 0 [ , , ,3,4] [c,1,2, , ]
2: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]
Nb Fails = 219
Nb Choice Points = 513
Heap Size = 5120
Elapsed Time = 0.010544 s
Mon Jan 4 15:56:24 2021
----------------------------------------------------------------------------
/**************************************************************************
* ４艘(そう)の舟運び
* 川の左岸に舟が４艘(そう)ある。
* 右岸まで横断するには、
* Ａ舟は２分、Ｂ舟は４分、Ｃ舟は８分、Ｄ舟は１６分かかる。
* この舟すべてを右岸に運びたいが、船頭は１人しかいない。
* １艘にもう１艘だけをロープでつないで渡ることができるが、
* そのときは遅いほうの時間がかかってしまう。
*
* すべてを運ぶには最短で何分かかるだろうか？
*
* ただし舟の乗りかえ、つなぐ時間などはすべて無視する。
* http://quiz-tairiku.com/logic/q10.html
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"
int DIM, MAX_STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
CSint **TIME;
enum {captain, boart1, boart2, boart3, boart4};
/**************************************************************************/
/**************************************************************************/
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;
int END = (long int)(int *)extra;
//cs_printf("%A\n", allvars, MAX_STP);
// if(val == QR_PD_END) return TRUE;
if(val == END){
for(i = index + 1; i < size; i++){
if(!cs_EQ(allvars[i], val)) return FALSE;
}
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] ={"c1234"};
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, cost %d\n", step, ++NbSolutions, cs_getValue(cost));
// cs_printf("TIME %A\n", TIME, step);
cs_printf("TIME %A\n", TIME, step);
printf("captain = 0, boart = 1_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("captain = 0, boart = 1_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");
}
}
/**************************************************************************/
/**************************************************************************/
CSint *cs_inc_pos_num(CSint **array, int num, int man, int pos){
CSint *current = cs_OccurDomain(pos, &array[DIM*num + man], 3);
CSint *prev = cs_OccurDomain(pos, &array[DIM*(num-1) + man], 3);
return cs_Sub(current, prev);
}
/**************************************************************************/
/**************************************************************************/
void boart_direction(CSint *pos_num, CSint *boart_dir){
cs_NEQ(cs_Add(cs_ReifLE(pos_num, 0), cs_ReifEQ(boart_dir, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(pos_num, 0), cs_ReifEQ(boart_dir, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(pos_num, 0), cs_ReifEQ(boart_dir, -1)), 0);
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;
DIM = 5;
QR_PD_END = (1 << DIM) - 1;
int order[5] ={1, 2, 4, 8, 16};
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
MAX_STP = atoi(argv[1]);
QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
TIME = (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);
QR_PD = (CSint **)malloc(MAX_STP * sizeof(CSint *));
for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM * i], &order[0], DIM);
}
TIME[0] = CSINT(0);
for(i = 1; i < MAX_STP; i++){
CSint **mv = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **Abs_mv = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
mv[j] = cs_Sub(QR[DIM*i+j], QR[DIM*(i-1)+j]);
Abs_mv[j] = cs_Abs(mv[j]);
}
CSint *inc_boart_pos0_num = cs_inc_pos_num(QR, i, boart1, 0);
CSint *inc_boart_pos1_num = cs_inc_pos_num(QR, i, boart1, 1);
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(mv[captain], 0), cs_ReifNEQ(mv[captain], 0));
cs_LE(cs_Sigma(&Abs_mv[boart1], DIM-1), 2);
cs_InInterval(inc_boart_pos0_num, -2, 2);
cs_InInterval(inc_boart_pos1_num, -2, 2);
int inc_boart_pos1_num_value[5] = {-1, -1, 0, 1, 1};
CSint *captain_pos1= cs_Element(cs_Add(CSINT(2), inc_boart_pos1_num), inc_boart_pos1_num_value, 5);
cs_EQ(cs_Add(inc_boart_pos0_num, inc_boart_pos1_num), 0);
cs_Eq(captain_pos1, mv[captain]);
cs_GE(cs_Mul(cs_Min(&mv[boart1], DIM-1), cs_Max(&mv[boart1], DIM-1)), 0);
int time_order[5] = {1, 2, 4, 8, 16};
CSint **tim_tmp = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
tim_tmp[j] = cs_Mul(Abs_mv[j], CSINT(time_order[j]));
}
// CSint *PRE_TIME = cs_createCSint(0, 1000);
int ttime_order[6] = {0, 1, 2, 4, 8, 16};
CSint *PRE_TIME = cs_createCSintFromDomain(&ttime_order[0], DIM+1);
//cs_printf("%D\n", PRE_TIME);
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(PRE_TIME, 0),
cs_ReifEq(PRE_TIME, cs_Max(&tim_tmp[0], DIM)));
TIME[i] = PRE_TIME;
}
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, (void *)(long)QR_PD_END);
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);
CSint *cost = cs_Sigma(TIME, MAX_STP);
// 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;
}
