制約論理プログラム iZ-C の導入
iZ-Cの導入
はじめに
iZ-Cは制約論理プログラムと呼ばれる問題解決プログラムソルバーです。
形式的にはC言語でプログラムしますが問題解決手法は全く違い、問題の
関係性を制約変数、制約式によって記述し問題を解きます。組み合わせの答えを
見つけると言っていいと思います。私はコンピュータでパズル問題を解くのに
論理制約がぴったりはまることがあるので重宝しています。当然、組み合わせ
爆発で限界点がきます。
はじめて目にする方はきっとポインタの多用やAPIの呼び出しで驚かれると
思います。独習は過去の知識、経験での手続き型言語が邪魔して難しいかも
知れません。
とにかく制約式にIF文がないので論理式で問題を表すのが難しいです。
iZ-Cの論理式で制約を表す時に大切なヒント
AならばBであるを次のように変形します。
Aが真 ならば Bが真である。
(Aが0 または Bが1) でなければフェイルします。
cs_NEQ(cs_Add(cs_ReifNEQ(A, 1), cs_ReifEQ(B, 1)), 0);
ところで私はNTTデータさんとは全く関係ありません。
ダウンロード／ドキュメント
「iZ-C NTTデータ」で検索して
(株)NTTデータセキスイシステムズ提供のC版の制約プログラミングライブラリ。
を見つけて下さい。ドキュメントも豊富です。
私の場合Linux Fedora32 64bitを使っていますがライブラリのキャッシュを
しないとエラーになりました。
ldconfig izC_v3_6_1_linux64/libへのパス
例題の参考にしているHP
「M.Hiroi's Home Page」パズルの参考にしています。
私が思う初心者がよく使うAPIをiZ-Cレファレンスマニュアルから抜き出します。
2.1 開始と終了
void cs_init(void)
void cs_end(void)
3.1 コンストラクタ
CSint *cs_createCSint(int min, int max)
CSint *CSINT(int n)
CSint **cs_createCSintArray(int nbVars, int min, int max)
3.2 領域変数の情報にアクセスするための関数
int cs_getMin(CSint *vint)
int cs_getMax(CSint *vint)
int *cs_getDomain(CSint *vint)
int cs_getValue(CSint *vint)
void cs_printf(const char *control, ...)
3.3 領域に関する制約
IZBOOL cs_InArray(CSint *vint, int *array, int size)
IZBOOL cs_NotInArray(CSint *vint, int *array, int size)
IZBOOL cs_InInterval(CSint *vint, int min, int max)
IZBOOL cs_NotInInterval(CSint *vint, int min, int max)
4.算術制約
CSint *cs_Add(CSint *vint1, CSint *vint2)
CSint *cs_VAdd(int nbVars, CSint *vint, ...)
CSint *cs_Sub(CSint *vint1, CSint *vint2)
CSint *cs_VSub(int nbVars, CSint *vint, ...)
CSint *cs_Mul(CSint *vint1, CSint *vint2)
CSint *cs_VMul(int nbVars, CSint *vint, ...)
CSint *cs_Sigma(CSint **array, int size)
CSint *cs_ScalProd(CSint **array, int *vector, int size)
CSint *cs_VScalProd(int nbVars, CSint *vint, ...)
CSint *cs_Abs(CSint *vint)
5.関係制約
IZBOOL cs_Le(CSint *vint1, CSint *vint2)
IZBOOL cs_Ge(CSint *vint1, CSint *vint2)
IZBOOL cs_Lt(CSint *vint1, CSint *vint2)
IZBOOL cs_Gt(CSint *vint1, CSint *vint2)
IZBOOL cs_Eq(CSint *vint1, CSint *vint2)
IZBOOL cs_Neq(CSint *vint1, CSint *vint2)
IZBOOL cs_LE(CSint *vint, int val)
IZBOOL cs_GE(CSint *vint, int val)
IZBOOL cs_LT(CSint *vint, int val)
IZBOOL cs_GT(CSint *vint, int val)
IZBOOL cs_EQ(CSint *vint, int val)
IZBOOL cs_NEQ(CSint *vint, int val)
IZBOOL cs_AllNeq(CSint **array, int size)
CSInt* cs_ReifLe(CSint *vint1, CSint *vint2)
CSInt* cs_ReifGe(CSint *vint1, CSint *vint2)
CSInt* cs_ReifLt(CSint *vint1, CSint *vint2)
CSInt* cs_ReifGt(CSint *vint1, CSint *vint2)
CSInt* cs_ReifEq(CSint *vint1, CSint *vint2)
CSInt* cs_ReifNeq(CSint *vint1, CSint *vint2)
CSint* cs_ReifLE(CSint *vint, int val)
CSint* cs_ReifGE(CSint *vint, int val)
CSint* cs_ReifLT(CSint *vint, int val)
CSint* cs_ReifGT(CSint *vint, int val)
CSint* cs_ReifEQ(CSint *vint, int val)
CSint* cs_ReifNEQ(CSint *vint, int val)
6.高水準制約
IZBOOL cs_IfEq(CSint *vint1, CSint *vint2, int val1, int val2)
vint1 vint2が指定のval1 val2を持つことが出来なければファイルします。
IZBOOL cs_IfNeq(CSint *vint1, CSint *vint2, int val1, int val2)
vint1 vint2が指定のval1 val2を持つならばファイルします。
CSint *cs_OccurDomain(int val, CSint **array, int size)
IZBOOL cs_OccurConstraints(CSint *vint, int val, CSint **array, int size)
CSint *cs_Index(CSint **array, int size, int val)
CSint *cs_Element(CSint *index, int *values, int size)
CSint *cs_VarElement(CSint *index, CSint **array, int size)
選ばれた領域変数に制約を掛けると元の領域変数に制約が及びます。
CSint *cs_Min(CSint **array, int size)
CSint *cs_VMin(int nbVars, CSint *vint, ...)
CSint *cs_Max(CSint **array, int size)
CSint *cs_VMax(int nbVars, CSint *vint, ...)
7.1 基本的な解探索
IZBOOL cs_search(CSint **allvars, int nbVars, CSint* (*findFreeVar)(CSint **allvars, int nbVars))
IZBOOL cs_Vsearch(int nbVars, CSint *vint, ...)
7.2 組み込みの選択関数
CSint *cs_findFreeVar(CSint **allvars, int nbVars)
CSint *cs_findFreeVarNbElements(CSint **allvars, int nbVars)
CSint *cs_findFreeVarNbElementsMin(CSint **allvars, int nbVars)
CSint *cs_findFreeVarNbConstraints(CSint **allvars, int nbVars)
IZBOOL cs_findAll(CSint **allvars, int nbVars, CSint* (*findFreeVar)(CSint **allvars, int nbVars), void(*found)(CSint **allvars, int nbVars))
IZBOOL cs_minimize(CSint **allvars, int nbVars, CSint* (*findFreeVar)(CSint **allvars, int nbVars), CSint *cost, void (*found)(CSint **allvars, int nbVars, CSint *cost))
8.デモン
IZBOOL cs_eventAllKnown(CSint **array, int size, IZBOOL (*allKnown)(CSint **array, int size, void *extra), void *extra)
IZBOOL cs_eventKnown(CSint **array, int size, IZBOOL (*known)(int val, int index, CSint **array, int size, void *extra), void *extra)
レファレンスマニュアルの抜き出しは以上です。
ここで応用プログラム例を一つ載せておきます。
「M.Hiroi's Home Page」 裏表パズル
ルービックキューブの平面版
---------------------------------------------------------------------------
make && time ./ura_omote 0 3 1 0 1 0 0 0 0 0 0 5
Fri Jul 10 13:47:42 2020
OPR:{0..5}, {0..5}, {0..5}, {0..5}
Step 5, Solution 1
0 : 0 :1, 0, 1, 0, 0, 0, 0, 0, 0
1 : 3 :0, 1, 0, 0, 0, 0, 0, 0, 0
2 : 0 :1, 1, 0, 1, 0, 0, 1, 0, 0
3 : 3 :1, 0, 0, 1, 0, 0, 1, 0, 0
4 : :0, 0, 0, 0, 0, 0, 0, 0, 0
Step 5, Solution 2
0 : 0 :1, 0, 1, 0, 0, 0, 0, 0, 0
1 : 5 :0, 1, 0, 0, 0, 0, 0, 0, 0
2 : 0 :0, 1, 1, 0, 0, 1, 0, 0, 1
3 : 5 :0, 0, 1, 0, 0, 1, 0, 0, 1
4 : :0, 0, 0, 0, 0, 0, 0, 0, 0
Nb Fails = 529
Nb Choice Points = 651
Heap Size = 1024
Elapsed Time = 0.001471 s
Fri Jul 10 13:47:42 2020
real 0m0.002s
user 0m0.001s
sys 0m0.001s
---------------------------------------------------------------------------
make && time ./ura_omote 1 3 1 0 1 0 0 0 0 0 0 5
Step 5, Solution 1
( 0 ): 0
1, 0, 1
0, 0, 0
0, 0, 0
( 1 ): 3
0, 1, 0
0, 0, 0
0, 0, 0
( 2 ): 0
1, 1, 0
1, 0, 0
1, 0, 0
( 3 ): 3
1, 0, 0
1, 0, 0
1, 0, 0
( 4 ):
0, 0, 0
0, 0, 0
0, 0, 0
Step 5, Solution 2
( 0 ): 0
1, 0, 1
0, 0, 0
0, 0, 0
( 1 ): 5
0, 1, 0
0, 0, 0
0, 0, 0
( 2 ): 0
0, 1, 1
0, 0, 1
0, 0, 1
( 3 ): 5
0, 0, 1
0, 0, 1
0, 0, 1
( 4 ):
0, 0, 0
0, 0, 0
0, 0, 0
Nb Fails = 529
Nb Choice Points = 651
Heap Size = 1024
Elapsed Time = 0.001505 s
Fri Jul 10 13:49:02 2020
real 0m0.002s
user 0m0.001s
sys 0m0.001s
---------------------------------------------------------------------------
/**************************************************************************
* 裏表パズル
* SAMPLE 3: 0 1 0 1 1 0 0 0 0 : 8 PATTERN
* SAMPLE 4: 4 0 0 0 0 0 0 1 1 0 0 1 1 1 0 0 1 :7 PATTERN
* SAMPLE 5: 0 0 1 0 0 0 0 1 0 0 1 1 1 0 0 0 0 0 0 0 0 0 0 0 0 : 14 PATTERN
* SAMPLE 5: 1 1 0 1 1 1 1 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 : 9 PATTERN
* SAMPLE 5: 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 : 7 PATTERN
**************************************************************************/
#include <stdlib.h>
#include <time.h>
#include <limits.h>
#include <string.h>
#include "iz.h"
int DIM, STP;
CSint **QR, **TQR, **OPR;
int DISP;
/**************************************************************************/
/**************************************************************************/
IZBOOL knownOPR(int val, int index, CSint **allvars, int size, void *extra) {
int i, j;
int ovf_DIM = val >= DIM ? 1 : 0;
int start_val = val - ovf_DIM * DIM;
CSint **SEL_QR = ovf_DIM ? &TQR[0] : &QR[0];
for(i = 0; i < DIM; i++){
int eq_ival_f = (i == start_val) ? 1 : 0;
for(j = 0; j < DIM; j++){
CSint *dst_QR = SEL_QR[DIM*DIM*(index + 1) + DIM*i + j];
CSint *src_QR = SEL_QR[DIM*DIM*index + DIM*i + eq_ival_f*(DIM-1) + (-2*eq_ival_f + 1)*j];
if(eq_ival_f) {
if(!cs_Neq(dst_QR, src_QR)) return FALSE;
}
else {
if(!cs_Eq(dst_QR, src_QR)) return FALSE;
}
}
}
CSint *QR_FLG[DIM*2];
for(i = 0; i < DIM; i++){
QR_FLG[i] = cs_OccurDomain(1, &QR[DIM*DIM*(index+1) + DIM*i], DIM);
QR_FLG[DIM + i] = cs_OccurDomain(1, &TQR[DIM*DIM*(index+1) + DIM*i], DIM);
}
CSint *NUM_0_DIM[2];
NUM_0_DIM[0] = cs_Add(cs_OccurDomain(0, &QR_FLG[0], DIM), cs_OccurDomain(DIM, &QR_FLG[0], DIM));
NUM_0_DIM[1] = cs_Add(cs_OccurDomain(0, &QR_FLG[DIM], DIM), cs_OccurDomain(DIM, &QR_FLG[DIM], DIM));
// cs_printf("%A", QR_FLG, 2*DIM); cs_printf(" : %A\n", NUM_0_DIM, 2);
for(i = 0; i < DIM; i++){
if*1{
return cs_EQ(OPR[index+1], i);
}
if*2{
return cs_EQ(OPR[index+1], DIM + i);
}
}
return TRUE;
}
/**************************************************************************/
/**************************************************************************/
void printSolution(CSint **allvars, int nbVars) {
static int NbSolutions = 0;
int i, j;
if(DISP == 0) {
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
for(i = 0; i < STP - 1; i++) {
printf("%2d : %2d :", i, cs_getValue(OPR[i]));
cs_printf("%A\n", &QR[DIM*DIM * i], DIM*DIM);
}
printf("%2d : :", STP - 1);
cs_printf("%A\n", &QR[DIM*DIM * (STP - 1)], DIM*DIM);
}
else {
/* top cursol */
// printf("\033[0;0f");
/* clear screen */
// printf("\033[2J\033[0;0f");
printf("\nStep %d, Solution %d\n", STP, ++NbSolutions);
for(i = 0; i < STP - 1; i++){
printf("\n(%2d ): %2d\n", i, cs_getValue(OPR[i]));
for(j = 0; j < DIM; j++){
cs_printf("%A\n", &QR[DIM*DIM*i + DIM*j], DIM);
}
}
printf("\n(%2d ): \n", i);
for(j = 0; j < DIM; j++){
cs_printf("%A\n", &QR[DIM*DIM*(STP - 1) + DIM*j], 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));
DISP = atoi(argv[1]);
DIM = atoi(argv[2]);
STP = atoi(argv[3 + DIM * DIM]);
CSint **dif_comb = (CSint **)malloc(STP * STP /2 *DIM*DIM * sizeof(CSint *));
OPR = (CSint **)malloc*3;
QR = (CSint **)malloc(DIM*DIM * STP * sizeof(CSint *));
TQR = (CSint **)malloc(DIM*DIM * STP * sizeof(CSint *));
/* 初期状態 */
for(i = 0; i < STP - 1; i++){
OPR[i] = cs_createCSint(0, 2*DIM - 1);
}
for(i = 0; i < DIM*DIM * STP; i++){
QR[i] = cs_createCSint(0, 1);
}
for(i = 0; i < DIM*DIM; i++){
QR[i] = CSINT(atoi(argv[3 + i]));
}
for(int k = 0; k < STP; k++){
for(i = 0; i < DIM; i++){
for(j = 0; j < DIM; j++){
TQR[DIM*DIM*k + DIM*i + j] = QR[DIM*DIM*k + DIM*j + i];
}
}
}
/* ゴール */
cs_EQ(cs_Sigma(&QR[DIM*DIM*(STP-1)], DIM*DIM), 0);
for(i = 0; i < STP - 2; i++){
CSint *Neq_OPR_C_N = cs_ReifNeq(cs_ReifGE(OPR[i], DIM), cs_ReifGE(OPR[i + 1], DIM));
cs_NEQ(cs_Add(Neq_OPR_C_N, cs_ReifGt(OPR[i+1], OPR[i])), 0);
}
int nn = 0;
for (i = 0; i < STP - 1; i++){
for (j = i + 1; j < STP; j++){
for (int k = 0; k < DIM*DIM; k++){
dif_comb[DIM*DIM * nn + k] = cs_ReifEq(QR[DIM*DIM * i + k], QR[DIM*DIM * j + k]);
}
cs_NEQ(cs_Sigma(&dif_comb[DIM*DIM * nn++], DIM*DIM), DIM*DIM);
}
}
cs_printf("OPR:%A\n", OPR, STP - 1);
/*
cs_printf("QR:%A\n", QR, DIM*DIM * STP);
cs_printf("diff_QR:%A\n", diff_QR, DIM*DIM * (STP - 1));
*/
if(DISP == 1) printf("\033[2J\033[0;0f"); /* clear screen */
cs_eventKnown(&OPR[0], STP - 1, knownOPR, NULL);
// cs_findAll(&QR[0], DIM*DIM * STP, cs_findFreeVarNbConstraints, printSolution);
//// cs_findAll(&QR[0], DIM*DIM * STP, cs_findFreeVarNbElementsMin, printSolution);
cs_findAll(&OPR[0], STP - 1, cs_findFreeVarNbElements, printSolution);
// cs_findAll(&QR[0], DIM*DIM * 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;
}
ソースコードは以上です。
