最小手数で夫婦３組の川渡りを制約論理プログラム iZ-Cを使って解きます。
最小手数で夫婦３組の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_marrige 17
make: 'all' に対して行うべき事はありません.
Tue Dec 22 21:16:32 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}
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}
Step 16, Solution 1
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 0, 0, 1, 0, 1 [ ,A,a,B, ,C, ] [S, , , ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 0 [S,A,a,B, ,C,c] [ , , , ,b, , ]
5: 1, 0, 1, 0, 1, 0, 0 [ ,A, ,B, ,C,c] [S, ,a, ,b, , ]
6: 0, 0, 1, 0, 0, 0, 0 [S,A, ,B,b,C,c] [ , ,a, , , , ]
7: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
8: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
9: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
10: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
11: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
12: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
13: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
14: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
15: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]
Step 14, Solution 2
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 0, 0, 1, 0, 1 [ ,A,a,B, ,C, ] [S, , , ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 0 [S,A,a,B, ,C,c] [ , , , ,b, , ]
5: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
6: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
7: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
8: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
9: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
10: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
11: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
12: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
13: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]
Step 12, Solution 3
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
5: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
6: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
7: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
8: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
9: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
10: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
11: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]
Nb Fails = 5406
Nb Choice Points = 10897
Heap Size = 7168
Elapsed Time = 0.046205 s
Tue Dec 22 21:16:32 2020
---------------------------------------------------------------------------
/**************************************************************************
* 夫婦３組の川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"
//#include "sgn.c"
int DIM, MAX_STP, STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
enum {boart, A,a, B,b, C,c};
/**************************************************************************/
/**************************************************************************/
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[7] ={"SAaBbCc"};
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("Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,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("Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,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;
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
DIM = 7;
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);
int order[7] ={1, 2, 4, 8, 16, 32, 64};
for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);
// CSint *pos_boart = QR[DIM*i+ boart];
CSint *pos_A = QR[DIM*i+ A];
CSint *pos_a = QR[DIM*i+ a];
CSint *pos_B = QR[DIM*i+ B];
CSint *pos_b = QR[DIM*i+ b];
CSint *pos_C = QR[DIM*i+ C];
CSint *pos_c = QR[DIM*i+ c];
cs_NEQ(cs_Add(cs_ReifEq(pos_A, pos_a), cs_ReifNeq(pos_a, pos_B)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_A, pos_a), cs_ReifNeq(pos_a, pos_C)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_B, pos_b), cs_ReifNeq(pos_b, pos_A)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_B, pos_b), cs_ReifNeq(pos_b, pos_C)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_C, pos_c), cs_ReifNeq(pos_c, pos_A)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_C, pos_c), cs_ReifNeq(pos_c, pos_B)), 0);
}
for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(QR[DIM*i+ boart], QR[DIM*(i-1) + boart]);
CSint *mv_A = cs_Sub(QR[DIM*i+ A], QR[DIM*(i-1) + A]);
CSint *mv_a = cs_Sub(QR[DIM*i+ a], QR[DIM*(i-1) + a]);
CSint *mv_B = cs_Sub(QR[DIM*i+ B], QR[DIM*(i-1) + B]);
CSint *mv_b = cs_Sub(QR[DIM*i+ b], QR[DIM*(i-1) + b]);
CSint *mv_C = cs_Sub(QR[DIM*i+ C], QR[DIM*(i-1) + C]);
CSint *mv_c = cs_Sub(QR[DIM*i+ c], QR[DIM*(i-1) + c]);
CSint *sum_mv = cs_VAdd(6, cs_Abs(mv_A), cs_Abs(mv_a), cs_Abs(mv_B),
cs_Abs(mv_b), cs_Abs(mv_C), cs_Abs(mv_c));
CSint *mv_p_0 = cs_Sub(cs_OccurDomain(0, &QR[DIM*i+A], DIM-1),
cs_OccurDomain(0, &QR[DIM*(i-1)+A], DIM-1));
CSint *mv_p_1 = cs_Sub(cs_OccurDomain(1, &QR[DIM*i+A], DIM-1),
cs_OccurDomain(1, &QR[DIM*(i-1)+A], DIM-1));
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_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(QR_PD[i], QR_PD_END)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(mv_boart, 0)), 0);
cs_LE(sum_mv, 2);
cs_NEQ(cs_Add(cs_ReifNEQ(sum_mv, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(sum_mv, 0), cs_ReifNEQ(mv_boart, 0)), 0);
/*
cs_Eq(mv_boart, Sgn(mv_p_1));
cs_Eq(mv_boart, cs_Sub(CSINT(0), Sgn(mv_p_0)));
*/
cs_NEQ(cs_Add(cs_ReifLE(mv_p_1, 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(mv_p_1, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(mv_p_1, 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifLE(mv_p_0, 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(mv_p_0, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(mv_p_0, 0), cs_ReifEQ(mv_boart, 1)), 0);
}
//exit(1);
// 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;
}
