sunasunaxの日記

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

値1のビットのグループ分けをiZ-Cを使って行います

値1のビットのグループ分けをiZ-Cを使って行います。
-----------------------------------------------------------------------------
make && ./bit_group 10 3

Wed Oct 7 15:32:12 2020

Solution 1
0, 0, 0, 0, 0, 1, 0, 1, 0, 1

Solution 2
0, 0, 0, 0, 1, 0, 0, 1, 0, 1
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Solution 461
1, 1, 1, 1, 1, 0, 1, 1, 0, 1

Solution 462
1, 1, 1, 1, 1, 1, 0, 1, 0, 1

Nb Fails = 29
Nb Choice Points = 980
Heap Size = 1024
Elapsed Time = 0.000824 s
Wed Oct 7 15:32:12 2020
-----------------------------------------------------------------------------
/**************************************************************************
* 1のビットをグループに分ける
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;

printf("\nSolution %d\n", ++NbSolutions);
cs_printf("%A\n", &allvars[0], nbVars);
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int DIM, GRP;
CSint **QR;
int i;
clock_t t0 = clock();
time_t nowtime;

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

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

QR = cs_createCSintArray(DIM, 0, 1);
EDGE[0] = cs_ReifEQ(QR[0], 1);
for(i = 1; i < DIM; i++){
EDGE[i] = cs_ReifEQ(cs_Add(cs_ReifEQ(QR[i - 1], 0), cs_ReifEQ(QR[i], 1)), 2);
}
cs_OccurConstraints(CSINT(GRP), 1, EDGE, DIM);

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