sunasunaxの日記

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

数独を制約論理プログラム iZ-C を使って解きます。

数独を制約論理プログラム iZ-C を使って解きます。
------------------------------------------------------------------
time ./suudoku
Tue Jul 14 06:01:29 2020

Solution 1
_| 0 1 2 3 4 5 6 7 8
0: 8 7 2 5 1 4 6 3 9
1: 4 6 3 2 7 9 8 5 1
2: 5 9 1 3 6 8 7 2 4
3: 1 3 4 8 5 2 9 6 7
4: 7 8 5 6 9 3 4 1 2
5: 9 2 6 1 4 7 3 8 5
6: 2 4 8 9 3 5 1 7 6
7: 6 5 9 7 8 1 2 4 3
8: 3 1 7 4 2 6 5 9 8

Nb Fails = 230
Nb Choice Points = 396
Heap Size = 1024
Elapsed Time = 0.002847 s
Tue Jul 14 06:01:29 2020

real 0m0.005s
user 0m0.003s
sys 0m0.002s
------------------------------------------------------------------
/**************************************************************************
* 数独
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

#define app4
/******************************************************/
/******************************************************/

#ifdef app1
char INIT_STR[9][9*3] = {
/* 0 1 2 3 4 5 6 7 8 */
/* 0 */ {" . . 5 3 . . . . ."},
/* 1 */ {" 8 . . . . . . 2 ."},
/* 2 */ {" . 7 . . 1 . 5 . ."},
/* 3 */ {" 4 . . . . 5 3 . ."},
/* 4 */ {" . 1 . . 7 . . . 6"},
/* 5 */ {" . . 3 2 . . . 8 ."},
/* 6 */ {" . 6 . 5 . . . . 9"},
/* 7 */ {" . . 4 . . . . 3 ."},
/* 8 */ {" . . . . . 9 7 . ."}};
#endif
/******************************************************/

#ifdef app2
char INIT_STR[9][9*3] = {
/* 0 1 2 3 4 5 6 7 8 */
/* 0 */ {" . . . . . . . . ."},
/* 1 */ {" . . . . . . 2 8 ."},
/* 2 */ {" 3 7 6 4 . . . . ."},
/* 3 */ {" 7 . . . . 1 . . ."},
/* 4 */ {" . 2 . . . . . . ."},
/* 5 */ {" 4 . . 3 . . . . 6"},
/* 6 */ {" . 1 . . 2 8 . . ."},
/* 7 */ {" . . . . . 5 . . ."},
/* 8 */ {" . . . . . . . . 3"}};
#endif
/******************************************************/

#ifdef app3
char INIT_STR[9][9*3] = {
/* 0 1 2 3 4 5 6 7 8 */
/* 0 */ {" 8 7 . . . . 6 . 9"},
/* 1 */ {" . . . 2 . . . . ."},
/* 2 */ {" . 9 . 3 . . . . 4"},
/* 3 */ {" . . 4 . . . 9 . ."},
/* 4 */ {" . 8 . . 9 . . 1 ."},
/* 5 */ {" . . 6 . . . 3 . ."},
/* 6 */ {" 2 . . . . 5 . 7 ."},
/* 7 */ {" . . . . . 1 . . ."},
/* 8 */ {" 3 . 7 . . . . 9 8"}};
#endif
/******************************************************/

#ifdef app4
char INIT_STR[9][9*3] = {
/* 0 1 2 3 4 5 6 7 8 */
/* 0 */ {" 3 8 . 6 . . . . ."},
/* 1 */ {" . . 9 . . . . . ."},
/* 2 */ {" . 2 . . 3 . 5 1 ."},
/* 3 */ {" . . . . . 5 . . ."},
/* 4 */ {" . 3 . . 1 . . 6 ."},
/* 5 */ {" . . . 4 . . . . ."},
/* 6 */ {" . 1 7 . 5 . . 8 ."},
/* 7 */ {" . . . . . . 9 . ."},
/* 8 */ {" . . . . . 7 . 3 2"}};
#endif

/**************************************************************************/
int DIM = 9;
int INIT[9 * 9];
CSint **QR;
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
int i, val;
static int NbSolutions = 0;

// printf("\033[0;0f");
printf("\nSolution %d\n", ++NbSolutions);
printf(" _|");
for (i = 0; i < DIM; i++) {
printf("%3d", i);
}
putchar('\n');
int j=0;
for (i = 0; i < DIM*DIM; i++) {
if*1;

for(i = 0; i < DIM*DIM; i++){
INIT[i] = INIT_STR[i / DIM][2 + 3* (i % DIM)] - '0';
if(INIT[i] < 1 || INIT[i] > 9) INIT[i] = 0;
}
QR = (CSint **)malloc(3*DIM*DIM * sizeof(CSint *));

for(i = 0; i < 3*DIM*DIM; i++){
QR[i] = cs_createCSint(1, 9);
}

for(i = 0; i < DIM*DIM; i++){
QR[DIM*DIM+ DIM*(i % DIM) + i / DIM] = QR[i];
}

for(i = 0; i < 3; i++){
for(j = 0; j < 3; j++){
for(k = 0; k < 9; k++){
QR[2*DIM*DIM + DIM*(3*i + j) + k] = QR[3*DIM*i+3*j + (k/3)*DIM + k%3];
}
}
}

for(i = 0; i < DIM; i++){
cs_AllNeq(&QR[0*DIM*DIM + DIM * i], DIM);
cs_AllNeq(&QR[1*DIM*DIM + DIM * i], DIM);
cs_AllNeq(&QR[2*DIM*DIM + DIM * i], DIM);
}

for(i = 0; i < DIM; i++){
for(j = 0; j < DIM; j++){
int ax = i * DIM + j;

k = INIT[ax];
if(k == 0) continue;
cs_EQ(QR[i * DIM + j], k);
}
}

cs_printf("%A\n", QR, 3*DIM*DIM);

printf("\033[2J\033[0;0f"); /* clear screen */
cs_findAll(&QR[0], 1*DIM*DIM, cs_findFreeVarNbConstraints, 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 % DIM*DIM) == 0) printf("%2d:", j++);
val = cs_getValue(QR[i]);
printf("%3d", val);
if((i+1) % DIM == 0) putchar('\n');
}
}
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i, j, k;
clock_t t0 = clock();
time_t nowtime;

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