2020-12-22

最小手数で夫婦３組の川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で夫婦３組の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_marrige 17
make: 'all' に対して行うべき事はありません.
Tue Dec 22 21:16:32 2020
QR: 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}
QR_PD: 0, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}, {1..127}

Step 16, Solution 1
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 0, 0, 1, 0, 1 [ ,A,a,B, ,C, ] [S, , , ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 0 [S,A,a,B, ,C,c] [ , , , ,b, , ]
5: 1, 0, 1, 0, 1, 0, 0 [ ,A, ,B, ,C,c] [S, ,a, ,b, , ]
6: 0, 0, 1, 0, 0, 0, 0 [S,A, ,B,b,C,c] [ , ,a, , , , ]
7: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
8: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
9: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
10: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
11: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
12: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
13: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
14: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
15: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]

Step 14, Solution 2
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 0, 0, 1, 0, 1 [ ,A,a,B, ,C, ] [S, , , ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 0 [S,A,a,B, ,C,c] [ , , , ,b, , ]
5: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
6: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
7: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
8: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
9: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
10: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
11: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
12: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
13: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]

Step 12, Solution 3
Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6
0: 0, 0, 0, 0, 0, 0, 0 [S,A,a,B,b,C,c] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,A,a,B,b, , ] [S, , , , ,C,c]
2: 0, 0, 0, 0, 0, 0, 1 [S,A,a,B,b,C, ] [ , , , , , ,c]
3: 1, 0, 1, 0, 1, 0, 1 [ ,A, ,B, ,C, ] [S, ,a, ,b, ,c]
4: 0, 0, 0, 0, 1, 0, 1 [S,A,a,B, ,C, ] [ , , , ,b, ,c]
5: 1, 0, 0, 1, 1, 1, 1 [ ,A,a, , , , ] [S, , ,B,b,C,c]
6: 0, 0, 0, 0, 0, 1, 1 [S,A,a,B,b, , ] [ , , , , ,C,c]
7: 1, 1, 0, 1, 0, 1, 1 [ , ,a, ,b, , ] [S,A, ,B, ,C,c]
8: 0, 1, 0, 1, 0, 1, 0 [S, ,a, ,b, ,c] [ ,A, ,B, ,C, ]
9: 1, 1, 0, 1, 1, 1, 1 [ , ,a, , , , ] [S,A, ,B,b,C,c]
10: 0, 0, 0, 1, 1, 1, 1 [S,A,a, , , , ] [ , , ,B,b,C,c]
11: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [S,A,a,B,b,C,c]

Nb Fails = 5406
Nb Choice Points = 10897
Heap Size = 7168
Elapsed Time = 0.046205 s
Tue Dec 22 21:16:32 2020
---------------------------------------------------------------------------
/**************************************************************************
* 夫婦３組の川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

//#include "sgn.c"

int DIM, MAX_STP, STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
enum {boart, A,a, B,b, C,c};
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe1), 0);
cs_NEQ(cs_Add(cs_ReifEQ(cond, 1), exe2), 0);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;

if(val == QR_PD_END) return TRUE;
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void print_sub(int selct, int chk_num){
char alph[7] ={"SAaBbCc"};
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);
printf("Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6\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);
printf("Ship = 0, A_cople = 1,2, B_cople= 3,4, C_cople = 5,6\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;

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

QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
QR_PD= (CSint **)malloc(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);
// cs_EQ(cs_Sigma(&QR[DIM * (MAX_STP -1)], DIM), DIM);

int order[7] ={1, 2, 4, 8, 16, 32, 64};
for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);

// CSint *pos_boart = QR[DIM*i+ boart];
CSint *pos_A = QR[DIM*i+ A];
CSint *pos_a = QR[DIM*i+ a];
CSint *pos_B = QR[DIM*i+ B];
CSint *pos_b = QR[DIM*i+ b];
CSint *pos_C = QR[DIM*i+ C];
CSint *pos_c = QR[DIM*i+ c];

cs_NEQ(cs_Add(cs_ReifEq(pos_A, pos_a), cs_ReifNeq(pos_a, pos_B)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_A, pos_a), cs_ReifNeq(pos_a, pos_C)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_B, pos_b), cs_ReifNeq(pos_b, pos_A)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_B, pos_b), cs_ReifNeq(pos_b, pos_C)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_C, pos_c), cs_ReifNeq(pos_c, pos_A)), 0);
cs_NEQ(cs_Add(cs_ReifEq(pos_C, pos_c), cs_ReifNeq(pos_c, pos_B)), 0);
}
for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(QR[DIM*i+ boart], QR[DIM*(i-1) + boart]);
CSint *mv_A = cs_Sub(QR[DIM*i+ A], QR[DIM*(i-1) + A]);
CSint *mv_a = cs_Sub(QR[DIM*i+ a], QR[DIM*(i-1) + a]);
CSint *mv_B = cs_Sub(QR[DIM*i+ B], QR[DIM*(i-1) + B]);
CSint *mv_b = cs_Sub(QR[DIM*i+ b], QR[DIM*(i-1) + b]);
CSint *mv_C = cs_Sub(QR[DIM*i+ C], QR[DIM*(i-1) + C]);
CSint *mv_c = cs_Sub(QR[DIM*i+ c], QR[DIM*(i-1) + c]);

CSint *sum_mv = cs_VAdd(6, cs_Abs(mv_A), cs_Abs(mv_a), cs_Abs(mv_B),
cs_Abs(mv_b), cs_Abs(mv_C), cs_Abs(mv_c));
CSint *mv_p_0 = cs_Sub(cs_OccurDomain(0, &QR[DIM*i+A], DIM-1),
cs_OccurDomain(0, &QR[DIM*(i-1)+A], DIM-1));
CSint *mv_p_1 = cs_Sub(cs_OccurDomain(1, &QR[DIM*i+A], DIM-1),
cs_OccurDomain(1, &QR[DIM*(i-1)+A], DIM-1));

cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(QR_PD[i-1], QR_PD_END), cs_ReifNEQ(cs_Abs(mv_boart), 0)), 0);

cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(QR_PD[i], QR_PD_END)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(mv_boart, 0)), 0);
cs_LE(sum_mv, 2);
cs_NEQ(cs_Add(cs_ReifNEQ(sum_mv, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(sum_mv, 0), cs_ReifNEQ(mv_boart, 0)), 0);
/*
cs_Eq(mv_boart, Sgn(mv_p_1));
cs_Eq(mv_boart, cs_Sub(CSINT(0), Sgn(mv_p_0)));
*/
cs_NEQ(cs_Add(cs_ReifLE(mv_p_1, 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(mv_p_1, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(mv_p_1, 0), cs_ReifEQ(mv_boart, -1)), 0);

cs_NEQ(cs_Add(cs_ReifLE(mv_p_0, 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(mv_p_0, 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(mv_p_0, 0), cs_ReifEQ(mv_boart, 1)), 0);

}
//exit(1);

// cs_AllNeq(&QR_PD[0], MAX_STP);
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, NULL);

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_printStats();
printf("Elapsed Time = %g s\n", (double) (clock() - t0) / CLOCKS_PER_SEC);
time(&nowtime); printf("%s", ctime(&nowtime));
cs_end();
return EXIT_SUCCESS;
}

2020-12-20

最小手数で宣教師と人食いの川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で宣教師と人食いの川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_missio_num 14
gcc -Wall -O3 -I. -L. -o river_missio_num river_missio_num.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Sun Dec 20 10:58:17 2020
QR: 0, 3, 3, 0, 0, 1, {1..3}, {1..3}, {0..2}, {0..2}, 0, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..3}, {0..3}, {0..3}, {0..3}, {0, 1}, {0..2}, {0..2}, {1..3}, {1..3}, 1, 0, 0, 3, 3
QR_PD: 60, {21..59, 61..701}, {0..59, 61..1020}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {0..59, 61..1021}, {320..1001}, 961

Step 12, Solution 1
boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4
0: 0, 3, 3, 0, 0
1: 1, 2, 2, 1, 1
2: 0, 3, 2, 0, 1
3: 1, 3, 0, 0, 3
4: 0, 3, 1, 0, 2
5: 1, 1, 1, 2, 2
6: 0, 2, 2, 1, 1
7: 1, 0, 2, 3, 1
8: 0, 0, 3, 3, 0
9: 1, 0, 1, 3, 2
10: 0, 0, 2, 3, 1
11: 1, 0, 0, 3, 3

Nb Fails = 44
Nb Choice Points = 79
Heap Size = 4096
Elapsed Time = 0.001232 s
Sun Dec 20 10:58:17 2020
---------------------------------------------------------------------------
/**************************************************************************
* 宣教師と人食いの川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, MAX_STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
//int boart = 0, missionary = 1_3, deamon = 4_6;
enum {boart=0, missionary0, deamon0, missionary1, deamon1};
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe1), 0);
cs_NEQ(cs_Add(cs_ReifEQ(cond, 1), exe2), 0);
}
/**************************************************************************/
/**************************************************************************/
CSint *is_GE_LE(CSint *Val, int n1, int n2){
CSint *a1 = cs_ReifGE(Val, n1);
CSint *a2 = cs_ReifLE(Val, n2);

return cs_ReifEQ(cs_Add(a1, a2), 2);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;
//cs_printf("%A\n", allvars, MAX_STP);
if(val == QR_PD_END) return TRUE;
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void print_sub(int selct, int chk_num){
char alph[7] ={"bmmmddd"};
int j;

printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf("boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4\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);
printf("boart = 0, missionary0 = 1, deamon0 = 2, missionary1 = 3, deamon1 = 4\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 = 5;
int order[5] ={1};
for(i = 1; i < 5; i++) order[i] = order[i-1]*4;
QR_PD_END = 1 + 3*order[3] + 3*order[4];

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 < MAX_STP; i++){
QR[DIM*i + boart] = cs_createCSint(0, 1);
QR[DIM*i + missionary0] = cs_createCSint(0, 3);
QR[DIM*i + deamon0] = cs_createCSint(0, 3);
QR[DIM*i + missionary1] = cs_createCSint(0, 3);
QR[DIM*i + deamon1] = cs_createCSint(0, 3);
}
// cs_EQ(cs_Sigma(&QR[0], 3), 0);
// cs_EQ(cs_Sigma(&QR[DIM * (MAX_STP -1)], DIM), DIM);
cs_EQ(QR[DIM*0 + boart], 0);
cs_EQ(QR[DIM*0 + missionary0], 3);
cs_EQ(QR[DIM*0 + deamon0], 3);
cs_EQ(QR[DIM*0 + missionary1], 0);
cs_EQ(QR[DIM*0 + deamon1], 0);

//enum {boart, missionary0, deamon0, missionary1, deamon1};

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

for(i = 0; i < MAX_STP; i++){
QR_PD[i] = cs_ScalProd(&QR[DIM * i], &order[0], DIM);
boart_pos[i] = QR[DIM*i + boart];
cs_NEQ(cs_Add(cs_ReifEQ(QR[DIM*i + missionary0], 0),
cs_ReifGe(QR[DIM*i + missionary0], QR[DIM*i + deamon0])), 0);
cs_NEQ(cs_Add(cs_ReifEQ(QR[DIM*i + missionary1], 0),
cs_ReifGe(QR[DIM*i + missionary1], QR[DIM*i + deamon1])), 0);

cs_EQ(cs_Add(QR[DIM*i + missionary0], QR[DIM*i + missionary1]), 3);
cs_EQ(cs_Add(QR[DIM*i + deamon0], QR[DIM*i + deamon1]), 3);
}
cs_EQ(QR_PD[MAX_STP - 1], QR_PD_END);
//exit(1);

for(i = 1; i < MAX_STP; i++){
cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(QR_PD[i], QR_PD_END)), 0);
}

for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(boart_pos[i], boart_pos[i -1]);
//cs_printf("%D\n", mv_boart);

CSint *m0_inc = cs_Sub(QR[DIM*i + missionary0], QR[DIM*(i-1) + missionary0]);
CSint *m1_inc = cs_Sub(QR[DIM*i + missionary1], QR[DIM*(i-1) + missionary1]);
CSint *d0_inc = cs_Sub(QR[DIM*i + deamon0], QR[DIM*(i-1) + deamon0]);
CSint *d1_inc = cs_Sub(QR[DIM*i + deamon1], QR[DIM*(i-1) + deamon1]);

CSint *md0_inc = cs_Sub(cs_Sigma(&QR[DIM*i + missionary0], 2),
cs_Sigma(&QR[DIM*(i-1) + missionary0], 2));
CSint *md1_inc = cs_Sub(cs_Sigma(&QR[DIM*i + missionary1], 2),
cs_Sigma(&QR[DIM*(i-1) + missionary1], 2));

cs_NEQ(cs_Add(cs_ReifNEQ(QR_PD[i-1], QR_PD_END), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(QR_PD[i-1], QR_PD_END), cs_ReifNEQ(cs_Abs(mv_boart), 0)), 0);

cs_LE(cs_Abs(m0_inc), 2); cs_LE(cs_Abs(m1_inc), 2);
cs_LE(cs_Abs(d0_inc), 2); cs_LE(cs_Abs(d1_inc), 2);
cs_GE(cs_Mul*1, 0); cs_GE(cs_Mul*2, 0);

cs_EQ(cs_Add(md0_inc, md1_inc), 0); cs_LE(cs_Abs(md0_inc), 2); cs_LE(cs_Abs(md1_inc), 2);

cs_NEQ(cs_Add(cs_ReifLE(md1_inc , 0), cs_ReifEQ(mv_boart, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(md1_inc , 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(md1_inc , 0), cs_ReifEQ(mv_boart, -1)), 0);

cs_NEQ(cs_Add(cs_ReifLE(md0_inc , 0), cs_ReifEQ(mv_boart, -1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(md0_inc , 0), cs_ReifEQ(mv_boart, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(md0_inc , 0), cs_ReifEQ(mv_boart, 1)), 0);
}

// cs_AllNeq(&QR_PD[0], MAX_STP);
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, NULL);

cs_printf("QR: %A\n", QR, DIM * MAX_STP);
cs_printf("QR_PD: %A\n", QR_PD, MAX_STP);
// for(i = 0; i < MAX_STP; i++){ cs_printf("%A\n", &QR[DIM*i], DIM); }

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

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:m0_inc), (d0_inc

*2:m1_inc), (d1_inc

2020-12-09

最小手数で農夫山羊狼キャベツの川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で農夫山羊狼キャベツの川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river 10
make: 'all' に対して行うべき事はありません.
Wed Dec 9 06:27:19 2020
QR: 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}
QR_PD: 0, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}, {1..15}

Step 8, Solution 1
farmer = 0, goat = 1, wolf = 2, cabbage = 3
0: 0, 0, 0, 0 [f,g,w,c] [ , , , ]
1: 1, 1, 0, 0 [ , ,w,c] [f,g, , ]
2: 0, 1, 0, 0 [f, ,w,c] [ ,g, , ]
3: 1, 1, 0, 1 [ , ,w, ] [f,g, ,c]
4: 0, 0, 0, 1 [f,g,w, ] [ , , ,c]
5: 1, 0, 1, 1 [ ,g, , ] [f, ,w,c]
6: 0, 0, 1, 1 [f,g, , ] [ , ,w,c]
7: 1, 1, 1, 1 [ , , , ] [f,g,w,c]

Nb Fails = 30
Nb Choice Points = 65
Heap Size = 2048
Elapsed Time = 0.001843 s
Wed Dec 9 06:27:19 2020
---------------------------------------------------------------------------
/**************************************************************************
* 農夫山羊狼キャベツの川渡り
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, MAX_STP, STP;
int QR_PD_END;
CSint **QR;
CSint **QR_PD;
//int farmer = 0, goat = 1, wolf = 2, cabbage = 3;
enum {farmer, goat, wolf, cabbage};
/**************************************************************************/
/**************************************************************************/
void cond_imp(CSint *cond, CSint *exe1, CSint *exe2){
cs_NEQ(cs_Add(cs_ReifEQ(cond, 0), exe1), 0);
cs_NEQ(cs_Add(cs_ReifEQ(cond, 1), exe2), 0);
}
/**************************************************************************/
/**************************************************************************/
IZBOOL knownQR_PD(int val, int index, CSint **allvars, int size, void *extra) {
int i;

printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf("farmer = 0, goat = 1, wolf = 2, cabbage = 3\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);
printf("farmer = 0, goat = 1, wolf = 2, cabbage = 3\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;

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

QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
QR_PD= (CSint **)malloc(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);
// cs_EQ(cs_Sigma(&QR[DIM * (MAX_STP -1)], DIM), DIM);

for(i = 0; i < MAX_STP - 1; i++){
int j = DIM * i, jn = DIM * (i + 1);
cs_Le(cs_VAdd(3,
cs_ReifNeq(QR[j + goat], QR[jn + goat]),
cs_ReifNeq(QR[j + wolf], QR[jn + wolf]),
cs_ReifNeq(QR[j + cabbage], QR[jn + cabbage])),
cs_ReifNeq(QR[j + farmer], QR[jn + farmer]));
}
int order[4] ={1, 2, 4, 8};
for(i = 0; i < MAX_STP; i++){
int j = DIM * i;
// farmer = 0, goat = 1, wolf = 2, cabbage = 3;
CSint *j_fm = QR[j + farmer];
CSint *Add_w_g = cs_Add(QR[j + wolf], QR[j + goat]);
CSint *Add_g_c = cs_Add(QR[j + goat], QR[j + cabbage]);

cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 0), cs_ReifNEQ(Add_w_g, 2)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 1), cs_ReifNEQ(Add_w_g, 0)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 0), cs_ReifNEQ(Add_g_c, 2)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(j_fm, 1), cs_ReifNEQ(Add_g_c, 0)), 0);

QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);
}
for(i = 1; i < MAX_STP; i++){
cond_imp(cs_ReifEQ(QR_PD[i-1], QR_PD_END),
cs_ReifEQ(QR_PD[i], QR_PD_END), cs_ReifEq(QR_PD[i], QR_PD[i]));
}

// cs_AllNeq(&QR_PD[0], MAX_STP);
cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, NULL);

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_printStats();
printf("Elapsed Time = %g s\n", (double) (clock() - t0) / CLOCKS_PER_SEC);
time(&nowtime); printf("%s", ctime(&nowtime));
cs_end();
return EXIT_SUCCESS;
}

2020-11-19

格子道順ふかしぎお姉さんといっしょに数えてみよう。をiZ-Cで解きます。

格子道順ふかしぎお姉さんといっしょに数えてみよう。をiZ-Cで解きます。
------------------------------------------------------
aa=5; make && ./kohshi $aa $*1 1

Thu Nov 19 06:13:49 2020
QR:0, 0, {0, 1}, {0, 1}, {0..2}, {0..2}, {0..3}, {0..3}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}, {0..4}
ESC[2JESC[0;0fESC[0;0f
Step 25, Solution 1
0 9 10 19 20
1 8 11 18 21
2 7 12 17 22
3 6 13 16 23
4 5 14 15 24
ESC[0;0f
Step 23, Solution 2
0 9 10 . .
1 8 11 18 19
2 7 12 17 20
3 6 13 16 21
4 5 14 15 22
ESC[0;0f
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Step 11, Solution 8511
0 1 2 3 4
. . . . 5
. . . . 6
. . . 8 7
. . . 9 10
ESC[0;0f
Step 9, Solution 8512
0 1 2 3 4
. . . . 5
. . . . 6
. . . . 7
. . . . 8

Nb Fails = 48504
Nb Choice Points = 92280
Heap Size = 2048
Elapsed Time = 0.357649 s
Thu Nov 19 06:14:24 2020

/**************************************************************************
* 格子道順
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

int DIM, STP;
CSint **QR, **PQR;
int *Board;
int DISP;
int ws = 1;
/**************************************************************************/
/**************************************************************************/
IZBOOL knownPQR(int val, int index, CSint **allvars, int size, void *extra) {
int i;

if(val == DIM * DIM -1) return TRUE;
for(i = 0; i < STP; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cs_Index(&PQR[0], STP, DIM * DIM - 1));

if(DISP == 0) {
printf("\nStep %2d, Solution %6d\n", step, ++NbSolutions);
cs_printf("%A\n", &PQR[0], step);
}
else {
printf("\033[0;0f"); /* top cursol */
printf("\nStep %2d, Solution %6d\n", step, ++NbSolutions);
for(i = 0; i < DIM * DIM; i++) Board[i] = -1;
for(i = 0; i < step; i++){
Board[cs_getValue(PQR[i])] = i;
if(cs_getValue(PQR[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( *2;
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 *));
PQR = (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);
PQR[i] = cs_VScalProd(2, QR[2*i + 1], QR[2*i + 0], DIM, 1);
}

for (i = 1; i < STP; i++){
CSint *px = QR[2*(i-1) + 0], *py = QR[2*(i-1) + 1];
CSint *cx = QR[2*i + 0], *cy = QR[2*i + 1];
CSint *dx = cs_Sub(cx, px), *dy = cs_Sub(cy, py);

CSint *f_c = cs_ReifEQ(cs_Add(cs_Abs(dx), cs_Abs(dy)), 1);
CSint *f_p = cs_ReifEQ(PQR[i - 1], DIM*DIM - 1);
CSint *nf_p = cs_ReifNEQ(PQR[i - 1], DIM*DIM - 1);
CSint *end_pqr = cs_ReifEQ(PQR[i], DIM*DIM - 1);

cs_NEQ(cs_Add(f_p, f_c), 0);
cs_NEQ(cs_Add(nf_p, end_pqr), 0);
}

cs_EQ(PQR[0], 0);
cs_EQ(PQR[STP - 1], DIM*DIM - 1);
cs_eventKnown(&PQR[0], STP, knownPQR, NULL);

cs_printf("QR:%A\n", QR, 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:$aa**2

*2: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

2020-11-05

魔方陣セルの即値化順による計算時間のサンプル調査

-----------------------------------------------------------------------------
tout=3; nn=5; pp="$ \+[0-9]\+$"; for*1; do printf "%5d" $aa >/dev/pts/40; timeout $tout ./magicsqure_simp $nn 6 8 16 18 12 0 24 4 20 $(echo 1 2 3 11 21 23 13 22 7 17 5 9 10 14 15 19 |tr " " "\n" |shuf) |sed -ne"/ARGS\|Fail\|Elapsed/ ! d; /ARGS/{h;}; /Fail/{H;}; /Elapsed/{H; g; s/\n/ /g; s/Nb..*Fails = //; s/Elapsed.*ime = //; p;}"; done |sort -nrk 27 |sed -e"s/$pp$pp$pp$pp$pp/\1\2\3\4\5 | /g;" |tail |grep -n " 0 \| 1 \| 2 \| 3 \| 4 "

1:ARGS 6 8 16 18 12 | 0 24 4 20 9 | 7 14 2 23 10 | 11 22 5 13 1 | 19 17 15 3 21 | 1133007 2.90488 s
2:ARGS 6 8 16 18 12 | 0 24 4 20 9 | 5 15 2 21 14 | 10 11 7 13 22 | 3 23 1 17 19 | 1122005 2.92625 s
3:ARGS 6 8 16 18 12 | 0 24 4 20 7 | 9 14 19 2 11 | 13 22 17 15 23 | 3 5 21 10 1 | 1096427 2.84937 s
4:ARGS 6 8 16 18 12 | 0 24 4 20 7 | 9 17 15 14 19 | 11 1 22 13 23 | 3 5 21 10 2 | 1063721 2.72319 s
5:ARGS 6 8 16 18 12 | 0 24 4 20 7 | 5 14 2 19 1 | 15 9 13 23 3 | 10 22 21 11 17 | 1049436 2.77985 s
6:ARGS 6 8 16 18 12 | 0 24 4 20 5 | 7 19 17 11 13 | 1 2 10 9 22 | 3 23 14 21 15 | 1006366 2.56388 s
7:ARGS 6 8 16 18 12 | 0 24 4 20 9 | 5 10 14 13 2 | 7 22 11 23 1 | 3 19 15 21 17 | 993892 2.6823 s
8:ARGS 6 8 16 18 12 | 0 24 4 20 5 | 7 14 10 11 15 | 2 1 3 13 17 | 9 22 21 19 23 | 982430 2.67024 s
9:ARGS 6 8 16 18 12 | 0 24 4 20 7 | 5 15 19 3 17 | 2 11 1 21 10 | 14 23 9 22 13 | 980750 2.55122 s
10:ARGS 6 8 16 18 12 | 0 24 4 20 7 | 5 15 14 13 22 | 23 3 2 11 21 | 10 19 9 17 1 | 959628 2.51054 s

-----------------------------------------------------------------------------
/**************************************************************************
* 魔方陣
* ./magicsqure_simp 5 6 8 16 18 12 0 24 4 20 1 2 3 11 21 23 13 22 7 17 5 9 10 14 15 19
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"

int DIM, LIM_MAIN;
CSint **CELL;
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
int i, val;
static int NbSolutions = 0;

//if(++NbSolutions >= 10000 / 2) exit(1);
if(++NbSolutions >= 10000 / 2) cs_cancelSearch();

// printf("\033[0;0f");
// printf("\nSolution %6d\n", ++NbSolutions);
return;
for (i = 0; i < DIM*DIM; i++) {
val = cs_getValue(CELL[i]);
printf("%3d", val);
if*2;
DIM = atoi(argv[1]); LIM_MAIN = DIM*(DIM*DIM-1)/2;

CELL = (CSint **)malloc(DIM*DIM * sizeof(CSint *));
CSint **N_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("ARGS ");
for(i = 0; i < DIM * DIM; i++){
int j = atoi(argv[2+i]);

printf("%3d", j);
N_CELL[i] = CELL[j];
}
putchar('\n');
cs_printf("%A\n", N_CELL, DIM*DIM);
//exit(1);
printf("\033[2J\033[0;0f"); /* clear screen */
/*
cs_findAll(&N_CELL[0], DIM*DIM, cs_findFreeVar, printSolution);
cs_findAll(&N_CELL[0], DIM*DIM, cs_findFreeVarNbElements, printSolution);
cs_findAll(&N_CELL[0], DIM*DIM, cs_findFreeVarNbElementsMin, printSolution);
cs_findAll(&N_CELL[0], DIM*DIM, cs_findFreeVarNbConstraints, printSolution);
*/
cs_findAll(&N_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:aa=0; aa<2 * 1200; aa++

*2: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

2020-10-07

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

2020-09-13

ナンバーリンクをiZ-Cを使って解きます。

ナンバーリンクをiZ-Cを使って解きます。
-----------------------------------------------------------------------------
make && ./num_link 10 1 3 3 7 7 11 2 2 8 8 15 1 1 6 7 12
Sun Sep 13 11:13:36 2020
10, 1
3 3 7 7 11
QR:3, 3, {2..4}, {2..4}, {1..5}, {1..5}, {0..6}, {0..6}, {1..7}, {1..7}, {2..8}, {2..8}, {3..9}, {3..9}, {4..9}, {4..9}, {5..9}, {5..9}, {6..8}, {6..8}, 7, 7, 2, 2, {1..3}, {1..3}, {0..4}, {0..4}, {0..5}, {0..5}, {0..6}, {0..6}, {0..7}, {0..7}, {0..8}, {0..8}, {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, 8, 1, 1, {0..2}, {0..2}, {0..3}, {0..3}, {0..4}, {0..4}, {0..5}, {0..5}, {0..6}, {1..6}, {1..7}, {2..7}, {2..8}, {3..8}, {3..9}, {4..9}, {4..8}, {5..9}, {5..7}, {6..8}, 6, 7
ESC[2JESC[0;0fESC[0;0f
Step 38, Solution 1
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 18 6 35 . .
. . . . . 19 7 36 . .
. . . . . 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
ESC[0;0f
Step 38, Solution 2
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 . 6 35 . .
. . . . 18 19 7 36 . .
. . . . . 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
ESC[0;0f
Step 38, Solution 3
. . . . . . . . . .
. 26 27 28 29 30 31 32 . .
. 12 11 1 2 3 4 33 . .
. 13 14 0 . . 5 34 . .
. . 15 16 17 . 6 35 . .
. . . . 18 . 7 36 . .
. . . . 19 20 8 37 . .
. . . . . 21 9 10 . .
. . . . . 22 23 24 25 .
. . . . . . . . . .
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Step 38, Solution 614726
. . . . . . . . . .
. 26 27 28 . . . . . .
. . 11 29 30 . . . . .
. . 12 0 31 . . . . .
. . 13 1 32 . . . . .
. . 14 2 33 . . . . .
. . 15 3 34 35 36 37 . .
. . 16 4 . . . 10 . .
. . 17 5 6 7 8 9 25 .
. . 18 19 20 21 22 23 24 .

Nb Fails = 6395740
Nb Choice Points = 12168382
Heap Size = 3072
Elapsed Time = 38.5832 s
Sun Sep 13 11:15:22 2020
----------------------------------------------------------------------------
/**************************************************************************
* 格子道順
**************************************************************************/
#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]);
DISP = atoi(argv[2]);
int SET_NUM = (argc -3)/5;
STP = 0;
for(i = 0; i < SET_NUM; i++){
for(j = 0; j < 5; j++){
NUM_SET[i][j] = atoi(argv[3 + 5 * i + j]);
}
STP += NUM_SET[i][4];
}
printf("%3d, %3d\n", DIM, DISP);
for(j = 0; j < 5; j++) printf("%4d", NUM_SET[0][j]);
putchar('\n');

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

int pre_STP = 0;
for (j = 0; j < SET_NUM; j++){
cs_EQ(QR[2*pre_STP + 0], NUM_SET[j][0]);
cs_EQ(QR[2*pre_STP + 1], NUM_SET[j][1]);
//exit(1);
cs_EQ(QR[2*(pre_STP + NUM_SET[j][4] - 1) + 0], NUM_SET[j][2]);
cs_EQ(QR[2*(pre_STP + NUM_SET[j][4] - 1) + 1], NUM_SET[j][3]);
for (i = pre_STP + 1; i < pre_STP + NUM_SET[j][4]; 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);
}
pre_STP += NUM_SET[j][4];
}

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, j;
int NUM_SET[10][5];
clock_t t0 = clock();
time_t nowtime;

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

sunasunaxの日記

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

最小手数で夫婦３組の川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で宣教師と人食いの川渡りを制約論理プログラム iZ-Cを使って解きます。

最小手数で農夫山羊狼キャベツの川渡りを制約論理プログラム iZ-Cを使って解きます。

格子道順ふかしぎお姉さんといっしょに数えてみよう。をiZ-Cで解きます。

魔方陣セルの即値化順による計算時間のサンプル調査

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

ナンバーリンクをiZ-Cを使って解きます。