sunasunaxの日記

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

最小手数で家族とじっちゃんの川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で家族とじっちゃんの川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
aa=28; make && ./river_family_p $aa
make: 'all' に対して行うべき事はありません.
Mon Jan 18 08:00:08 2021
QR: 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}
QR_PD: 0, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}, {1..2047}

Step 24, Solution 1
boart=0, dog=1, maid=2, grandpa=3, father=4, mother=5, son=6_7, daughter=8_9, baby=10
0: 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 [b,d,m,P,f,M,S,s,G,g,B] [ , , , , , , , , , , ]
1: 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0 [ , , ,P,f,M,S,s,G,g,B] [b,d,m, , , , , , , , ]
2: 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0 [b, ,m,P,f,M,S,s,G,g,B] [ ,d, , , , , , , , , ]
3: 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0 [ , , ,P,f,M,S,s,G, ,B] [b,d,m, , , , , , ,g, ]
4: 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0 [b,d,m,P,f,M,S,s,G, ,B] [ , , , , , , , , ,g, ]
5: 1, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0 [ ,d,m,P,f, ,S,s, , ,B] [b, , , , ,M, , ,G,g, ]
6: 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0 [b,d,m,P,f,M,S,s, , ,B] [ , , , , , , , ,G,g, ]
7: 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0 [ ,d,m, ,f, ,S,s, , ,B] [b, , ,P, ,M, , ,G,g, ]
8: 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0 [b,d,m,P,f, ,S,s, , ,B] [ , , , , ,M, , ,G,g, ]
9: 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 1 [ ,d,m, ,f, ,S,s, , , ] [b, , ,P, ,M, , ,G,g,B]
10: 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1 [b,d,m,P,f, ,S,s, , , ] [ , , , , ,M, , ,G,g,B]
11: 1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1 [ ,d,m, , , ,S,s, , , ] [b, , ,P,f,M, , ,G,g,B]
12: 0, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0 [b,d,m, ,f, ,S,s, , ,B] [ , , ,P, ,M, , ,G,g, ]
13: 1, 1, 1, 1, 0, 1, 0, 0, 1, 1, 0 [ , , , ,f, ,S,s, , ,B] [b,d,m,P, ,M, , ,G,g, ]
14: 0, 1, 1, 0, 0, 1, 0, 0, 1, 1, 0 [b, , ,P,f, ,S,s, , ,B] [ ,d,m, , ,M, , ,G,g, ]
15: 1, 1, 1, 1, 0, 1, 0, 0, 1, 1, 1 [ , , , ,f, ,S,s, , , ] [b,d,m,P, ,M, , ,G,g,B]
16: 0, 1, 1, 0, 0, 1, 0, 0, 1, 1, 1 [b, , ,P,f, ,S,s, , , ] [ ,d,m, , ,M, , ,G,g,B]
17: 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1 [ , , , , , ,S,s, , , ] [b,d,m,P,f,M, , ,G,g,B]
18: 0, 1, 1, 1, 0, 1, 0, 0, 1, 1, 1 [b, , , ,f, ,S,s, , , ] [ ,d,m,P, ,M, , ,G,g,B]
19: 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1 [ , , , , , ,S, , , , ] [b,d,m,P,f,M, ,s,G,g,B]
20: 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1 [b,d,m, , , ,S, , , , ] [ , , ,P,f,M, ,s,G,g,B]
21: 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1 [ ,d, , , , , , , , , ] [b, ,m,P,f,M,S,s,G,g,B]
22: 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1 [b,d,m, , , , , , , , ] [ , , ,P,f,M,S,s,G,g,B]
23: 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 [ , , , , , , , , , , ] [b,d,m,P,f,M,S,s,G,g,B]

Step 22, Solution 2
boart=0, dog=1, maid=2, grandpa=3, father=4, mother=5, son=6_7, daughter=8_9, baby=10
0: 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0 [b,d,m,P,f,M,S,s,G,g,B] [ , , , , , , , , , , ]
1: 1, 1, 1, 0, 0, 0, 0, 0, 0, 0, 0 [ , , ,P,f,M,S,s,G,g,B] [b,d,m, , , , , , , , ]
2: 0, 1, 0, 0, 0, 0, 0, 0, 0, 0, 0 [b, ,m,P,f,M,S,s,G,g,B] [ ,d, , , , , , , , , ]
3: 1, 1, 1, 0, 0, 0, 0, 0, 0, 1, 0 [ , , ,P,f,M,S,s,G, ,B] [b,d,m, , , , , , ,g, ]
4: 0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0 [b,d,m,P,f,M,S,s,G, ,B] [ , , , , , , , , ,g, ]
5: 1, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0 [ ,d,m,P,f, ,S,s, , ,B] [b, , , , ,M, , ,G,g, ]
6: 0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0 [b,d,m,P,f,M,S,s, , ,B] [ , , , , , , , ,G,g, ]
7: 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 0 [ ,d,m, ,f, ,S,s, , ,B] [b, , ,P, ,M, , ,G,g, ]
8: 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 0 [b,d,m,P,f, ,S,s, , ,B] [ , , , , ,M, , ,G,g, ]
9: 1, 0, 0, 1, 0, 1, 0, 0, 1, 1, 1 [ ,d,m, ,f, ,S,s, , , ] [b, , ,P, ,M, , ,G,g,B]
10: 0, 0, 0, 0, 0, 1, 0, 0, 1, 1, 1 [b,d,m,P,f, ,S,s, , , ] [ , , , , ,M, , ,G,g,B]
11: 1, 0, 0, 1, 1, 1, 0, 0, 1, 1, 1 [ ,d,m, , , ,S,s, , , ] [b, , ,P,f,M, , ,G,g,B]
12: 0, 0, 0, 1, 0, 1, 0, 0, 1, 1, 1 [b,d,m, ,f, ,S,s, , , ] [ , , ,P, ,M, , ,G,g,B]
13: 1, 1, 1, 1, 0, 1, 0, 0, 1, 1, 1 [ , , , ,f, ,S,s, , , ] [b,d,m,P, ,M, , ,G,g,B]
14: 0, 1, 1, 0, 0, 1, 0, 0, 1, 1, 1 [b, , ,P,f, ,S,s, , , ] [ ,d,m, , ,M, , ,G,g,B]
15: 1, 1, 1, 1, 1, 1, 0, 0, 1, 1, 1 [ , , , , , ,S,s, , , ] [b,d,m,P,f,M, , ,G,g,B]
16: 0, 1, 1, 1, 0, 1, 0, 0, 1, 1, 1 [b, , , ,f, ,S,s, , , ] [ ,d,m,P, ,M, , ,G,g,B]
17: 1, 1, 1, 1, 1, 1, 0, 1, 1, 1, 1 [ , , , , , ,S, , , , ] [b,d,m,P,f,M, ,s,G,g,B]
18: 0, 0, 0, 1, 1, 1, 0, 1, 1, 1, 1 [b,d,m, , , ,S, , , , ] [ , , ,P,f,M, ,s,G,g,B]
19: 1, 0, 1, 1, 1, 1, 1, 1, 1, 1, 1 [ ,d, , , , , , , , , ] [b, ,m,P,f,M,S,s,G,g,B]
20: 0, 0, 0, 1, 1, 1, 1, 1, 1, 1, 1 [b,d,m, , , , , , , , ] [ , , ,P,f,M,S,s,G,g,B]
21: 1, 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 [ , , , , , , , , , , ] [b,d,m,P,f,M,S,s,G,g,B]

Nb Fails = 2083
Nb Choice Points = 4223
Heap Size = 30720
Elapsed Time = 0.099972 s
Mon Jan 18 08:00:08 2021
---------------------------------------------------------------------------
/**************************************************************************
* ある家族がいて、舟を使って川を向こう岸へ渡ろうとしています。
* この家族は父、母、息子1、息子2、娘1、娘2、メイド、犬、じっちゃん、
* 赤ん坊の10人家族(犬も1人と数えます)です。
* 舟は1艘(そう)しかなく、1度に2人まで乗ることができます。
* また、この舟をこげるのは父と母とメイドとじっちゃんの4人です。
*
* そしてこの家族、実はとっても危ない家族なんです。
* 父は、母がいなくなると娘を殺してしまいます。
* 母は、父がいなくなると息子を殺してしまいます。
* じっちゃんは、親がいないと息子や娘、赤ん坊を殺してしまいます。
* 息子や娘は、親がいないと赤ん坊を殺してしまいます。
* そしてきわめつけ。
* 犬は、メイドがいないと家族をみんな殺してしまいます。
*
* それでは問題です。
* みんなが無事に川を渡り切るには、どのような手順で渡ればよいでしょうか?
* http://quiz-tairiku.com/logic/q10.html
****************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, MAX_STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
enum {boart, dog, maid, grandpa, father, mother, son1, son2, daughter1, daughter2, baby};
/**************************************************************************/
/**************************************************************************/
void imp(CSint *cond, CSint *exe){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe), 0);
}
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
imp(cs_ReifEQ(cond, 1), exe1);
imp(cs_ReifEQ(cond, 0), exe2);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;
int END = (long int)(int *)extra;

if(val == END){
for(i = index + 1; i < size; i++){
if(!cs_EQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
CSint **curr_pos_diff(int num, CSint **array, int src, int target){
int k;
CSint **ret_array = (CSint **)malloc(num * sizeof(CSint *));
for(k = 0; k < num; k++) ret_array[k] = cs_ReifEq(array[src], array[target + k]);
return ret_array;
}
/**************************************************************************/
/**************************************************************************/
void print_sub(int selct, int chk_num){
//enum {boart, dog, maid, father, mother, son1, son2, daughter1, daughter2};
char alph[11] ={"bdmPfMSsGgB"};
int j;

for(j = 0; j < DIM; j++) printf("%c%c",
cs_getValue(QR[DIM * selct + j]) == chk_num ? alph[j] : ' ', j < DIM-1 ? ',':']');
}
/**************************************************************************/
/**************************************************************************/
void printSolution1(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cs_Index(&QR_PD[0], MAX_STP, QR_PD_END));

printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
// enum {boart, dog, maid, grandpa, father, mother, son1, son2, daughter1, daughter2, baby};
printf("boart=0, dog=1, maid=2, grandpa=3, father=4, mother=5, son=6_7, daughter=8_9, baby=10\n");
for(i = 0; i < step; i++){
printf("%3d: ", i);
cs_printf("%A ", &QR[DIM * i], DIM);
putchar('['); print_sub(i, 0);
printf(" ["); print_sub(i, 1);
printf("\n");
}
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;

printf("\nStep %d, Solution %d\n", nbVars / DIM, ++NbSolutions);
// enum {boart, dog, maid, grandpa, father, mother, son1, son2, daughter1, daughter2, baby};
printf("boart=0, dog=1, maid=2, grandpa=3, father=4, mother=5, son=6_7, daughter=8_9, baby=10\n");
for(i = 0; i < nbVars / DIM; i++){
printf("%3d: ", i);
cs_printf("%A ", &QR[DIM * i], DIM);
putchar('['); print_sub(i, 0);
printf(" ["); print_sub(i, 1);
printf("\n");
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;
DIM = 11;
QR_PD_END = (1 << DIM) - 1;
int *order =(int *)malloc(DIM * sizeof(int));
for(i = 0; i < DIM; i++) order[i] = 1 << i;

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

QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
for(i = 0; i < DIM * MAX_STP; i++){
QR[i] = cs_createCSint(0, 1);
}
cs_EQ(cs_Sigma(&QR[0], DIM), 0);

QR_PD = (CSint **)malloc(MAX_STP * sizeof(CSint *));

for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM * i], &order[0], DIM);
}

//enum {boart, dog, maid, grandpa, father, mother, son1, son2, daughter1, daughter2, baby};
for(i = 1; i < MAX_STP; i++){
CSint **curr_pos = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **prev_pos = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **mv = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **chg = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
curr_pos[j] = QR[DIM * i + j];
prev_pos[j] = QR[DIM * (i - 1) + j];

mv[j] = cs_Sub(curr_pos[j], prev_pos[j]);
chg[j] = cs_ReifNEQ(mv[j], 0);
}

cond_imp(cs_ReifEQ(QR_PD[i - 1], QR_PD_END), cs_ReifEQ(mv[boart], 0), cs_ReifNEQ(mv[boart], 0));
cs_LE(cs_Sigma(&chg[dog], DIM - 1), 2);
for(int j = 1; j < DIM; j++){
CSint *mv_0 = cs_ReifEQ(mv[boart + j], 0);
for(int k = -1; k <= 1; k++){
imp(cs_ReifEQ(mv[boart], k), cs_ReifNEQ(cs_Add(cs_ReifEQ(mv[boart + j], k), mv_0), 0));
}
}

//enum {boart, dog, maid, grandpa, father, mother, son1, son2, daughter1, daughter2, baby};
CSint **mv_eq_boart = curr_pos_diff(4, &mv[0], boart, maid);
imp(cs_ReifNEQ(mv[boart], 0), cs_ReifNEQ(cs_Sigma(&mv_eq_boart[0], 4), 0));

CSint *curr_pos_diff_fath_moth = cs_ReifNeq(curr_pos[father], curr_pos[mother]);
CSint **curr_pos_diff_moth_son = curr_pos_diff(2, &curr_pos[0], mother, son1);
CSint **curr_pos_diff_fath_dau = curr_pos_diff(2, &curr_pos[0], father, daughter1);
imp(curr_pos_diff_fath_moth, cs_ReifEQ(cs_Sigma(&curr_pos_diff_moth_son[0], 2), 0));
imp(curr_pos_diff_fath_moth, cs_ReifEQ(cs_Sigma(&curr_pos_diff_fath_dau[0], 2), 0));

CSint **curr_pos_diff_dog_family = curr_pos_diff(8, &curr_pos[0], dog, grandpa);
imp(cs_ReifNeq(curr_pos[dog], curr_pos[maid]),
cs_ReifEQ(cs_Sigma(&curr_pos_diff_dog_family[0], 8), 0));

/******************************************************************************/
CSint **curr_pos_diff_baby_parent = curr_pos_diff(2, &curr_pos[0], baby, father);
CSint **curr_pos_diff_baby_children = curr_pos_diff(4, &curr_pos[0], baby, son1);
imp(cs_ReifEQ(cs_Sigma(&curr_pos_diff_baby_parent[0], 2), 0),
cs_ReifEQ(cs_Sigma(&curr_pos_diff_baby_children[0], 4), 0));

CSint **curr_pos_diff_grandpa_parent = curr_pos_diff(2, &curr_pos[0], grandpa, father);
CSint **curr_pos_diff_grandpa_children = curr_pos_diff(5, &curr_pos[0], grandpa, son1);
imp(cs_ReifEQ(cs_Sigma(&curr_pos_diff_grandpa_parent[0], 2), 0),
cs_ReifEQ(cs_Sigma(&curr_pos_diff_grandpa_children[0], 5), 0));
}
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, (void *)(long)QR_PD_END);

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

CSint *cost = cs_Index(&QR_PD[0], MAX_STP, QR_PD_END);

// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVar, printSolution);
// cs_findAll(&QR[0], DIM * MAX_STP, cs_findFreeVarNbConstraints, printSolution);
cs_minimize(&QR[0], DIM * MAX_STP, cs_findFreeVar, cost, printSolution1);
// cs_minimize(&QR[0], DIM * MAX_STP, cs_findFreeVarNbConstraints, cost, printSolution1);

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;
}