ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。最小手数に最適化してゆきます。
ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
解答は板がどの棒に刺さっているかが変化し最小手数に最適化してゆきます。
make && ./hanoi 4 18
make: 'all' に対して行うべき事はありません.
Sun Jan 10 07:51:23 2021
QR:0, 0, 0, 0, {1, 2}, 0, 0, 0, {0..2}, {0..2}, 0, 0, {0..2}, {0..2}, {0..2}, 0, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}
QR_PD:0, {1, 2}, {0..8}, {0..26}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}
Step 18, Solution 1
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 0, 2, 0, 0
4 : 2, 2, 0, 0
5 : 2, 2, 1, 0
6 : 0, 2, 1, 0
7 : 0, 1, 1, 0
8 : 1, 1, 1, 0
9 : 1, 1, 1, 2
10 : 0, 1, 1, 2
11 : 2, 1, 1, 2
12 : 2, 0, 1, 2
13 : 0, 0, 1, 2
14 : 0, 0, 2, 2
15 : 1, 0, 2, 2
16 : 1, 2, 2, 2
17 : 2, 2, 2, 2
Step 17, Solution 2
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 0, 2, 0, 0
4 : 2, 2, 0, 0
5 : 2, 2, 1, 0
6 : 0, 2, 1, 0
7 : 0, 1, 1, 0
8 : 1, 1, 1, 0
9 : 1, 1, 1, 2
10 : 2, 1, 1, 2
11 : 2, 0, 1, 2
12 : 0, 0, 1, 2
13 : 0, 0, 2, 2
14 : 1, 0, 2, 2
15 : 1, 2, 2, 2
16 : 2, 2, 2, 2
Step 16, Solution 3
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 2, 2, 0, 0
4 : 2, 2, 1, 0
5 : 0, 2, 1, 0
6 : 0, 1, 1, 0
7 : 1, 1, 1, 0
8 : 1, 1, 1, 2
9 : 2, 1, 1, 2
10 : 2, 0, 1, 2
11 : 0, 0, 1, 2
12 : 0, 0, 2, 2
13 : 1, 0, 2, 2
14 : 1, 2, 2, 2
15 : 2, 2, 2, 2
Nb Fails = 1923
Nb Choice Points = 2979
Heap Size = 5120
Elapsed Time = 0.027825 s
Sun Jan 10 07:51:23 2021
/**************************************************************************
* ハノイの塔 最小手数に最適化する
BBB
012
0:000
1:200
2:210
3:110
4:112
5:012
6:022
7:222
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"
/**************************************************************************/
CSint **QR;
int QR_PD_END;
CSint **QR_PD;
int DIM, MAX_STP;
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
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) return TRUE;
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution1(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cost);
printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf(" ");
for(i = 0; i < DIM; i++) {
printf("%1d %c", i, (i+1) % DIM == 0 ? '\n' : ' ');
}
for(i = 0; i < step; i++) {
printf("%2d : ", i);
cs_printf("%A\n", &QR[DIM * i], DIM);
}
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;
printf("\nStep %d, Solution %d\n", MAX_STP, ++NbSolutions);
printf(" ");
for(i = 0; i < DIM; i++) {
printf("%1d %c", i, (i+1) % DIM == 0 ? '\n' : ' ');
}
for(i = 0; i < MAX_STP; i++) {
printf("%2d : ", i);
cs_printf("%A\n", &QR[DIM * i], DIM);
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i, j;
clock_t t0 = clock();
time_t nowtime;
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
DIM = atoi(argv[1]);
MAX_STP = atoi(argv[2]);
int *order = (int *)malloc(DIM *sizeof(int));
for(order[0] = 1, i = 0; i < DIM - 1; i++){
order[i + 1] = order[i] * 3;
}
QR_PD_END = order[DIM-1] * 3 - 1;
QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
QR_PD = (CSint **)malloc(MAX_STP * sizeof(CSint *));
for(i = 0; i < MAX_STP; i++){
for(j = 0; j < DIM; j++){
QR[DIM * i + j] = cs_createCSint(0, 2);
}
QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);
}
cs_EQ(QR_PD[0], 0);
for (i = 1; i < MAX_STP; i++){
CSint **curr = (CSint **)malloc(DIM* sizeof(CSint *));
CSint **prev = (CSint **)malloc(DIM* sizeof(CSint *));
CSint **chg = (CSint **)malloc(DIM*MAX_STP * sizeof(CSint *));
for (j = 0; j < DIM; j++){
curr[j] = QR[DIM*i + j];
prev[j] = QR[DIM*(i - 1) + j];
chg[j] = cs_ReifNeq(curr[j], prev[j]);
}
CSint *chg_num = cs_OccurDomain(1, &chg[0], DIM);
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(chg_num, 0), cs_ReifEQ(chg_num, 1));
for (int i = 1; i < DIM; i++){
for (int j = 0; j < i; j++){
imp(cs_ReifEq(prev[i], prev[j]), cs_ReifEq(curr[i], prev[i]));
imp(cs_ReifNeq(prev[i], prev[j]), cs_ReifNeq(prev[j], curr[i]));
}
}
}
cs_printf("QR:%A\n", QR, DIM * MAX_STP);
cs_printf("QR_PD:%A\n", QR_PD, MAX_STP);
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, (void *)(long)QR_PD_END);
CSint *cost = cs_Index(&QR_PD[0], MAX_STP, QR_PD_END);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVarNbConstraints, printSolution);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVarNbElementsMin, printSolution);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVarNbElements, printSolution);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVar, 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;
}
