最小手数で家族の川渡りを制約論理プログラム iZ-Cを使って解きます。
最小手数で家族の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
aa=22; make && ./river_family $aa
make: 'all' に対して行うべき事はありません.
Sat Jan 16 20:38:34 2021
QR: 0, 0, 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}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {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..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}
Step 18, Solution 1
boart = 0, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8
0: 0, 0, 0, 0, 0, 0, 0, 0, 0 [b,d,m,f,M,S,s,G,g] [ , , , , , , , , ]
1: 1, 1, 1, 0, 0, 0, 0, 0, 0 [ , , ,f,M,S,s,G,g] [b,d,m, , , , , , ]
2: 0, 1, 0, 0, 0, 0, 0, 0, 0 [b, ,m,f,M,S,s,G,g] [ ,d, , , , , , , ]
3: 1, 1, 1, 0, 0, 0, 0, 0, 1 [ , , ,f,M,S,s,G, ] [b,d,m, , , , , ,g]
4: 0, 0, 0, 0, 0, 0, 0, 0, 1 [b,d,m,f,M,S,s,G, ] [ , , , , , , , ,g]
5: 1, 0, 0, 0, 1, 0, 0, 1, 1 [ ,d,m,f, ,S,s, , ] [b, , , ,M, , ,G,g]
6: 0, 0, 0, 0, 0, 0, 0, 1, 1 [b,d,m,f,M,S,s, , ] [ , , , , , , ,G,g]
7: 1, 0, 0, 1, 1, 0, 0, 1, 1 [ ,d,m, , ,S,s, , ] [b, , ,f,M, , ,G,g]
8: 0, 0, 0, 0, 1, 0, 0, 1, 1 [b,d,m,f, ,S,s, , ] [ , , , ,M, , ,G,g]
9: 1, 1, 1, 0, 1, 0, 0, 1, 1 [ , , ,f, ,S,s, , ] [b,d,m, ,M, , ,G,g]
10: 0, 1, 1, 0, 0, 0, 0, 1, 1 [b, , ,f,M,S,s, , ] [ ,d,m, , , , ,G,g]
11: 1, 1, 1, 1, 1, 0, 0, 1, 1 [ , , , , ,S,s, , ] [b,d,m,f,M, , ,G,g]
12: 0, 1, 1, 0, 1, 0, 0, 1, 1 [b, , ,f, ,S,s, , ] [ ,d,m, ,M, , ,G,g]
13: 1, 1, 1, 1, 1, 0, 1, 1, 1 [ , , , , ,S, , , ] [b,d,m,f,M, ,s,G,g]
14: 0, 0, 0, 1, 1, 0, 1, 1, 1 [b,d,m, , ,S, , , ] [ , , ,f,M, ,s,G,g]
15: 1, 0, 1, 1, 1, 1, 1, 1, 1 [ ,d, , , , , , , ] [b, ,m,f,M,S,s,G,g]
16: 0, 0, 0, 1, 1, 1, 1, 1, 1 [b,d,m, , , , , , ] [ , , ,f,M,S,s,G,g]
17: 1, 1, 1, 1, 1, 1, 1, 1, 1 [ , , , , , , , , ] [b,d,m,f,M,S,s,G,g]
Nb Fails = 356
Nb Choice Points = 727
Heap Size = 18432
Elapsed Time = 0.008341 s
Sat Jan 16 20:38:34 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;
enum {boart, dog, maid, father, mother, son1, son2, daughter1, daughter2};
/**************************************************************************/
/**************************************************************************/
void imp(CSint *cond, CSint *exe){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe), 0);
}
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
imp(cs_ReifEQ(cond, 1), exe1);
imp(cs_ReifEQ(cond, 0), exe2);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;
int END = (long int)(int *)extra;
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){
//enum {boart, dog, maid, father, mother, son1, son2, daughter1, daughter2};
char alph[9] ={"bdmfMSsGg"};
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, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8\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, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8\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 = 9;
QR_PD_END = (1 << DIM) - 1;
// int order[9] ={1, 2, 4, 8, 16, 32, 64, 128, 256};
int *order =(int *)malloc(DIM * sizeof(int));
for(i = 0; i < DIM; i++) order[i] = 1 << i;
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);
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);
}
//enum {boart, dog, maid, father, mother, son1, son2, daughter1, daughter2};
for(i = 1; i < MAX_STP; i++){
CSint **curr_pos = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **prev_pos = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **mv = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **chg = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
curr_pos[j] = QR[DIM * i + j];
prev_pos[j] = QR[DIM * (i - 1) + j];
mv[j] = cs_Sub(curr_pos[j], prev_pos[j]);
chg[j] = cs_ReifNEQ(mv[j], 0);
}
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(mv[boart], 0), cs_ReifNEQ(mv[boart], 0));
cs_LE(cs_Sigma(&chg[dog], DIM-1), 2);
for(int j = 1; j < DIM; j++){
CSint *mv_bt_j = cs_ReifEQ(mv[boart + j], 0);
for(int k = -1; k <= 1; k++){
imp(cs_ReifEQ(mv[boart], k), cs_ReifNEQ(cs_Add(cs_ReifEQ(mv[boart + j], k), mv_bt_j), 0));
}
}
CSint **mv_eq_boart = (CSint **)malloc(3 * sizeof(CSint *));
for(int k = 0; k < 3; k++) mv_eq_boart[k] = cs_ReifEq(mv[boart], mv[maid + k]);
imp(cs_ReifNEQ(mv[boart], 0), cs_ReifNEQ(cs_Sigma(&mv_eq_boart[0], 3), 0));
CSint *curr_pos_fath_moth = cs_ReifNeq(curr_pos[father], curr_pos[mother]);
imp(curr_pos_fath_moth,
cs_ReifEQ(cs_Add(cs_ReifEq(curr_pos[mother], curr_pos[son1]),
cs_ReifEq(curr_pos[mother], curr_pos[son2])), 0));
imp(curr_pos_fath_moth,
cs_ReifEQ(cs_Add(cs_ReifEq(curr_pos[father], curr_pos[daughter1]),
cs_ReifEq(curr_pos[father], curr_pos[daughter2])), 0));
CSint **curr_pos_eq_dog = (CSint **)malloc(6 * sizeof(CSint *));
for(int k = 0; k < 6; k++) curr_pos_eq_dog[k] = cs_ReifEq(curr_pos[dog], curr_pos[father + k]);
imp(cs_ReifNeq(curr_pos[dog], curr_pos[maid]), cs_ReifEQ(cs_Sigma(&curr_pos_eq_dog[0], 6), 0));
}
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);
// 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;
}
