sunasunaxの日記

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

整数の集合をほぼ等しく制約論理プログラム 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;
}