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

複合魔方陣を制約論理プログラム iZ-Cを使って解きます。

複合魔方陣を制約論理プログラム iZ-Cを使って解きます。
-----------------------------------------------------------------------------
make && ./chk_mcons
gcc -Wall -O3 -I. -L. -o chk_mcons chk_mcons.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Tue Sep 8 17:51:42 2020

Solution 1 (NbFails = 613):
# . . . . . # #
# . . . . # . .
# # # # # . . .
. # # # # # # #
. . . . # # . .
. # # # # . . #
. . . . . . # .
. . . . . . . .

Solution 2 (NbFails = 613):
# . . . . . # #
# . . . . # . .
# # # # # . . .
. # # # # # # #
. . . . # # . .
. # # # # . # .
. . . . . . . #
. . . . . . . .

Solution 3 (NbFails = 647):
# . . . . # # .
# . . . . . . #
# # # # # . . .
. # # # # # # #
. . . . # # . .
. # # # # . . #
. . . . . . # .
. . . . . . . .

Solution 4 (NbFails = 647):
# . . . . # # .
# . . . . . . #
# # # # # . . .
. # # # # # # #
. . . . # # . .
. # # # # . # .
. . . . . . . #
. . . . . . . .

Nb Fails = 700
Nb Choice Points = 1406
Heap Size = 3072
Elapsed Time = 0.002062s
Tue Sep 8 17:51:42 2020
---------------------------------------------------------------------------------
#include <stdlib.h>
#include <time.h>
#include "iz.h"

#define app1

/********************************************************************************************/
#ifdef app1

#define N 8
int row_1 = {2, 1, 2};
int row_2 = {2, 1, 1};
int row_3 = {1, 5};
int row_4 = {1, 7};
int row_5 = {1, 2};
int row_6 = {2, 4, 1};
int row_7 = {1, 1};
int row_8 = {0};

int col_1 = {1, 3};
int col_2 = {2, 2, 1};
int col_3 = {2, 2, 1};
int col_4 = {2, 2, 1};
int col_5 = {1, 4};
int col_6 = {2, 1, 2};
int col_7 = {3, 1, 1, 1};
int col_8 = {3, 1, 1, 1};

int *row[N] = {row_1, row_2, row_3, row_4, row_5, row_6, row_7, row_8};
int *col[N] = {col_1, col_2, col_3, col_4, col_5, col_6, col_7, col_8};

#endif

/********************************************************************************************/
#ifdef app2

#define N 8
int row_1 = {1, 4};
int row_2 = {2, 2, 2};
int row_3 = {2, 2, 2};
int row_4 = {1, 8};
int row_5 = {1, 2};
int row_6 = {2, 2, 2};
int row_7 = {2, 2, 2};
int row_8 = {1, 4};
int col_1 = {1, 4};
int col_2 = {1, 6};
int col_3 = {3, 2, 1, 2};
int col_4 = {3, 1, 1, 1};
int col_5 = {3, 1, 1, 1};
int col_6 = {3, 2, 1, 2};
int col_7 = {2, 3, 2};
int col_8 = {2, 2, 1};

int *row[N] = {row_1, row_2, row_3, row_4, row_5, row_6, row_7, row_8};
int *col[N] = {col_1, col_2, col_3, col_4, col_5, col_6, col_7, col_8};

#endif

/********************************************************************************************/
#ifdef app4

#define N 8
int row_1 = {1, 4};
int row_2 = {1, 4};
int row_3 = {1, 4};
int row_4 = {1, 4};
int row_5 = {0};
int row_6 = {0};
int row_7 = {0};
int row_8 = {0};

int col_1 = {1, 4};
int col_2 = {1, 4};
int col_3 = {1, 4};
int col_4 = {1, 4};
int col_5 = {0};
int col_6 = {0};
int col_7 = {0};
int col_8 = {0};

int *row[N] = {row_1, row_2, row_3, row_4, row_5, row_6, row_7, row_8};
int *col[N] = {col_1, col_2, col_3, col_4, col_5, col_6, col_7, col_8};

#endif

/********************************************************************************************/
#ifdef app3

#define N 8
int row_1 = {1, 6};
int row_2 = {2, 1, 1};
int row_3 = {2, 1, 1};
int row_4 = {1, 6};
int row_5 = {1, 1};
int row_6 = {1, 1};
int row_7 = {1, 1};
int row_8 = {1, 1};

int col_1 = {1, 8};
int col_2 = {2, 1, 1};
int col_3 = {2, 1, 1};
int col_4 = {2, 1, 1};
int col_5 = {2, 1, 1};
int col_6 = {2, 1, 1};
int col_7 = {1, 2};
int col_8 = {0};

int *row[N] = {row_1, row_2, row_3, row_4, row_5, row_6, row_7, row_8};
int *col[N] = {col_1, col_2, col_3, col_4, col_5, col_6, col_7, col_8};

#endif

/********************************************************************************************/
#ifdef app10

#define N 15
int row_01 = {2, 1, 1};
int row_02 = {2, 2, 2};
int row_03 = {1, 9};
int row_04 = {2, 4, 6};
int row_05 = {2, 1, 7};
int row_06 = {4, 3, 1, 1, 5};
int row_07 = {4, 1, 1, 2, 3};
int row_08 = {2, 2, 5};
int row_09 = {2, 3, 4};
int row_10 = {2, 4, 1};
int row_11 = {2, 3, 1};
int row_12 = {1, 10};
int row_13 = {3, 2, 3, 2};
int row_14 = {1, 7};
int row_15 = {1, 5};

int col_01 = {1, 3};
int col_02 = {2, 1, 1};
int col_03 = {2, 1, 7};
int col_04 = {2, 4, 6};
int col_05 = {2, 2, 6};
int col_06 = {5, 1, 2, 1, 1, 2};
int col_07 = {2, 1, 4};
int col_08 = {3, 1, 2, 4};
int col_09 = {3, 1, 5, 4};
int col_10 = {4, 3, 2, 1, 2};
int col_11 = {2, 8, 3};
int col_12 = {1, 13};
int col_13 = {1, 4};
int col_14 = {1, 3};
int col_15 = {1, 3};

int *row[N] = {row_01, row_02, row_03, row_04, row_05, row_06, row_07, row_08, row_09, row_10,
row_11, row_12, row_13, row_14, row_15};
int *col[N] = {col_01, col_02, col_03, col_04, col_05, col_06, col_07, col_08, col_09, col_10,
col_11, col_12, col_13, col_14, col_15};

#endif

/********************************************************************************************/
/********************************************************************************************/
void printSolution(CSint **allvars, int nbVars)
{
int i, j, n = 0;
static int NbSolution = 0;

printf("\nSolution %d (NbFails = %d):\n", ++NbSolution, cs_getNbFails());
for (i = 0; i < N; i++) {
for (j = 0; j < N; j++){
int nn = cs_getValue(allvars[n++]);
if(nn == 0) printf(" .");
else printf(" #");
}
putchar('\n');
}
/*
for (i = 0; i < N; i++) {
if(cs_getValue(cs_Sigma(&allvars[N * i], N)) == 0) {printf("_\n");}
else
cs_printf("%D\n", cs_Index(&allvars[N * i], N, 1));
}
*/
}
/********************************************************************************************/
/********************************************************************************************/
IZBOOL knownRC(int val, int index, CSint **allvars, int size, void *mat_allvars) {
if(val == 0) return TRUE;
int r = index / N, c = index % N;
CSint *pre_step = cs_Sigma(&allvars[index - c], c + 1);
int step = cs_getMin(pre_step);
int r_p = (index + row[r][step] -1) / N;
if( r != r_p) return FALSE;
return
cs_OccurConstraints(CSINT(row[r][step]), 1, (CSint **)mat_allvars + index, row[r][step]);

}
/********************************************************************************************/
/********************************************************************************************/
IZBOOL knownCR(int val, int index, CSint **allvars, int size, void *mat_allvars) {
if(val == 0) return TRUE;
int r = index / N, c = index % N;
CSint *pre_step = cs_Sigma(&allvars[index - c], c + 1);
int step = cs_getMin(pre_step);
int r_p = (index + col[r][step] -1) / N;
if( r != r_p) return FALSE;
return
cs_OccurConstraints(CSINT(col[r][step]), 1, (CSint **)mat_allvars + index, col[r][step]);

}
/********************************************************************************************/
/********************************************************************************************/
/********************************************************************************************/
int main(int argc, char **argv)
{
clock_t t0 = clock();
time_t nowtime;

CSint *matrixRC[N][N], *edgeRC[N][N];
CSint *matrixCR[N][N], *edgeCR[N][N];
CSint *allvars[N * N];
CSint *all_edgeRC[N * N], *all_edgeCR[N * N];
int i, j, n = 0;

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

n = 0;
for (i = 0; i < N; i++){
for (j = 0; j < N; j++){
allvars[n++] = matrixCR[j][i] = matrixRC[i][j] = cs_createCSint(0, 1);
}
}

for (i = 0; i < N; i++){
edgeRC[i][0] = cs_ReifEQ(matrixRC[i][0], 1);
edgeCR[i][0] = cs_ReifEQ(matrixCR[i][0], 1);
for (j = 1; j < N; j++){
edgeRC[i][j] = cs_ReifEQ(cs_Add(cs_ReifEQ(matrixRC[i][j-1], 0), cs_ReifEQ(matrixRC[i][j], 1)), 2);
edgeCR[i][j] = cs_ReifEQ(cs_Add(cs_ReifEQ(matrixCR[i][j-1], 0), cs_ReifEQ(matrixCR[i][j], 1)), 2);
}
}
for (i = 0; i < N; i++){
cs_OccurConstraints(CSINT(row[i][0]), 1, edgeRC[i], N);
cs_OccurConstraints(CSINT(col[i][0]), 1, edgeCR[i], N);
}
n = 0;
for (i = 0; i < N; i++){
for (j = 0; j < N; j++){
all_edgeRC[n] = edgeRC[i][j];
all_edgeCR[n++] = edgeCR[i][j];
}
}

for (i = 0; i < N; i++){
int row_sum = 0, col_sum = 0;
for (j = 1; j <= row[i][0]; j++){
row_sum += row[i][j];
}
for (j = 1; j <= col[i][0]; j++){
col_sum += col[i][j];
}
cs_OccurConstraints(CSINT(row_sum), 1, matrixRC[i], N);
cs_OccurConstraints(CSINT(col_sum), 1, matrixCR[i], N);
}


/*
printf("matrixRC \n");
for (i = 0; i < N; i++){
cs_printf("%A\n", matrixRC[i], N);
}
printf("edgeRC \n");
for (i = 0; i < N; i++){
cs_printf("%A\n", edgeRC[i], N);
}
cs_printf("RC: %A\n", &all_edgeRC[0], N * N);
cs_printf("CR: %A\n", &all_edgeCR[0], N * N);
*/

cs_eventKnown(&all_edgeRC[0], N * N, knownRC, (void *)allvars);
CSint *Tallvars[N * N];
n = 0;
for (i = 0; i < N; i++){
for (j = 0; j < N; j++){
Tallvars[n++] = matrixCR[i][j];
}
}
cs_eventKnown(&all_edgeCR[0], N * N, knownCR, (void *)Tallvars);

cs_findAll(allvars, N * N, cs_findFreeVar, printSolution);

cs_printStats();
printf("Elapsed Time = %fs\n", (double) (clock() - t0) / CLOCKS_PER_SEC);
time(&nowtime); printf("%s", ctime(&nowtime));
cs_end();
return EXIT_SUCCESS;
}

 

Tutorial Sgn定義は誤りだろう。

Tutorial Sgn定義は誤りだろう。
-----------------------------------------------------------------------------
CSint *Sgn(CSint *vint)
{
int n = 0;
int array[3];
CSint *s;
if (cs_getMin(vint) < 0)
array[n++] = -1;
if (cs_getMax(vint) > 0)
array[n++] = 1;
if (cs_isIn(vint, 1))
array[n++] = 0;
s = cs_createCSintFromDomain(array, n);
-----------------------------------------------------------------------------
if (cs_isIn(vint, 1)) <----- if (cs_isIn(vint, 0))
array[n++] = 0;

魔方陣を制約論理プログラム iZ-Cを使って技巧的に解きます。

魔方陣を制約論理プログラム iZ-Cを使って技巧的に解きます。
-----------------------------------------------------------------------------
make && ./magicsqure_simp 4 |less
Sun Aug 23 07:03:24 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
..........................
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.078023 s
Sun Aug 23 07:03:45 2020
---------------------------------------------------------------------------------
/**************************************************************************
* 魔方陣
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, LIM_MAIN;
/**************************************************************************/
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(allvars[i]);
printf("%3d", val);
if*1;
DIM = atoi(argv[1]); LIM_MAIN = DIM*(DIM*DIM-1)/2;

CSint **CELL = (CSint **)malloc(DIM*DIM * sizeof(CSint *));

CSint ***RC_CELL = (CSint ***)malloc(DIM * sizeof(CSint **));
CSint ***CR_CELL = (CSint ***)malloc(DIM * sizeof(CSint **));
for(i = 0; i < DIM; i++){
RC_CELL[i] = (CSint **)malloc(DIM * sizeof(CSint *));
CR_CELL[i] = (CSint **)malloc(DIM * sizeof(CSint *));
}

CSint ***dRL = (CSint ***)malloc(2 * sizeof(CSint **));
for(i = 0; i < 2; i++){
dRL[i] = (CSint **)malloc(DIM * sizeof(CSint *));
}

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

for(i = 0; i < DIM; i++){
cs_EQ(cs_Sigma(RC_CELL[i], DIM), LIM_MAIN);
cs_EQ(cs_Sigma(CR_CELL[i], DIM), LIM_MAIN);
}

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

for(i = 0; i < 2; i++){
cs_EQ(cs_Sigma(dRL[i], DIM), LIM_MAIN);
}

cs_Lt(RC_CELL[0][0], RC_CELL[0][DIM-1]);
cs_Lt(RC_CELL[0][DIM-1], RC_CELL[DIM-1][0]);
cs_Lt(RC_CELL[0][0], RC_CELL[DIM-1][DIM-1]);

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

printf("\033[2J\033[0;0f"); /* clear screen */
cs_findAll(&CELL[0], DIM*DIM, cs_findFreeVarNbConstraints, printSolution);
// cs_findAll(&CELL[0], DIM*DIM, 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;
clock_t t0 = clock();
time_t nowtime;

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

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

覆面算を制約論理プログラム iZ-Cを使って解きます。
-------------------------------------------------------------------------------------
iZ-Cチュートリアルにある覆面算を短く改編しました。積和演算cs_ScalProdで自動変数が
無効になることに気づかず時間がかかりました。
./mult
-------------------- ./mult --------------------
Solution 1
179
* 224
-----
716
358
358
-----
40096
-------------------------------------------------------------------------------------
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include "iz.h"

/****************************************************************************/
#define NB_DIGITS 20
CSint **Digit;
CSint *L1, *L2, *L3, *L4, *L5, *L6;

CSint *L[7];
/****************************************************************************/
void constraints()
{
/* 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19, */
enum {a = 0, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t};
static int ORDER[3] = {100, 10, 1};
static int ORDER5[5] = {10000, 1000, 100, 10, 1};
static int REV_ORDER[3] = {1, 10, 100};
/***********************/
/* A B C (L1) */
/* * D E F (L2) */
/* --------- */
/* G H I (L3) */
/* J K L (L4) */
/* M N O (L5) */
/* ---------- */
/* P Q R S T (L6) */
/***********************/

int val, ii;

Digit = cs_createCSintArray(NB_DIGITS, 0, 9);
/*
L1 = cs_ScalProd(&Digit[a], &ORDER[0], 3);
L2 = cs_ScalProd(&Digit[d], &ORDER[0], 3);
L3 = cs_ScalProd(&Digit[g], &ORDER[0], 3);
L4 = cs_ScalProd(&Digit[j], &ORDER[0], 3);
L5 = cs_ScalProd(&Digit[m], &ORDER[0], 3);
L6 = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);
*/
for(ii = 0; ii < 6; ii++){
L[ii + 1] = cs_ScalProd(&Digit[3 * ii], &ORDER[0], 3);
}
// L[6] = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);
L[6] = cs_ScalProd(&Digit[p], &ORDER5[0], 5);
//exit(1);

/*
cs_Eq(L6, cs_Mul(L1, L2));
cs_Eq(L3, cs_Mul(Digit[f], L1));
cs_Eq(L4, cs_Mul(Digit[e], L1));
cs_Eq(L5, cs_Mul(Digit[d], L1));
cs_Eq(L6, cs_VScalProd(3, L5, L4, L3, 100, 10, 1));
*/
cs_Eq(L[6], cs_Mul(L[1], L[2]));
cs_Eq(L[3], cs_Mul(Digit[f], L[1]));
cs_Eq(L[4], cs_Mul(Digit[e], L[1]));
cs_Eq(L[5], cs_Mul(Digit[d], L[1]));
// cs_Eq(L[6], cs_VScalProd(3, L[5], L[4], L[3], 100, 10, 1));
cs_Eq(L[6], cs_ScalProd(&L[3], &REV_ORDER[0], 3));

/* cs_Eq(L6, cs_Mul(L1, L2));*/

/*
cs_NEQ(Digit[a], 0);
cs_NEQ(Digit[d], 0);
cs_NEQ(Digit[g], 0);
cs_NEQ(Digit[j], 0);
cs_NEQ(Digit[m], 0);
cs_NEQ(Digit[p], 0);
*/
for(ii = 0; ii < 6; ii++){
cs_NEQ(Digit[3 * ii], 0);
}

for (val = 0; val <= 9 ; val++){
cs_OccurConstraints(CSINT(2), val, Digit, NB_DIGITS);
}
}


/****************************************************************************/
void constraints1()
{
enum {a = 0, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t};
/***********************/
/* A B C (L1) */
/* * D E F (L2) */
/* --------- */
/* G H I (L3) */
/* J K L (L4) */
/* M N O (L5) */
/* ---------- */
/* P Q R S T (L6) */
/***********************/

int val;

Digit = cs_createCSintArray(NB_DIGITS, 0, 9);
L1 = cs_VScalProd(3, Digit[a], Digit[b], Digit[c], 100, 10, 1);
L2 = cs_VScalProd(3, Digit[d], Digit[e], Digit[f], 100, 10, 1);
L3 = cs_VScalProd(3, Digit[g], Digit[h], Digit[i], 100, 10, 1);
L4 = cs_VScalProd(3, Digit[j], Digit[k], Digit[l], 100, 10, 1);
L5 = cs_VScalProd(3, Digit[m], Digit[n], Digit[o], 100, 10, 1);
L6 = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);

cs_Eq(L6, cs_Mul(L1, L2));

cs_Eq(L3, cs_Mul(Digit[f], L1));
cs_Eq(L4, cs_Mul(Digit[e], L1));
cs_Eq(L5, cs_Mul(Digit[d], L1));
cs_Eq(L6, cs_VScalProd(3, L5, L4, L3, 100, 10, 1));
/* cs_Eq(L6, cs_Mul(L1, L2));*/

cs_NEQ(Digit[a], 0);
cs_NEQ(Digit[d], 0);
cs_NEQ(Digit[g], 0);
cs_NEQ(Digit[j], 0);
cs_NEQ(Digit[m], 0);
cs_NEQ(Digit[p], 0);

for (val = 0; val <= 9 ; val++)
cs_OccurConstraints(CSINT(2), val, Digit, NB_DIGITS);
}

/****************************************************************************/
void printSolution(CSint **allvars, int nbVars)
{
static int NbSolutions = 0;
printf("Solution %4d\n", ++NbSolutions);

cs_printf(" %D\n", L[1]);
cs_printf("* %D\n", L[2]);
cs_printf("-----\n");
cs_printf(" %D\n", L[3]);
cs_printf(" %D \n", L[4]);
cs_printf("%D \n", L[5]);
cs_printf("-----\n");
cs_printf("%D \n", L[6]);
}

/****************************************************************************/
/****************************************************************************/
int main(int argc, char **argv)
{
clock_t t0 = clock();

printf("\n-------------------- %s --------------------\n", argv[0]);
cs_init();

constraints();
//constraints1();
cs_findAll(Digit, NB_DIGITS, cs_findFreeVarNbElements, printSolution);
// cs_search(Digit, NB_DIGITS, cs_findFreeVarNbElements);
// printSolution(Digit, NB_DIGITS);

cs_printStats();
cs_end();
printf("Elapsed Time = %fs\n", (double) (clock() - t0) / CLOCKS_PER_SEC);

return 0;
}

 

論理的関係制約を制約論理プログラム iZ-Cを使って表現します。

論理的関係制約を制約論理プログラム iZ-Cを使って表現します。
-------------------------------------------------------------------------------------
制約変数xiが{1,0}である場合、論理関数は次のように制約を設定することができます。

 

NOT                  cs_EQ(cs_ReifEQ(x1, 0), 1);

 

AND                  cs_EQ(cs_Add(3, x1, x2, x3), 3);

 

OR                    cs_NEQ(cs_Add(3, x1, x2, x3), 0);

 

EXOR                y1 = cs_ReifEQ(cs_Add(3, x1, x2, x3), 1);
                          y2 = cs_ReifEQ(cs_Add(3, x1, x2, x3), 3);
                          cs_NEQ(cs_Add(y1, y2), 0);

 

全称記号∀          cs_EQ(cs_Add(3, x1, x2, x3), 3);

 

存在記号∃          cs_NEQ(cs_Add(3, x1, x2, x3), 0);

 

整数の集合をほぼ等しく制約論理プログラム iZ-Cを使って分割します。

整数の集合をほぼ等しく制約論理プログラム iZ-Cを使って分割します。

-------------------------------------------------------------------------------------
make && time ./int_div 3 $(primes 1 53)
make: 'all' に対して行うべき事はありません.
15 3
Fri Aug 7 10:21:57 2020
QR:{0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}

Solution 1
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
0: 328 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1
1: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0
2: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

Solution 2
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1
0: 281 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0
1: 47 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1
2: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

Solution 3
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1
0: 238 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0
1: 90 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1
2: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

Solution 4
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1
0: 197 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0
1: 131 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1
2: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

Solution 5
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1
0: 160 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0
1: 168 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1
2: 0 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0

Solution 6
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 2
0: 160 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0
1: 121 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0
2: 47 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1

Solution 7
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2
0: 129 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0
1: 152 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 0
2: 47 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1

Solution 8
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 2, 2
0: 129 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0
1: 109 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0
2: 90 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1

Solution 9
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2
0: 100 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0
1: 138 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 0, 0
2: 90 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1

Solution 10
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 2, 2, 2
0: 100 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0
1: 97 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0, 0
2: 131 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1

Solution 11
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 2, 1, 2, 2
0: 100 : 1, 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 0, 0
1: 101 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0, 1, 0, 0
2: 127 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1

Solution 12
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 2, 2, 2, 1
0: 106 : 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0
1: 101 : 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 0, 0, 1
2: 121 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0

Solution 13
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 2, 1, 2, 1, 2
0: 106 : 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0
1: 103 : 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 1, 0
2: 119 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 1

Solution 14
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 2, 1, 2, 2, 1
0: 106 : 1, 1, 1, 1, 1, 1, 1, 1, 0, 1, 0, 0, 0, 0, 0
1: 107 : 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1
2: 115 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 0

Solution 15
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0, 1, 2, 2, 1
0: 108 : 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 0
1: 107 : 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 0, 0, 1
2: 113 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0

Solution 16
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 0, 1, 2, 0, 2, 1, 2, 1
0: 108 : 1, 1, 1, 1, 1, 1, 1, 1, 0, 0, 1, 0, 0, 0, 0
1: 111 : 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 1, 0, 1
2: 109 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0, 1, 0, 1, 0

Solution 17
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 2, 2, 2, 1, 1
0: 110 : 1, 1, 1, 1, 1, 1, 1, 0, 1, 1, 0, 0, 0, 0, 0
1: 109 : 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 1
2: 109 : 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 0, 0

Solution 18
2 3 5 7 11 13 17 19 23 29 31 37 41 43 47
0, 0, 0, 0, 0, 0, 1, 2, 1, 1, 0, 0, 1, 2, 2
0: 109 : 1, 1, 1, 1, 1, 1, 0, 0, 0, 0, 1, 1, 0, 0, 0
1: 110 : 0, 0, 0, 0, 0, 0, 1, 0, 1, 1, 0, 0, 1, 0, 0
2: 109 : 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 1, 1

Nb Fails = 1913206
Nb Choice Points = 2870015
Heap Size = 1024
Elapsed Time = 3.10079 s
Fri Aug 7 10:22:00 2020

real 0m3.107s
user 0m3.099s
sys 0m0.003s

-------------------------------------------------------------------------------------
/**************************************************************************
* 整数の集合をほぼ等しく分割
*
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

int DIV, DIM, *NUM;
CSint **QR, **NUM_DAT;
CSint **SUM;
/**************************************************************************/
/**************************************************************************/
void cost_printSolution(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;
int i;

printf("\nSolution %d\n\t", ++NbSolutions);
for(i = 0; i < DIM; i++){
printf("%4d", NUM[i]);
}
putchar('\n');
cs_printf("\t\t%A\n", &QR[0], DIM);
for(i = 0; i < DIV; i++){
printf("%4d", i);
cs_printf(":\t%D", SUM[i]);
cs_printf("\t: %A\n", &NUM_DAT[DIM * i], DIM);
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i, j;
CSint *cost;
clock_t t0 = clock();
time_t nowtime;

DIM = argc - 2;
DIV = atoi(argv[1]);
printf("%4d %4d\n", DIM, DIV);
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));

SUM = (CSint **)malloc(DIV * sizeof(CSint *));
CSint **SUM_delt = (CSint **)malloc(DIV * sizeof(CSint *));
NUM = (int *)malloc(DIM * sizeof(int ));
NUM_DAT = (CSint **)malloc(DIV * DIM * sizeof(CSint *));
for(i = 0; i < DIM; i++){
NUM[i] = atoi(argv[i + 2]);
//printf("%4d %4d\n", i, NUM[i]);
}

QR = cs_createCSintArray(DIM, 0, DIV - 1);

for(i = 0; i < DIV; i++){
for(j = 0; j < DIM; j++){
NUM_DAT[DIM * i + j] = cs_ReifEQ(QR[j], i);
}
}
for(i = 0; i < DIV; i++){
SUM[i] = cs_ScalProd(&NUM_DAT[DIM * i], &NUM[0], DIM);
}
for(i = 0; i < DIV; i++){
SUM_delt[i] = cs_Abs(cs_Sub(SUM[i], SUM[0]));
}

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

cost = cs_Sigma(SUM_delt, DIV);

cs_minimize(&QR[0], DIM, cs_findFreeVar, cost, cost_printSolution);
//// cs_findAll(&QR[0], NUM, cs_findFreeVarNbConstraints, printSolution);
// cs_findAll(&QR[0], DIM*DIM * STP, cs_findFreeVarNbElementsMin, printSolution);
//cs_findAll(&QR[0], DIM*DIM * STP, cs_findFreeVarNbElements, printSolution);
//cs_findAll(&QR[0], DIM*DIM * 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;
}