改良版： ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
改良版： ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
aa=5; make && ./hanoi $aa $*1
make: 'all' に対して行うべき事はありません.
Fri Jan 22 15:58:49 2021
QR:0, 0, 0, 0, 0, {1, 2}, 0, 0, 0, 0, {1, 2}, {0..2}, 0, 0, 0, {0..2}, {0..2}, {0..2}, 0, 0, {0..2}, {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}, {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}, {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}, {1..8}, {0..26}, {0..80}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}
Step 32, Solution 1
0 1 2 3 4
0 : 0, 0, 0, 0, 0
1 : 2, 0, 0, 0, 0
2 : 2, 1, 0, 0, 0
3 : 1, 1, 0, 0, 0
4 : 1, 1, 2, 0, 0
5 : 0, 1, 2, 0, 0
6 : 0, 2, 2, 0, 0
7 : 2, 2, 2, 0, 0
8 : 2, 2, 2, 1, 0
9 : 1, 2, 2, 1, 0
10 : 1, 0, 2, 1, 0
11 : 0, 0, 2, 1, 0
12 : 0, 0, 1, 1, 0
13 : 2, 0, 1, 1, 0
14 : 2, 1, 1, 1, 0
15 : 1, 1, 1, 1, 0
16 : 1, 1, 1, 1, 2
17 : 0, 1, 1, 1, 2
18 : 0, 2, 1, 1, 2
19 : 2, 2, 1, 1, 2
20 : 2, 2, 0, 1, 2
21 : 1, 2, 0, 1, 2
22 : 1, 0, 0, 1, 2
23 : 0, 0, 0, 1, 2
24 : 0, 0, 0, 2, 2
25 : 2, 0, 0, 2, 2
26 : 2, 1, 0, 2, 2
27 : 1, 1, 0, 2, 2
28 : 1, 1, 2, 2, 2
29 : 0, 1, 2, 2, 2
30 : 0, 2, 2, 2, 2
31 : 2, 2, 2, 2, 2
Nb Fails = 70
Nb Choice Points = 143
Heap Size = 21504
Elapsed Time = 0.026379 s
Fri Jan 22 15:58:49 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 (j = 0; j < DIM; j++){
int k = 1 << j;
if(i < MAX_STP - k){
for (int l = 1; l < k + 1; l++){
imp(cs_ReifEQ(chg[j], 1), cs_ReifEq(QR[DIM*(i + l) + j], curr[j]));
}
}
}
for (j = 1; j < DIM; j++){
for (int k = 0; k < j; k++){
CSint *eq_prev = cs_ReifEq(prev[k], prev[j]);
imp(eq_prev, cs_ReifEq(curr[j], prev[j]));
imp(cs_ReifEq(prev[k], curr[j]), eq_prev);
}
}
}
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;
}
*1:2**aa + 1
