sunasunaxの日記

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

魔方陣をiZ-Cを使って解きます。

方陣を制約論理プログラム iZ-Cを使って解きます。
-----------------------------------------------------------------------------
time ./magicsqure_simp 4 |less
Thu Jul 16 06:48:10 2020
{0..13}, {0..15}, {0..15}, {1..14}, {0..15}, {0..15}, {0..15}, {0..15}, {0..15}, {0..15}, {0..15}, {0..15}, {2..15}, {0..15}, {0..15}, {1..15}
ESC[2JESC[0;0fESC[0;0f
Solution 1
0 14 13 3
11 5 6 8
7 9 10 4
12 2 1 15
ESC[0;0f
Solution 2
0 13 14 3
11 6 5 8
7 10 9 4
12 1 2 15
ESC[0;0f
Solution 3
0 14 13 3
7 9 10 4
11 5 6 8
12 2 1 15

Solution 880
6 3 13 8
10 15 1 4
5 12 2 11
9 0 14 7

Nb Fails = 39353
Nb Choice Points = 47076
Heap Size = 1024
Elapsed Time = 0.077699 s
Thu Jul 16 06:48:38 2020

real 0m0.080s
user 0m0.073s
sys 0m0.007s

-----------------------------------------------------------------------------

/**************************************************************************
* 魔方陣
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, LIM_MAIN;
CSint **CELL, **tCELL;
CSint **dR, **dL;
IZBOOL knownQueen(int val, int index, CSint **allvars, int NbQueens, void *extra)
{
cs_printf("%A\n", allvars, NbQueens);
return TRUE;
}
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
int i, val;
static int NbSolutions = 0;

printf("\033[0;0f");
printf("\nSolution %d\n", ++NbSolutions);
for (i = 0; i < DIM*DIM; i++) {
val = cs_getValue(CELL[i]);
printf("%3d", val);
if*1 return FALSE;
// if(!cs_isIn(sum, num)) return FALSE;
}
// return cs_EQ(sum, num);
return cs_EQ(cs_Sigma(&array[0], size), num);
}
/**************************************************************************/
CSint *my_Sigma(CSint **array, int size){
int i;
CSint *sum = CSINT(0);
for(i = 0; i < size; i++){
sum = cs_Add(sum, array[i]);
}
return sum;
}
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;

cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
DIM = atoi(argv[1]); LIM_MAIN = DIM*(DIM*DIM-1)/2;

CELL = (CSint **)malloc(DIM*DIM * sizeof(CSint *));
tCELL = (CSint **)malloc(DIM*DIM * sizeof(CSint *));
dR = (CSint **)malloc(DIM * sizeof(CSint *));
dL = (CSint **)malloc(DIM * sizeof(CSint *));

for(i = 0; i < DIM*DIM; i++){
CELL[i] = cs_createCSint(0, DIM*DIM-1);
}

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

for(i = 0; i < DIM; i++){
/*
cs_EQ(my_Sigma(&CELL[DIM*i], DIM), LIM_MAIN);
cs_EQ(my_Sigma(&tCELL[DIM*i], DIM), LIM_MAIN);
*/
jg_my_Sigma(&CELL[DIM*i], DIM, LIM_MAIN);
jg_my_Sigma(&tCELL[DIM*i], DIM, LIM_MAIN);
}

for(i = 0; i < DIM; i++){
dR[i] = CELL[(DIM+1)*i];
dL[i] = CELL[(DIM-1)*(i+1)];
}
cs_AllNeq(&CELL[0], DIM*DIM);

/*
cs_EQ(my_Sigma(dR, DIM), LIM_MAIN);
cs_EQ(my_Sigma(dL, DIM), LIM_MAIN);
*/
jg_my_Sigma(dR, DIM, LIM_MAIN);
jg_my_Sigma(dL, DIM, LIM_MAIN);

cs_Lt(CELL[0], CELL[DIM-1]);
cs_Lt(CELL[DIM-1], CELL[DIM*(DIM-1)]);
cs_Lt(CELL[0], CELL[DIM*DIM-1]);

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

// cs_eventKnown(&CELL[0], DIM*DIM, knownQueen, NULL);

printf("\033[2J\033[0;0f"); /* clear screen */
cs_findAll(&CELL[0], 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+1) % DIM == 0) putchar('\n');
}
}
/**************************************************************************/
IZBOOL jg_my_Sigma(CSint **array, int size, int num){
int i;
CSint *sum = CSINT(0);
for(i = 0; i < -size; i++){
sum = cs_Add(sum, array[i]);
// if(cs_getMin(sum) > num) return FALSE;
// if(!cs_LE(sum, num