おしどりあそびを制約論理プログラム iZ-Cを使って解きます。
おしどりあそびを制約論理プログラム iZ-Cを使って解きます。
---------------------------------------------------------------------------
./oshidori
Sat Jul 18 07:05:17 2020
2, 2, 2, 1, 1, 1, 0, 0, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {0..2}, {1, 2}, {1, 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}, {1, 2}, {1, 2}, 1, 1, 1, 2, 2, 2, 0, 0
Step 6, Solution 1
0: 2, 2, 2, 1, 1, 1, _, _
1: 2, 2, 2, _, _, 1, 1, 1
2: 2, _, _, 2, 2, 1, 1, 1
3: 2, 1, 1, 2, 2, _, _, 1
4: _, _, 1, 2, 2, 2, 1, 1
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 2
0: 2, 2, 2, 1, 1, 1, _, _
1: 2, 2, 2, _, _, 1, 1, 1
2: 2, _, _, 2, 2, 1, 1, 1
3: 2, 2, 1, 2, _, _, 1, 1
4: _, _, 1, 2, 2, 2, 1, 1
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 3
0: 2, 2, 2, 1, 1, 1, _, _
1: 2, 2, 2, 1, _, _, 1, 1
2: _, _, 2, 1, 2, 2, 1, 1
3: 1, 2, 2, _, _, 2, 1, 1
4: 1, _, _, 2, 2, 2, 1, 1
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 4
0: 2, 2, 2, 1, 1, 1, _, _
1: 2, _, _, 1, 1, 1, 2, 2
2: 2, 1, 1, _, _, 1, 2, 2
3: _, _, 1, 2, 1, 1, 2, 2
4: 1, 1, 1, 2, _, _, 2, 2
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 5
0: 2, 2, 2, 1, 1, 1, _, _
1: _, _, 2, 1, 1, 1, 2, 2
2: 1, 1, 2, _, _, 1, 2, 2
3: 1, 1, 2, 1, 2, _, _, 2
4: 1, 1, _, _, 2, 2, 1, 2
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 6
0: 2, 2, 2, 1, 1, 1, _, _
1: _, _, 2, 1, 1, 1, 2, 2
2: 1, 1, 2, 1, _, _, 2, 2
3: 1, _, _, 1, 1, 2, 2, 2
4: 1, 1, 1, _, _, 2, 2, 2
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 7
0: 2, 2, 2, 1, 1, 1, _, _
1: 2, 2, _, _, 1, 1, 2, 1
2: 2, 2, 1, 2, 1, _, _, 1
3: 2, 2, 1, _, _, 2, 1, 1
4: _, _, 1, 2, 2, 2, 1, 1
5: 1, 1, 1, 2, 2, 2, _, _
Step 6, Solution 8
0: 2, 2, 2, 1, 1, 1, _, _
1: _, _, 2, 1, 1, 1, 2, 2
2: 1, 2, 2, 1, 1, _, _, 2
3: 1, _, _, 1, 1, 2, 2, 2
4: 1, 1, 1, _, _, 2, 2, 2
5: 1, 1, 1, 2, 2, 2, _, _
Nb Fails = 10145
Nb Choice Points = 16137
Heap Size = 3072
Elapsed Time = 0.063874 s
Sat Jul 18 07:05:17 2020
---------------------------------------------------------------------------
0:空白 1:白 2:黒
/**************************************************************************
* おしどりあそび
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include "iz.h"
//##############################################
#define app4
//##############################################
/**************************************************************************/
#ifdef app0
#define DIM 8
#define STP 5
/* 初期状態 */
// 0 1 2 3 4 5 6 7
int init_state[DIM] = { 1, 2, 1, 2, 1, 2, 0, 0};
/* ゴール */
int final_state[DIM] = { 1, 1, 1, 2, 2, 2, 0, 0};
#endif
/**************************************************************************/
#ifdef app1
#define DIM 8
#define STP 6
/* 初期状態 */
// 0 1 2 3 4 5 6 7
int init_state[DIM] = { 0, 0, 1, 2, 1, 2, 1, 2};
/* ゴール */
int final_state[DIM] = { 1, 1, 1, 2, 2, 2, 0, 0};
#endif
/**************************************************************************/
#ifdef app2
#define DIM 8
#define STP 5
/* 初期状態 */
// 0 1 2 3 4 5 6 7
int init_state[DIM] = { 0, 0, 1, 1, 1, 2, 2, 2};
/* ゴール */
int final_state[DIM] = { 1, 1, 1, 2, 2, 2, 0, 0};
#endif
/**************************************************************************/
#ifdef app4
#define DIM 8
#define STP 6
/* 初期状態 */
// 0 1 2 3 4 5 6 7
int init_state[DIM] = { 2, 2, 2, 1, 1, 1, 0, 0};
/* ゴール */
int final_state[DIM] = { 1, 1, 1, 2, 2, 2, 0, 0};
#endif
/**************************************************************************/
#ifdef app3
#define DIM 8
#define STP 4
/* 初期状態 */
// 0 1 2 3 4 5 6 7
int init_state[DIM] = { 1, 2, 2, 0, 0, 1, 1, 2};
/* ゴール */
int final_state[DIM] = { 2, 2, 2, 1, 1, 1, 0, 0};
#endif
/**************************************************************************/
CSint **QR;
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i, j;
char str_char[4] = "_12";
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
for(i = 0; i < STP; i++){
printf("%3d: ", i);
for(j = 0; j < DIM; j++){
printf("%2c%1c", str_char[cs_getValue(QR[DIM * i + j])], (j + 1) % DIM == 0 ? ' ' : ',');
}
putchar('\n');
}
}
/**************************************************************************/
/**************************************************************************/
/**************************************************************************/
int main(int argc, char **argv) {
CSint **diff_elmt;
CSint **pare_check;
int i, j;
clock_t t0 = clock();
time_t nowtime;
cs_init();
time(&nowtime); printf("%s", ctime(&nowtime));
QR = (CSint **)malloc(DIM * STP * sizeof(CSint *));
diff_elmt = (CSint **)malloc(DIM * STP * sizeof(CSint *));
pare_check = (CSint **)malloc(DIM * STP * sizeof(CSint *));
CSint **same_QR = (CSint **)malloc(DIM * STP*STP/2 * sizeof(CSint *));
for(i = 0; i < DIM * STP; i++){
QR[i] = cs_createCSint(0, 2);
}
for(i = 0; i < DIM; i++){
cs_EQ(QR[DIM * 0 + i], init_state[i]);
cs_EQ(QR[DIM * (STP -1) + i], final_state[i]);
}
for(i = 0; i < STP - 1; i++){
for(j = 0; j < DIM; j++){
diff_elmt[DIM * i + j] = cs_ReifNeq(QR[DIM * i + j], QR[DIM * (i + 1) + j]);
}
}
for(i = 0; i < STP - 1; i++){
cs_EQ(cs_Sigma(&diff_elmt[DIM * i], DIM), 4);
}
for(i = 0; i < STP - 1; i++){
for(j = 0; j < DIM; j++){
cs_IfNeq(QR[DIM * i + j], QR[DIM * (i + 1) + j], 0, 0);
}
}
for(i = 0; i < STP; i++){
for(j = 0; j < DIM - 1; j++){
pare_check[DIM * i + j] = cs_ReifEQ(cs_Sigma(&QR[DIM * i + j], 2), 0);
}
cs_EQ(cs_Sigma(&pare_check[DIM * i], DIM - 1), 1);
}
for(i = 0; i < STP - 1; i++){
CSint *space_loc_c = cs_Index(&pare_check[DIM * (i + 0)], DIM - 1, 1);
CSint *space_loc_n = cs_Index(&pare_check[DIM * (i + 1)], DIM - 1, 1);
cs_Eq(cs_VarElement(space_loc_c, &QR[DIM * (i + 1)], DIM),
cs_VarElement(space_loc_n, &QR[DIM * (i + 0)], DIM));
cs_Eq(cs_VarElement(cs_Add(space_loc_c, CSINT(1)), &QR[DIM * (i + 1)], DIM),
cs_VarElement(cs_Add(space_loc_n, CSINT(1)), &QR[DIM * (i + 0)], DIM));
}
for(i = 0; i < STP; i++){
cs_OccurConstraints(CSINT(2), 0, &QR[DIM * i], DIM);
cs_OccurConstraints(CSINT(3), 1, &QR[DIM * i], DIM);
cs_OccurConstraints(CSINT(3), 2, &QR[DIM * i], DIM);
}
int n = 0;
for (i = 0; i < STP - 1; i++){
for (j = i + 1; j < STP; j++){
for (int k = 0; k < DIM; k++){
same_QR[DIM * n + k] = cs_ReifEq(QR[DIM * i + k], QR[DIM * j + k]);
}
cs_NEQ(cs_OccurDomain(0, &same_QR[DIM * n++], DIM), 0);
}
}
cs_printf("%A\n", QR, DIM * STP);
cs_findAll(&QR[0], DIM * STP, cs_findFreeVarNbConstraints, 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;
}
