ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
解答は板がどの棒に刺さっているかが変化してゆきます。
./hanoi 4 16
Sat Jul 25 08:34:08 2020
QR:0, 0, 0, 0, 1, 0, 0, 0, 1, 2, 0, 0, 2, 2, 0, 0, 2, 2, 1, 0, 0, 2, 1, 0, 0, {0..2}, {0..2}, 0, 1, {0..2}, {0..2}, 0, 1, {0..2}, {0..2}, {0..2}, 2, {0..2}, {0..2}, {0..2}, 2, {0..2}, {0..2}, {0..2}, 0, {0..2}, {0..2}, {0..2}, 0, {0..2}, {0..2}, {0..2}, 1, {0..2}, {0..2}, {0..2}, 1, 2, 2, 2, 2, 2, 2, 2
DIFF_QR:1, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 0, {0, 1}, {0, 1}, 0, 1, 0, 0, 0, 0, {0, 1}, {0, 1}, {0, 1}, 1, 0, 0, 0, 0, {0, 1}, {0, 1}, {0, 1}, 1, 0, 0, 0, 0, {0, 1}, {0, 1}, {0, 1}, 1, 0, 0, 0, 0, {0, 1}, {0, 1}, {0, 1}, 1, 0, 0, 0
Step 16, Solution 1
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 = 2
Nb Choice Points = 3
Heap Size = 4096
Elapsed Time = 0.002203 s
Sat Jul 25 08:34:08 2020
---------------------------------------------------------------------------
/**************************************************************************
* ハノイの塔
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, **DIFF_QR, **dif_comb;
int DIM, STP;
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR(int val, int index, CSint **allvars, int size, void *extra) {
int i;
// printf("#%2d: %2d\n", index, val);
printf("#%2d:%2d,%2d: %2d\n", index, index / DIM, index % DIM, val);
for(i=0; i< STP; i++){
cs_printf("%2d # %A\n", i, &QR[DIM * i], DIM);
// if(i < STP -1) cs_printf(" %A\n", &DIFF_QR[DIM * i], DIM);
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
printf(" ");
for(i = 0; i < DIM; i++) {
printf("%1d %c", i, (i+1) % DIM == 0 ? '\n' : ' ');
}
for(i = 0; i < 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]);
STP = atoi(argv[2]);
QR = (CSint **)malloc(DIM * STP * sizeof(CSint *));
DIFF_QR = (CSint **)malloc(DIM * STP * sizeof(CSint *));
dif_comb = (CSint **)malloc(DIM * STP*STP/2 * sizeof(CSint *));
for(j = 0; j < STP; j++){
for(i = 0; i < DIM; i++){
QR[DIM * j + i] = cs_createCSint(0, 2);
}
}
for(i = 0; i < DIM; i++){
cs_EQ(QR[i], 0);
cs_EQ(QR[DIM * (STP-1) + i], 2);
}
for (i = 1; i < STP - 1; i++){
switch (((i - 1) % 6) / 2) {
case 0 : cs_EQ(QR[DIM * i + 0], 1 + (DIM % 2)); break;
case 1 : cs_EQ(QR[DIM * i + 0], 2 - (DIM % 2)); break;
case 2 : cs_EQ(QR[DIM * i + 0], 0); break;
}
}
for (j = 0; j < STP - 1; j++){
for(i = 0; i < DIM; i++){
DIFF_QR[DIM * j + i] = cs_ReifNeq(QR[DIM * j + i], QR[DIM * (j + 1) + i]);
}
// cs_OccurConstraints(CSINT(1), 1, &DIFF_QR[DIM * j], DIM);
cs_EQ(cs_Sigma(&DIFF_QR[DIM * j], DIM), 1);
}
for (j = 0; j < STP - 2; j++){
// cs_Neq(DIFF_QR[DIM * (j + 1) + 0], DIFF_QR[DIM * j + 0]);
for(i = 0; i < DIM; i++){
cs_NEQ(cs_Add(cs_ReifNEQ(DIFF_QR[DIM * j + i], 1), cs_ReifEQ(DIFF_QR[DIM * (j + 1) + i], 0)), 0);
}
}
for (j = 0; j < STP - 1; j++){
for(i = 1; i < DIM; i++){
for(int k = 0; k < i; k++){
cs_NEQ(cs_Add(cs_ReifNEQ(DIFF_QR[DIM * j + i], 1),
cs_ReifNeq(QR[DIM * j + i], QR[DIM * j + k])), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(DIFF_QR[DIM * j + i], 1),
cs_ReifNeq(QR[DIM * (j + 1) + i], QR[DIM * j + k])), 0);
}
}
}
int n = 0;
for (j = 0; j < STP - 1; j++){
for(i = j + 1; i < STP; i++){
for(int k = 0; k < DIM; k++){
dif_comb[DIM * n + k] = cs_ReifEq(QR[DIM * j + k], QR[DIM * i + k]);
}
cs_NEQ(cs_Sigma(&dif_comb[DIM * n++], DIM), DIM);
}
}
cs_printf("QR:%A\n", QR, DIM * STP);
cs_printf("DIFF_QR:%A\n", DIFF_QR, DIM * (STP - 1));
// cs_eventKnown(&QR[0], DIM * STP, knownQR, NULL);
// cs_findAll(&QR[0], DIM * STP, cs_findFreeVarNbConstraints, printSolution);
// cs_findAll(&QR[0], DIM * STP, cs_findFreeVarNbElementsMin, printSolution);
cs_findAll(&QR[0], DIM * STP, cs_findFreeVarNbElements, printSolution);
// cs_findAll(&QR[0], DIM * STP, cs_findFreeVar, printSolution);
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;
}
