sunasunaxの日記

制約論理プログラム iZ-C の紹介

格子道順ふかしぎ お姉さんといっしょに数えてみよう。をiZ-Cで解きます。

格子道順ふかしぎ お姉さんといっしょに数えてみよう。をiZ-Cで解きます。
------------------------------------------------------
aa=5; make && ./kohshi $aa $*1 1

Thu Nov 19 06:13:49 2020
QR:0, 0, {0, 1}, {0, 1}, {0..2}, {0..2}, {0..3}, {0..3}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}
ESC[2JESC[0;0fESC[0;0f
Step 25, Solution 1
0 9 10 19 20
1 8 11 18 21
2 7 12 17 22
3 6 13 16 23
4 5 14 15 24
ESC[0;0f
Step 23, Solution 2
0 9 10 . .
1 8 11 18 19
2 7 12 17 20
3 6 13 16 21
4 5 14 15 22
ESC[0;0f
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Step 11, Solution 8511
0 1 2 3 4
. . . . 5
. . . . 6
. . . 8 7
. . . 9 10
ESC[0;0f
Step 9, Solution 8512
0 1 2 3 4
. . . . 5
. . . . 6
. . . . 7
. . . . 8

Nb Fails = 48504
Nb Choice Points = 92280
Heap Size = 2048
Elapsed Time = 0.357649 s
Thu Nov 19 06:14:24 2020

/**************************************************************************
* 格子道順
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

int DIM, STP;
CSint **QR, **PQR;
int *Board;
int DISP;
int ws = 1;
/**************************************************************************/
/**************************************************************************/
IZBOOL knownPQR(int val, int index, CSint **allvars, int size, void *extra) {
int i;

if(val == DIM * DIM -1) return TRUE;
for(i = 0; i < STP; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cs_Index(&PQR[0], STP, DIM * DIM - 1));

if(DISP == 0) {
printf("\nStep %2d, Solution %6d\n", step, ++NbSolutions);
cs_printf("%A\n", &PQR[0], step);
}
else {
printf("\033[0;0f"); /* top cursol */
printf("\nStep %2d, Solution %6d\n", step, ++NbSolutions);
for(i = 0; i < DIM * DIM; i++) Board[i] = -1;
for(i = 0; i < step; i++){
Board[cs_getValue(PQR[i])] = i;
if(cs_getValue(PQR[i]) == DIM * DIM -1) break;
}

for(i = 0; i < DIM * DIM; i++) {
if(Board[i] == -1) printf("%*c", ws, '.');
else printf("%*d", ws, Board[i]);
if( *2;
DIM = atoi(argv[1]);
STP = atoi(argv[2]);
DISP = atoi(argv[3]);

int tt = DIM * DIM - 1;
while(tt){ ws++; tt /= 10; }

QR = (CSint **)malloc(2 * STP * sizeof(CSint *));
PQR = (CSint **)malloc(STP * sizeof(CSint *));
Board = (int *)malloc(DIM * DIM * sizeof(int));

for(i = 0; i < STP; i++){
QR[2*i + 0] = cs_createCSint(0, DIM - 1);
QR[2*i + 1] = cs_createCSint(0, DIM - 1);
PQR[i] = cs_VScalProd(2, QR[2*i + 1], QR[2*i + 0], DIM, 1);
}

for (i = 1; i < STP; i++){
CSint *px = QR[2*(i-1) + 0], *py = QR[2*(i-1) + 1];
CSint *cx = QR[2*i + 0], *cy = QR[2*i + 1];
CSint *dx = cs_Sub(cx, px), *dy = cs_Sub(cy, py);

CSint *f_c = cs_ReifEQ(cs_Add(cs_Abs(dx), cs_Abs(dy)), 1);
CSint *f_p = cs_ReifEQ(PQR[i - 1], DIM*DIM - 1);
CSint *nf_p = cs_ReifNEQ(PQR[i - 1], DIM*DIM - 1);
CSint *end_pqr = cs_ReifEQ(PQR[i], DIM*DIM - 1);

cs_NEQ(cs_Add(f_p, f_c), 0);
cs_NEQ(cs_Add(nf_p, end_pqr), 0);
}

cs_EQ(PQR[0], 0);
cs_EQ(PQR[STP - 1], DIM*DIM - 1);
cs_eventKnown(&PQR[0], STP, knownPQR, NULL);

cs_printf("QR:%A\n", QR, STP);

if(DISP == 1) printf("\033[2J\033[0;0f"); /* clear screen */
// cs_findAll(&QR[0], 2* STP, cs_findFreeVarNbConstraints, printSolution);
cs_findAll(&QR[0], 2* 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;
}

*1:$aa**2

*2:i+1) % DIM) == 0) putchar('\n');
}
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;

cs_init();
time(&nowtime); printf("%s", ctime(&nowtime