sunasunaxの日記

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

指定したステップ数でゴールの格子点に到達するをiZ-Cを使って解きます。

指定したステップ数でゴールの格子点に到達するをiZ-Cを使って解きます。
-----------------------------------------------------------------------------
make && ./kohshi 10 29 1
Thu Sep 10 19:57:00 2020
QR:0, 0, {0, 1}, {0, 1}, {0..2}, {0..2}, {0..3}, {0..3}, {0..4}, {0..4}, {0..5}, {0..5}, {0..6}, {0..6}, {
0..7}, {0..7}, {0..8}, {0..8}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0.
.9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {0..9}, {1..9
}, {1..9}, {2..9}, {2..9}, {3..9}, {3..9}, {4..9}, {4..9}, {5..9}, {5..9}, {6..9}, {6..9}, {7..9}, {7..9},
{8, 9}, {8, 9}, 9, 9
ESC[2JESC[0;0fESC[0;0f
Step 29, Solution 1
0 1 2 3 4 5 6 7 8 9
. . . . 15 14 13 12 11 10
. . . . 16 17 18 19 20 21
. . . . . . . . . 22
. . . . . . . . . 23
. . . . . . . . . 24
. . . . . . . . . 25
. . . . . . . . . 26
. . . . . . . . . 27
. . . . . . . . . 28
ESC[0;0f
Step 29, Solution 2
0 1 2 3 4 5 6 7 8 9
. . . . 15 14 13 12 11 10
. . . . 16 17 18 19 20 .
. . . . . . . . 21 22
. . . . . . . . . 23
. . . . . . . . . 24
. . . . . . . . . 25
. . . . . . . . . 26
. . . . . . . . . 27
. . . . . . . . . 28
ESC[0;0f
Step 29, Solution 3
0 1 2 3 4 5 6 7 8 9
. . . . 15 14 13 12 11 10
. . . . 16 17 18 19 20 .
. . . . . . . . 21 .
. . . . . . . . 22 23
. . . . . . . . . 24
. . . . . . . . . 25
. . . . . . . . . 26
. . . . . . . . . 27
. . . . . . . . . 28
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
---------------------------------------------------------------------------------------
/**************************************************************************
* 格子道順
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

int DIM, STP;
CSint **QR, **P_QR;
int *Board;
int DISP;
int ws = 1;
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;

if(DISP == 0) {
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
cs_printf("%A\n", &P_QR[0], STP);
}
else {
printf("\033[0;0f"); /* top cursol */
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
for(i = 0; i < DIM * DIM; i++) Board[i] = -1;
for(i = 0; i < STP; i++){
Board[cs_getValue(P_QR[i])] = i;
if(cs_getValue(P_QR[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( *1;
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 *));
P_QR = (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);
P_QR[i] = cs_VScalProd(2, QR[2*i + 0], QR[2*i + 1], DIM, 1);
}

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

dx = cs_Sub(cx, px);
dy = cs_Sub(cy, py);

cs_EQ(cs_Add(cs_Abs(dx), cs_Abs(dy)), 1);
}

cs_EQ(QR[0], 0);
cs_EQ(QR[1], 0);
cs_EQ(QR[2*(STP - 1) + 0], DIM - 1);
cs_EQ(QR[2*(STP - 1) + 1], DIM - 1);
cs_AllNeq(&P_QR[0], STP);

cs_printf("QR:%A\n", QR, 2*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: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