sunasunaxの日記

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

ナンバーリンクをiZ-Cを使って解きます。

ナンバーリンクをiZ-Cを使って解きます。
-----------------------------------------------------------------------------
make && ./num_link 10 1 3 3 7 7 11 2 2 8 8 15 1 1 6 7 12
Sun Sep 13 11:13:36 2020
10, 1
3 3 7 7 11
QR:3, 3, {2..4}, {2..4}, {1..5}, {1..5}, {0..6}, {0..6}, {1..7}, {1..7}, {2..8}, {2..8}, {3..9}, {3..9}, {4..9}, {4..9}, {5..9}, {5..9}, {6..8}, {6..8}, 7, 7, 2, 2, {1..3}, {1..3}, {0..4}, {0..4}, {0..5}, {0..5}, {0..6}, {0..6}, {0..7}, {0..7}, {0..8}, {0..8}, {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, 8, 1, 1, {0..2}, {0..2}, {0..3}, {0..3}, {0..4}, {0..4}, {0..5}, {0..5}, {0..6}, {1..6}, {1..7}, {2..7}, {2..8}, {3..8}, {3..9}, {4..9}, {4..8}, {5..9}, {5..7}, {6..8}, 6, 7
ESC[2JESC[0;0fESC[0;0f
Step 38, Solution 1
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 18 6 35 . .
. . . . . 19 7 36 . .
. . . . . 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
ESC[0;0f
Step 38, Solution 2
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 . 6 35 . .
. . . . 18 19 7 36 . .
. . . . . 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
ESC[0;0f
Step 38, Solution 3
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 . 6 35 . .
. . . . 18 . 7 36 . .
. . . . 19 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Step 38, Solution 614726
. . . . . . . . . .
. 26 27 28 . . . . . .
. . 11 29 30 . . . . .
. . 12 0 31 . . . . .
. . 13 1 32 . . . . .
. . 14 2 33 . . . . .
. . 15 3 34 35 36 37 . .
. . 16 4 . . . 10 . .
. . 17 5 6 7 8 9 25 .
. . 18 19 20 21 22 23 24 .

Nb Fails = 6395740
Nb Choice Points = 12168382
Heap Size = 3072
Elapsed Time = 38.5832 s
Sun Sep 13 11:15:22 2020
----------------------------------------------------------------------------
/**************************************************************************
* 格子道順
**************************************************************************/
#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]);
DISP = atoi(argv[2]);
int SET_NUM = (argc -3)/5;
STP = 0;
for(i = 0; i < SET_NUM; i++){
for(j = 0; j < 5; j++){
NUM_SET[i][j] = atoi(argv[3 + 5 * i + j]);
}
STP += NUM_SET[i][4];
}
printf("%3d, %3d\n", DIM, DISP);
for(j = 0; j < 5; j++) printf("%4d", NUM_SET[0][j]);
putchar('\n');

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);
}

int pre_STP = 0;
for (j = 0; j < SET_NUM; j++){
cs_EQ(QR[2*pre_STP + 0], NUM_SET[j][0]);
cs_EQ(QR[2*pre_STP + 1], NUM_SET[j][1]);
//exit(1);
cs_EQ(QR[2*(pre_STP + NUM_SET[j][4] - 1) + 0], NUM_SET[j][2]);
cs_EQ(QR[2*(pre_STP + NUM_SET[j][4] - 1) + 1], NUM_SET[j][3]);
for (i = pre_STP + 1; i < pre_STP + NUM_SET[j][4]; 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);
}
pre_STP += NUM_SET[j][4];
}

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, j;
int NUM_SET[10][5];
clock_t t0 = clock();
time_t nowtime;

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