sunasunaxの日記

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

隣接行列から到達可能経路と距離を制約論理プログラム 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;
}