2021-02-05

隣接行列から到達可能経路と距離を制約論理プログラム iZ-Cを使って探します

隣接行列から到達可能経路と距離を制約論理プログラム iZ-Cを使って探します。
---------------------------------------------------------------------------
make && ./short_path 0 4 6
make: 'all' に対して行うべき事はありません.
Fri Feb 5 08:59:06 2021
QR:0, {0..5}, {0..5}, {0..5}, {0..5}, {0..5}

Solution 1 SUM 24 step 6
QR: 0, 1, 2, 3, 5, 4
QR_SUM: 0, 1, 3, 6, 9, 24

Solution 2 SUM 4 step 4
QR: 0, 1, 2, 4
QR_SUM: 0, 1, 3, 4

Solution 3 SUM 7 step 5
QR: 0, 1, 3, 2, 4
QR_SUM: 0, 1, 3, 6, 7

Solution 4 SUM 10 step 5
QR: 0, 1, 3, 5, 4
QR_SUM: 0, 1, 3, 6, 10

Solution 5 SUM 14 step 6
QR: 0, 2, 1, 3, 5, 4
QR_SUM: 0, 5, 7, 9, 12, 14

Solution 6 SUM 15 step 5
QR: 0, 2, 3, 5, 4
QR_SUM: 0, 5, 8, 11, 15

Solution 7 SUM 6 step 3
QR: 0, 2, 4
QR_SUM: 0, 5, 6

Nb Fails = 18
Nb Choice Points = 37
Heap Size = 1024
Elapsed Time = 0.000163 s
Fri Feb 5 08:59:06 2021
---------------------------------------------------------------------------
/**************************************************************************
* 隣接行列から到達可能経路と距離を探す。
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

#define app1

/**************************************************************************/
#ifdef app1
#define DIM 6
int ADJ[DIM][DIM] = {
// 0 1 2 3 4 5
{ 0, 1, 5, 0, 0, 0}, // 0
{ 1, 0, 2, 2, 0, 0}, // 1
{ 5, 2, 0, 3, 1, 0}, // 2
{ 0, 2, 3, 0, 0, 3}, // 3
{ 0, 0, 1, 0, 0, 4}, // 4
{ 0, 0, 0, 3, 4, 0}}; // 5
#endif
/**************************************************************************/
/**************************************************************************/
CSint **QR;
CSint **QR_SUM;
int START, GOAL, MAX_STP;
CSint *cost;
CSint *cost_index;
/**************************************************************************/
/**************************************************************************/
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(int val, int index, CSint **allvars, int size, void *extra) {
int i;
int END = (long int)(int *)extra;
int prevQR;

if(index == 0){
QR_SUM[0] = CSINT(0);
}
else {
if(cs_isFree(QR[index - 1])) return FALSE;
prevQR = cs_getValue(QR[index - 1]);
if(ADJ[prevQR][val] == 0) return FALSE;
QR_SUM[index] = cs_Add(QR_SUM[index - 1], CSINT(ADJ[prevQR][val]));
}
for(i = 0; i < size; i++){
if(val == END) break;
if(i == index) continue;
if(! cs_NEQ(allvars[i], val)) return FALSE;
}
// cs_printf("%A\n", QR, size);

if(val == END) {
prevQR = cs_getValue(QR[index - 1]);
if(prevQR != END) {
// QR_SUM[index - 1] = cs_Add(QR_SUM[index - 2], CSINT(ADJ[cs_getValue(QR[index - 1])][prevQR]));
QR_SUM[index] = cs_Add(QR_SUM[index - 1], CSINT(ADJ[prevQR][val]));
// cs_printf("%A\n", QR_SUM, index+1);
// cost_index = CSINT(index);
}
for(i = index + 1; i < size; i++){
if(cs_EQ(allvars[i], END)) return FALSE;
}
// cs_printf("%A\n", QR, size);
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;

int step = 1 + cs_getMin(cost);
int path_sum = cs_getValue(QR_SUM[step - 1]);

printf("\nSolution %d SUM %d step %d\n", ++NbSolutions, path_sum, step);

printf(" QR: ");
cs_printf("%A\n", &QR[0], step);
printf("QR_SUM: ");
cs_printf("%A\n", &QR_SUM[0], step);
}
/**************************************************************************/
/**************************************************************************/
void printSolution1(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;

int step = 1 + cs_getMin(cost);
int path_sum = cs_getValue(QR_SUM[step - 1]);

printf("\nSolution %d SUM %d step %d\n", ++NbSolutions, path_sum, step);

printf(" QR: ");
cs_printf("%A\n", &QR[0], step);
printf("QR_SUM: ");
cs_printf("%A\n", &QR_SUM[0], step);
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;

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

START = atoi(argv[1]);
GOAL = atoi(argv[2]);
MAX_STP = atoi(argv[3]);

QR = (CSint **)malloc(MAX_STP * sizeof(CSint *));
QR_SUM = (CSint **)malloc(MAX_STP * sizeof(CSint *));

for(i = 0; i < MAX_STP; i++){
QR[i] = cs_createCSint(0, DIM - 1);
QR_SUM[i] = CSINT(20);
}
cs_EQ(QR[0], START);

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

cs_eventKnown(&QR[0], MAX_STP, knownQR, (void *)(long)GOAL);

cost_index = cs_Index(&QR[0], MAX_STP, GOAL);
cost = cost_index;
/*
cs_printf("cost_index: %D\n", cost_index);
*/

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

2021-01-22

改良版：ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。

改良版：ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
aa=5; make && ./hanoi $aa $*1
make: 'all' に対して行うべき事はありません.
Fri Jan 22 15:58:49 2021
QR:0, 0, 0, 0, 0, {1, 2}, 0, 0, 0, 0, {1, 2}, {0..2}, 0, 0, 0, {0..2}, {0..2}, {0..2}, 0, 0, {0..2}, {0..2}, {0..2}, {0..2}, 0, {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}, {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}, {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}, {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}, {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}, {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}, {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}, {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}, {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}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}
QR_PD:0, {1, 2}, {1..8}, {0..26}, {0..80}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}, {0..242}

Step 32, Solution 1
0 1 2 3 4
0 : 0, 0, 0, 0, 0
1 : 2, 0, 0, 0, 0
2 : 2, 1, 0, 0, 0
3 : 1, 1, 0, 0, 0
4 : 1, 1, 2, 0, 0
5 : 0, 1, 2, 0, 0
6 : 0, 2, 2, 0, 0
7 : 2, 2, 2, 0, 0
8 : 2, 2, 2, 1, 0
9 : 1, 2, 2, 1, 0
10 : 1, 0, 2, 1, 0
11 : 0, 0, 2, 1, 0
12 : 0, 0, 1, 1, 0
13 : 2, 0, 1, 1, 0
14 : 2, 1, 1, 1, 0
15 : 1, 1, 1, 1, 0
16 : 1, 1, 1, 1, 2
17 : 0, 1, 1, 1, 2
18 : 0, 2, 1, 1, 2
19 : 2, 2, 1, 1, 2
20 : 2, 2, 0, 1, 2
21 : 1, 2, 0, 1, 2
22 : 1, 0, 0, 1, 2
23 : 0, 0, 0, 1, 2
24 : 0, 0, 0, 2, 2
25 : 2, 0, 0, 2, 2
26 : 2, 1, 0, 2, 2
27 : 1, 1, 0, 2, 2
28 : 1, 1, 2, 2, 2
29 : 0, 1, 2, 2, 2
30 : 0, 2, 2, 2, 2
31 : 2, 2, 2, 2, 2

Nb Fails = 70
Nb Choice Points = 143
Heap Size = 21504
Elapsed Time = 0.026379 s
Fri Jan 22 15:58:49 2021
/**************************************************************************
* ハノイの塔最小手数に最適化する
BBB
012
0:000
1:200
2:210
3:110
4:112
5:012
6:022
7:222
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

/**************************************************************************/
CSint **QR;
int QR_PD_END;
CSint **QR_PD;
int DIM, MAX_STP;
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
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) return TRUE;
for(i = 0; i < size; i++){
if(i == index) continue;
if(!cs_NEQ(allvars[i], val)) return FALSE;
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution1(CSint **allvars, int nbVars, CSint *cost) {
static int NbSolutions = 0;
int i;
int step = 1 + cs_getMin(cost);

printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf(" ");
for(i = 0; i < DIM; i++) {
printf("%1d %c", i, (i+1) % DIM == 0 ? '\n' : ' ');
}
for(i = 0; i < step; i++) {
printf("%2d : ", i);
cs_printf("%A\n", &QR[DIM * i], DIM);
}
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i;

printf("\nStep %d, Solution %d\n", MAX_STP, ++NbSolutions);
printf(" ");
for(i = 0; i < DIM; i++) {
printf("%1d %c", i, (i+1) % DIM == 0 ? '\n' : ' ');
}
for(i = 0; i < MAX_STP; i++) {
printf("%2d : ", i);
cs_printf("%A\n", &QR[DIM * i], DIM);
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i, j;
clock_t t0 = clock();
time_t nowtime;

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

DIM = atoi(argv[1]);
MAX_STP = atoi(argv[2]);

int *order = (int *)malloc(DIM *sizeof(int));
for(order[0] = 1, i = 0; i < DIM - 1; i++){
order[i + 1] = order[i] * 3;
}
QR_PD_END = order[DIM-1] * 3 - 1;

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

for(i = 0; i < MAX_STP; i++){
for(j = 0; j < DIM; j++){
QR[DIM * i + j] = cs_createCSint(0, 2);
}
QR_PD[i] = cs_ScalProd(&QR[DIM*i], &order[0], DIM);
}
cs_EQ(QR_PD[0], 0);
for (i = 1; i < MAX_STP; i++){
CSint **curr = (CSint **)malloc(DIM* sizeof(CSint *));
CSint **prev = (CSint **)malloc(DIM* sizeof(CSint *));
CSint **chg = (CSint **)malloc(DIM*MAX_STP * sizeof(CSint *));
for (j = 0; j < DIM; j++){
curr[j] = QR[DIM*i + j];
prev[j] = QR[DIM*(i - 1) + j];
chg[j] = cs_ReifNeq(curr[j], prev[j]);
}

CSint *chg_num = cs_OccurDomain(1, &chg[0], DIM);
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(chg_num, 0), cs_ReifEQ(chg_num, 1));

for (j = 0; j < DIM; j++){
int k = 1 << j;
if(i < MAX_STP - k){
for (int l = 1; l < k + 1; l++){
imp(cs_ReifEQ(chg[j], 1), cs_ReifEq(QR[DIM*(i + l) + j], curr[j]));
}
}
}

for (j = 1; j < DIM; j++){
for (int k = 0; k < j; k++){
CSint *eq_prev = cs_ReifEq(prev[k], prev[j]);
imp(eq_prev, cs_ReifEq(curr[j], prev[j]));
imp(cs_ReifEq(prev[k], curr[j]), eq_prev);
}
}
}

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

cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, (void *)(long)QR_PD_END);

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

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

*1:2**aa + 1

2021-01-18

最小手数で家族とじっちゃんの川渡りを制約論理プログラム 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
---------------------------------------------------------------------------
/**************************************************************************
* ある家族がいて、舟を使って川を向こう岸へ渡ろうとしています。
* この家族は父、母、息子１、息子２、娘１、娘２、メイド、犬、じっちゃん、
* 赤ん坊の１０人家族(犬も１人と数えます)です。
* 舟は１艘(そう)しかなく、１度に２人まで乗ることができます。
* また、この舟をこげるのは父と母とメイドとじっちゃんの４人です。
*
* そしてこの家族、実はとっても危ない家族なんです。
* 父は、母がいなくなると娘を殺してしまいます。
* 母は、父がいなくなると息子を殺してしまいます。
* じっちゃんは、親がいないと息子や娘、赤ん坊を殺してしまいます。
* 息子や娘は、親がいないと赤ん坊を殺してしまいます。
* そしてきわめつけ。
* 犬は、メイドがいないと家族をみんな殺してしまいます。
*
* それでは問題です。
* みんなが無事に川を渡り切るには、どのような手順で渡ればよいでしょうか？
* 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;
}

2021-01-16

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

最小手数で家族の川渡りを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
aa=22; make && ./river_family $aa
make: 'all' に対して行うべき事はありません.
Sat Jan 16 20:38:34 2021
QR: 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}
QR_PD: 0, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}, {1..511}

Step 18, Solution 1
boart = 0, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8
0: 0, 0, 0, 0, 0, 0, 0, 0, 0 [b,d,m,f,M,S,s,G,g] [ , , , , , , , , ]
1: 1, 1, 1, 0, 0, 0, 0, 0, 0 [ , , ,f,M,S,s,G,g] [b,d,m, , , , , , ]
2: 0, 1, 0, 0, 0, 0, 0, 0, 0 [b, ,m,f,M,S,s,G,g] [ ,d, , , , , , , ]
3: 1, 1, 1, 0, 0, 0, 0, 0, 1 [ , , ,f,M,S,s,G, ] [b,d,m, , , , , ,g]
4: 0, 0, 0, 0, 0, 0, 0, 0, 1 [b,d,m,f,M,S,s,G, ] [ , , , , , , , ,g]
5: 1, 0, 0, 0, 1, 0, 0, 1, 1 [ ,d,m,f, ,S,s, , ] [b, , , ,M, , ,G,g]
6: 0, 0, 0, 0, 0, 0, 0, 1, 1 [b,d,m,f,M,S,s, , ] [ , , , , , , ,G,g]
7: 1, 0, 0, 1, 1, 0, 0, 1, 1 [ ,d,m, , ,S,s, , ] [b, , ,f,M, , ,G,g]
8: 0, 0, 0, 0, 1, 0, 0, 1, 1 [b,d,m,f, ,S,s, , ] [ , , , ,M, , ,G,g]
9: 1, 1, 1, 0, 1, 0, 0, 1, 1 [ , , ,f, ,S,s, , ] [b,d,m, ,M, , ,G,g]
10: 0, 1, 1, 0, 0, 0, 0, 1, 1 [b, , ,f,M,S,s, , ] [ ,d,m, , , , ,G,g]
11: 1, 1, 1, 1, 1, 0, 0, 1, 1 [ , , , , ,S,s, , ] [b,d,m,f,M, , ,G,g]
12: 0, 1, 1, 0, 1, 0, 0, 1, 1 [b, , ,f, ,S,s, , ] [ ,d,m, ,M, , ,G,g]
13: 1, 1, 1, 1, 1, 0, 1, 1, 1 [ , , , , ,S, , , ] [b,d,m,f,M, ,s,G,g]
14: 0, 0, 0, 1, 1, 0, 1, 1, 1 [b,d,m, , ,S, , , ] [ , , ,f,M, ,s,G,g]
15: 1, 0, 1, 1, 1, 1, 1, 1, 1 [ ,d, , , , , , , ] [b, ,m,f,M,S,s,G,g]
16: 0, 0, 0, 1, 1, 1, 1, 1, 1 [b,d,m, , , , , , ] [ , , ,f,M,S,s,G,g]
17: 1, 1, 1, 1, 1, 1, 1, 1, 1 [ , , , , , , , , ] [b,d,m,f,M,S,s,G,g]

Nb Fails = 356
Nb Choice Points = 727
Heap Size = 18432
Elapsed Time = 0.008341 s
Sat Jan 16 20:38:34 2021

---------------------------------------------------------------------------
/**************************************************************************
* ある家族がいます。
* この家族は舟を使って川の向こう岸へわたろうとしています。
* 舟は１艘(そう)しかなく、１度に２人まで乗ることができます。
* 家族は父、母、息子１、息子２、娘１、
* 娘２、メイド、犬の８人(犬も１人と数えます)であり、
* またこの舟をこげるのは父か母かメイドの３人だけです。
*
* さぁ、そしてこの家族、ぢつは！とっても危険な家族なんです。
* まず父は、母がいないと娘を殺してしまいます。
* また母は、父がいないと息子を殺してしまいます。
* そしてきわめつけ。
* 犬は、メイドがいないと家族をみんな殺してしまいます。
*
* 誰も死ぬことなく川をわたりきるにはどうすればよいでしょうか？
* 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, father, mother, son1, son2, daughter1, daughter2};
/**************************************************************************/
/**************************************************************************/
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;

printf("\nStep %d, Solution %d\n", step, ++NbSolutions);
printf("boart = 0, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8\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, dog = 1, maid = 2, father = 3, mother = 4, son = 5_6, daughter = 7_8\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 = 9;
QR_PD_END = (1 << DIM) - 1;
// int order[9] ={1, 2, 4, 8, 16, 32, 64, 128, 256};
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, father, mother, son1, son2, daughter1, daughter2};
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_bt_j = 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_bt_j), 0));
}
}

CSint **mv_eq_boart = (CSint **)malloc(3 * sizeof(CSint *));
for(int k = 0; k < 3; k++) mv_eq_boart[k] = cs_ReifEq(mv[boart], mv[maid + k]);
imp(cs_ReifNEQ(mv[boart], 0), cs_ReifNEQ(cs_Sigma(&mv_eq_boart[0], 3), 0));

CSint *curr_pos_fath_moth = cs_ReifNeq(curr_pos[father], curr_pos[mother]);
imp(curr_pos_fath_moth,
cs_ReifEQ(cs_Add(cs_ReifEq(curr_pos[mother], curr_pos[son1]),
cs_ReifEq(curr_pos[mother], curr_pos[son2])), 0));

imp(curr_pos_fath_moth,
cs_ReifEQ(cs_Add(cs_ReifEq(curr_pos[father], curr_pos[daughter1]),
cs_ReifEq(curr_pos[father], curr_pos[daughter2])), 0));

CSint **curr_pos_eq_dog = (CSint **)malloc(6 * sizeof(CSint *));
for(int k = 0; k < 6; k++) curr_pos_eq_dog[k] = cs_ReifEq(curr_pos[dog], curr_pos[father + k]);
imp(cs_ReifNeq(curr_pos[dog], curr_pos[maid]), cs_ReifEQ(cs_Sigma(&curr_pos_eq_dog[0], 6), 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_printStats();
printf("Elapsed Time = %g s\n", (double) (clock() - t0) / CLOCKS_PER_SEC);
time(&nowtime); printf("%s", ctime(&nowtime));
cs_end();
return EXIT_SUCCESS;
}

2021-01-10

ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。最小手数に最適化してゆきます。

ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
解答は板がどの棒に刺さっているかが変化し最小手数に最適化してゆきます。
make && ./hanoi 4 18
make: 'all' に対して行うべき事はありません.
Sun Jan 10 07:51:23 2021
QR:0, 0, 0, 0, {1, 2}, 0, 0, 0, {0..2}, {0..2}, 0, 0, {0..2}, {0..2}, {0..2}, 0, {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}, {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}, {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}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}
QR_PD:0, {1, 2}, {0..8}, {0..26}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}, {0..80}

Step 18, Solution 1
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 0, 2, 0, 0
4 : 2, 2, 0, 0
5 : 2, 2, 1, 0
6 : 0, 2, 1, 0
7 : 0, 1, 1, 0
8 : 1, 1, 1, 0
9 : 1, 1, 1, 2
10 : 0, 1, 1, 2
11 : 2, 1, 1, 2
12 : 2, 0, 1, 2
13 : 0, 0, 1, 2
14 : 0, 0, 2, 2
15 : 1, 0, 2, 2
16 : 1, 2, 2, 2
17 : 2, 2, 2, 2

Step 17, Solution 2
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 0, 2, 0, 0
4 : 2, 2, 0, 0
5 : 2, 2, 1, 0
6 : 0, 2, 1, 0
7 : 0, 1, 1, 0
8 : 1, 1, 1, 0
9 : 1, 1, 1, 2
10 : 2, 1, 1, 2
11 : 2, 0, 1, 2
12 : 0, 0, 1, 2
13 : 0, 0, 2, 2
14 : 1, 0, 2, 2
15 : 1, 2, 2, 2
16 : 2, 2, 2, 2

Step 16, Solution 3
0 1 2 3
0 : 0, 0, 0, 0
1 : 1, 0, 0, 0
2 : 1, 2, 0, 0
3 : 2, 2, 0, 0
4 : 2, 2, 1, 0
5 : 0, 2, 1, 0
6 : 0, 1, 1, 0
7 : 1, 1, 1, 0
8 : 1, 1, 1, 2
9 : 2, 1, 1, 2
10 : 2, 0, 1, 2
11 : 0, 0, 1, 2
12 : 0, 0, 2, 2
13 : 1, 0, 2, 2
14 : 1, 2, 2, 2
15 : 2, 2, 2, 2

Nb Fails = 1923
Nb Choice Points = 2979
Heap Size = 5120
Elapsed Time = 0.027825 s
Sun Jan 10 07:51:23 2021

/**************************************************************************
* ハノイの塔最小手数に最適化する
BBB
012
0:000
1:200
2:210
3:110
4:112
5:012
6:022
7:222
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"

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

DIM = atoi(argv[1]);
MAX_STP = atoi(argv[2]);

int *order = (int *)malloc(DIM *sizeof(int));
for(order[0] = 1, i = 0; i < DIM - 1; i++){
order[i + 1] = order[i] * 3;
}
QR_PD_END = order[DIM-1] * 3 - 1;

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

for (int i = 1; i < DIM; i++){
for (int j = 0; j < i; j++){
imp(cs_ReifEq(prev[i], prev[j]), cs_ReifEq(curr[i], prev[i]));
imp(cs_ReifNeq(prev[i], prev[j]), cs_ReifNeq(prev[j], curr[i]));
}
}
}

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

cs_eventKnown(&QR_PD[0], MAX_STP, knownQR_PD, (void *)(long)QR_PD_END);

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

2021-01-04

最小時間で4艘の舟運びを制約論理プログラム iZ-Cを使って解きます。

025_最小時間で4艘の舟運びを制約論理プログラム iZ-Cを使って解きます。
----------------------------------------------------------------------------
make && ./river_boart 18
gcc -Wall -O3 -I. -L. -o river_boart river_boart.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Mon Jan 4 15:56:24 2021
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}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {0, 1}, {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..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}, {1..31}

Step 12, Solution 1, cost 88
TIME 0, 16, 8, 8, 16, 4, 8, 2, 4, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 0, 1, 1, 0 [ ,1, , ,4] [c, ,2,3, ]
6: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
7: 1, 1, 1, 0, 0 [ , , ,3,4] [c,1,2, , ]
8: 0, 1, 0, 0, 0 [c, ,2,3,4] [ ,1, , , ]
9: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
10: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
11: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 10, Solution 2, cost 86
TIME 0, 16, 8, 8, 16, 4, 8, 16, 2, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 0, 1, 1, 0 [ ,1, , ,4] [c, ,2,3, ]
6: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
7: 1, 1, 1, 0, 1 [ , , ,3, ] [c,1,2, ,4]
8: 0, 0, 1, 0, 1 [c,1, ,3, ] [ , ,2, ,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 10, Solution 3, cost 80
TIME 0, 16, 8, 8, 16, 2, 8, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 1, 0, 1, 0 [ , ,2, ,4] [c,1, ,3, ]
6: 0, 1, 0, 0, 0 [c, ,2,3,4] [ ,1, , , ]
7: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
8: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 8, Solution 4, cost 70
TIME 0, 16, 8, 8, 16, 16, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 0 [c,1,2, ,4] [ , , ,3, ]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
7: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 10, Solution 5, cost 60
TIME 0, 16, 8, 8, 4, 2, 8, 4, 2, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 1, 0, 0, 1 [c, ,2,3, ] [ ,1, , ,4]
7: 1, 1, 1, 0, 1 [ , , ,3, ] [c,1,2, ,4]
8: 0, 0, 1, 0, 1 [c,1, ,3, ] [ , ,2, ,4]
9: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 8, Solution 6, cost 54
TIME 0, 16, 8, 8, 4, 2, 8, 8
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
6: 0, 1, 0, 0, 1 [c, ,2,3, ] [ ,1, , ,4]
7: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 7, cost 40
TIME 0, 16, 8, 8, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 8, cost 38
TIME 0, 16, 8, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 0, 1, 1 [ ,1,2, , ] [c, , ,3,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 9, cost 36
TIME 0, 16, 4, 8, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 1, 0, 1 [ ,1, ,3, ] [c, ,2, ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 10, cost 34
TIME 0, 16, 4, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 0, 1, 0, 1 [ ,1, ,3, ] [c, ,2, ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 11, cost 32
TIME 0, 16, 2, 8, 2, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 1, 0, 0, 1 [ , ,2,3, ] [c,1, , ,4]
2: 0, 0, 0, 0, 1 [c,1,2,3, ] [ , , , ,4]
3: 1, 1, 0, 1, 1 [ , ,2, , ] [c,1, ,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Step 6, Solution 12, cost 30
TIME 0, 4, 2, 16, 4, 4
captain = 0, boart = 1_4
0: 0, 0, 0, 0, 0 [c,1,2,3,4] [ , , , , ]
1: 1, 1, 1, 0, 0 [ , , ,3,4] [c,1,2, , ]
2: 0, 0, 1, 0, 0 [c,1, ,3,4] [ , ,2, , ]
3: 1, 0, 1, 1, 1 [ ,1, , , ] [c, ,2,3,4]
4: 0, 0, 0, 1, 1 [c,1,2, , ] [ , , ,3,4]
5: 1, 1, 1, 1, 1 [ , , , , ] [c,1,2,3,4]

Nb Fails = 219
Nb Choice Points = 513
Heap Size = 5120
Elapsed Time = 0.010544 s
Mon Jan 4 15:56:24 2021
----------------------------------------------------------------------------
/**************************************************************************
* ４艘(そう)の舟運び
* 川の左岸に舟が４艘(そう)ある。
* 右岸まで横断するには、
* Ａ舟は２分、Ｂ舟は４分、Ｃ舟は８分、Ｄ舟は１６分かかる。
* この舟すべてを右岸に運びたいが、船頭は１人しかいない。
* １艘にもう１艘だけをロープでつないで渡ることができるが、
* そのときは遅いほうの時間がかかってしまう。
*
* すべてを運ぶには最短で何分かかるだろうか？
*
* ただし舟の乗りかえ、つなぐ時間などはすべて無視する。
* 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;
CSint **TIME;
enum {captain, boart1, boart2, boart3, boart4};
/**************************************************************************/
/**************************************************************************/
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;
int END = (long int)(int *)extra;
//cs_printf("%A\n", allvars, MAX_STP);
// if(val == QR_PD_END) return TRUE;
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;
}
/**************************************************************************/
/**************************************************************************/
void print_sub(int selct, int chk_num){
char alph[7] ={"c1234"};
int j;

printf("\nStep %d, Solution %d, cost %d\n", step, ++NbSolutions, cs_getValue(cost));
// cs_printf("TIME %A\n", TIME, step);
cs_printf("TIME %A\n", TIME, step);
printf("captain = 0, boart = 1_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("captain = 0, boart = 1_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");
}
}
/**************************************************************************/
/**************************************************************************/
CSint *cs_inc_pos_num(CSint **array, int num, int man, int pos){
CSint *current = cs_OccurDomain(pos, &array[DIM*num + man], 3);
CSint *prev = cs_OccurDomain(pos, &array[DIM*(num-1) + man], 3);
return cs_Sub(current, prev);
}
/**************************************************************************/
/**************************************************************************/
void boart_direction(CSint *pos_num, CSint *boart_dir){
cs_NEQ(cs_Add(cs_ReifLE(pos_num, 0), cs_ReifEQ(boart_dir, 1)), 0);
cs_NEQ(cs_Add(cs_ReifNEQ(pos_num, 0), cs_ReifEQ(boart_dir, 0)), 0);
cs_NEQ(cs_Add(cs_ReifGE(pos_num, 0), cs_ReifEQ(boart_dir, -1)), 0);
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
int i;
clock_t t0 = clock();
time_t nowtime;
DIM = 5;
QR_PD_END = (1 << DIM) - 1;
int order[5] ={1, 2, 4, 8, 16};

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

QR = (CSint **)malloc(DIM * MAX_STP * sizeof(CSint *));
TIME = (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);

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

TIME[0] = CSINT(0);
for(i = 1; i < MAX_STP; i++){
CSint **mv = (CSint **)malloc(DIM * sizeof(CSint *));
CSint **Abs_mv = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
mv[j] = cs_Sub(QR[DIM*i+j], QR[DIM*(i-1)+j]);
Abs_mv[j] = cs_Abs(mv[j]);
}

CSint *inc_boart_pos0_num = cs_inc_pos_num(QR, i, boart1, 0);
CSint *inc_boart_pos1_num = cs_inc_pos_num(QR, i, boart1, 1);

cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(mv[captain], 0), cs_ReifNEQ(mv[captain], 0));
cs_LE(cs_Sigma(&Abs_mv[boart1], DIM-1), 2);
cs_InInterval(inc_boart_pos0_num, -2, 2);
cs_InInterval(inc_boart_pos1_num, -2, 2);

int inc_boart_pos1_num_value[5] = {-1, -1, 0, 1, 1};
CSint *captain_pos1= cs_Element(cs_Add(CSINT(2), inc_boart_pos1_num), inc_boart_pos1_num_value, 5);

cs_EQ(cs_Add(inc_boart_pos0_num, inc_boart_pos1_num), 0);
cs_Eq(captain_pos1, mv[captain]);

cs_GE(cs_Mul(cs_Min(&mv[boart1], DIM-1), cs_Max(&mv[boart1], DIM-1)), 0);

int time_order[5] = {1, 2, 4, 8, 16};
CSint **tim_tmp = (CSint **)malloc(DIM * sizeof(CSint *));
for(int j = 0; j < DIM; j++){
tim_tmp[j] = cs_Mul(Abs_mv[j], CSINT(time_order[j]));
}
// CSint *PRE_TIME = cs_createCSint(0, 1000);
int ttime_order[6] = {0, 1, 2, 4, 8, 16};
CSint *PRE_TIME = cs_createCSintFromDomain(&ttime_order[0], DIM+1);
//cs_printf("%D\n", PRE_TIME);
cond_imp(cs_ReifEQ(QR_PD[i- 1], QR_PD_END), cs_ReifEQ(PRE_TIME, 0),
cs_ReifEq(PRE_TIME, cs_Max(&tim_tmp[0], DIM)));
TIME[i] = PRE_TIME;
}

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);
CSint *cost = cs_Sigma(TIME, MAX_STP);

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-23

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

最小手数で宣教師と人食いの川渡り2 （人数をまとめない）を制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
make && ./river_missio 18
gcc -Wall -O3 -I. -L. -o river_missio river_missio.c -L. -liz -L/home/sunasuna/TEST/IZC64/izC_v3_6_1_linux64/lib/
Wed Dec 23 08:18:28 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}, {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}, {1..127}

Step 18, Solution 1
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 0 [ ,m,m,m, , ,d] [b, , , ,d,d, ]
6: 0, 0, 0, 0, 0, 1, 0 [b,m,m,m,d, ,d] [ , , , , ,d, ]
7: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
8: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
9: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
10: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
11: 1, 0, 1, 1, 1, 0, 1 [ ,m, , , ,d, ] [b, ,m,m,d, ,d]
12: 0, 0, 0, 1, 1, 0, 0 [b,m,m, , ,d,d] [ , , ,m,d, , ]
13: 1, 1, 1, 1, 1, 0, 0 [ , , , , ,d,d] [b,m,m,m,d, , ]
14: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
15: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
16: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
17: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]

Step 16, Solution 2
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 0 [ ,m,m,m, , ,d] [b, , , ,d,d, ]
6: 0, 0, 0, 0, 0, 1, 0 [b,m,m,m,d, ,d] [ , , , , ,d, ]
7: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
8: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
9: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
10: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
11: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
12: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
13: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
14: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
15: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]

Step 14, Solution 3
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 0, 1 [ ,m,m,m, ,d, ] [b, , , ,d, ,d]
4: 0, 0, 0, 0, 1, 0, 0 [b,m,m,m, ,d,d] [ , , , ,d, , ]
5: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
6: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
7: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
8: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
9: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
10: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
11: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
12: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
13: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]

Step 12, Solution 4
boart = 0, missionary = 1_3, deamon = 4_6
0: 0, 0, 0, 0, 0, 0, 0 [b,m,m,m,d,d,d] [ , , , , , , ]
1: 1, 0, 0, 0, 0, 1, 1 [ ,m,m,m,d, , ] [b, , , , ,d,d]
2: 0, 0, 0, 0, 0, 0, 1 [b,m,m,m,d,d, ] [ , , , , , ,d]
3: 1, 0, 0, 0, 1, 1, 1 [ ,m,m,m, , , ] [b, , , ,d,d,d]
4: 0, 0, 0, 0, 0, 1, 1 [b,m,m,m,d, , ] [ , , , , ,d,d]
5: 1, 0, 1, 1, 0, 1, 1 [ ,m, , ,d, , ] [b, ,m,m, ,d,d]
6: 0, 0, 0, 1, 0, 0, 1 [b,m,m, ,d,d, ] [ , , ,m, , ,d]
7: 1, 1, 1, 1, 0, 0, 1 [ , , , ,d,d, ] [b,m,m,m, , ,d]
8: 0, 1, 1, 1, 0, 0, 0 [b, , , ,d,d,d] [ ,m,m,m, , , ]
9: 1, 1, 1, 1, 0, 1, 1 [ , , , ,d, , ] [b,m,m,m, ,d,d]
10: 0, 0, 1, 1, 0, 1, 1 [b,m, , ,d, , ] [ , ,m,m, ,d,d]
11: 1, 1, 1, 1, 1, 1, 1 [ , , , , , , ] [b,m,m,m,d,d,d]

Nb Fails = 63771
Nb Choice Points = 127637
Heap Size = 7168
Elapsed Time = 0.402291 s
Wed Dec 23 08:18:28 2020
---------------------------------------------------------------------------
/**************************************************************************
* 宣教師と人食いの川渡り2 （人数をまとめない）
**************************************************************************/
#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, missionary1, missionary2, missionary3, deamon1, deamon2, deamon3};
/**************************************************************************/
/**************************************************************************/
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, missionary = 1_3, deamon = 4_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("boart = 0, missionary = 1_3, deamon = 4_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;
DIM = 7;
QR_PD_END = (1 << DIM) - 1;
int order[7] ={1, 2, 4, 8, 16, 32, 64};

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

//enum {boart, missionary1, missionary2, missionary3, deamon1, deamon2, deamon3};

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);
CSint *mission_pos0_num = cs_OccurDomain(0, &QR[DIM*i + missionary1], 3);
CSint *mission_pos1_num = cs_OccurDomain(1, &QR[DIM*i + missionary1], 3);
CSint *deamon_pos0_num = cs_OccurDomain(0, &QR[DIM*i + deamon1], 3);
CSint *deamon_pos1_num = cs_OccurDomain(1, &QR[DIM*i + deamon1], 3);

boart_pos[i] = QR[DIM*i + boart];

cs_NEQ(cs_Add(cs_ReifEQ(mission_pos0_num, 0), cs_ReifGe(mission_pos0_num, deamon_pos0_num)), 0);
cs_NEQ(cs_Add(cs_ReifEQ(mission_pos1_num, 0), cs_ReifGe(mission_pos1_num, deamon_pos1_num)), 0);
}
//exit(1);

for(i = 1; i < MAX_STP; i++){
CSint *mv_boart = cs_Sub(boart_pos[i], boart_pos[i-1]);

CSint *mv_missionary1 = cs_Sub(QR[DIM*i + missionary1], QR[DIM*(i-1) + missionary1]);
CSint *mv_missionary2 = cs_Sub(QR[DIM*i + missionary2], QR[DIM*(i-1) + missionary2]);
CSint *mv_missionary3 = cs_Sub(QR[DIM*i + missionary3], QR[DIM*(i-1) + missionary3]);
CSint *mv_deamon1 = cs_Sub(QR[DIM*i + deamon1], QR[DIM*(i-1) + deamon1]);
CSint *mv_deamon2 = cs_Sub(QR[DIM*i + deamon2], QR[DIM*(i-1) + deamon2]);
CSint *mv_deamon3 = cs_Sub(QR[DIM*i + deamon3], QR[DIM*(i-1) + deamon3]);

CSint *inc_mission_pos0_num = cs_Sub(cs_OccurDomain(0, &QR[DIM*i + missionary1], 3),
cs_OccurDomain(0, &QR[DIM*(i-1) + missionary1], 3));
CSint *inc_mission_pos1_num = cs_Sub(cs_OccurDomain(1, &QR[DIM*i + missionary1], 3),
cs_OccurDomain(1, &QR[DIM*(i-1) + missionary1], 3));
CSint *inc_deamon_pos0_num = cs_Sub(cs_OccurDomain(0, &QR[DIM*i + deamon1], 3),
cs_OccurDomain(0, &QR[DIM*(i-1) + deamon1], 3));
CSint *inc_deamon_pos1_num = cs_Sub(cs_OccurDomain(1, &QR[DIM*i + deamon1], 3),
cs_OccurDomain(1, &QR[DIM*(i-1) + deamon1], 3));
CSint *inc_md_pos0_num = cs_Add(inc_mission_pos0_num, inc_deamon_pos0_num);
CSint *inc_md_pos1_num = cs_Add(inc_mission_pos1_num, inc_deamon_pos1_num);

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(mv_boart, 0)), 0);
cs_LE(cs_VAdd(6, cs_Abs(mv_missionary1), cs_Abs(mv_missionary2), cs_Abs(mv_missionary3),
cs_Abs(mv_deamon1), cs_Abs(mv_deamon2), cs_Abs(mv_deamon3)), 2);

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

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

cs_GE(cs_Mul(inc_mission_pos0_num, inc_deamon_pos0_num), 0);
cs_GE(cs_Mul(inc_mission_pos1_num, inc_deamon_pos1_num), 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);

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

sunasunaxの日記

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

隣接行列から到達可能経路と距離を制約論理プログラム iZ-Cを使って探します

改良版：ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。

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

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

ハノイの塔パズルを制約論理プログラム iZ-Cを使って解きます。最小手数に最適化してゆきます。

最小時間で4艘の舟運びを制約論理プログラム iZ-Cを使って解きます。

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