覆面算を制約論理プログラム iZ-Cを使って解きます。

覆面算を制約論理プログラム iZ-Cを使って解きます。
-------------------------------------------------------------------------------------
iZ-Cチュートリアルにある覆面算を短く改編しました。積和演算cs_ScalProdで自動変数が
無効になることに気づかず時間がかかりました。
./mult
-------------------- ./mult --------------------
Solution 1
179
* 224
-----
716
358
358
-----
40096
-------------------------------------------------------------------------------------
#include <stdio.h>
#include <stdlib.h>
#include <time.h>
#include "iz.h"

/****************************************************************************/
#define NB_DIGITS 20
CSint **Digit;
CSint *L1, *L2, *L3, *L4, *L5, *L6;

CSint *L[7];
/****************************************************************************/
void constraints()
{
/* 0, 1, 2, 3, 4, 5, 6, 7, 8, 9,10,11,12,13,14,15,16,17,18,19, */
enum {a = 0, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t};
static int ORDER[3] = {100, 10, 1};
static int ORDER5[5] = {10000, 1000, 100, 10, 1};
static int REV_ORDER[3] = {1, 10, 100};
/***********************/
/* A B C (L1) */
/* * D E F (L2) */
/* --------- */
/* G H I (L3) */
/* J K L (L4) */
/* M N O (L5) */
/* ---------- */
/* P Q R S T (L6) */
/***********************/

int val, ii;

Digit = cs_createCSintArray(NB_DIGITS, 0, 9);
/*
L1 = cs_ScalProd(&Digit[a], &ORDER[0], 3);
L2 = cs_ScalProd(&Digit[d], &ORDER[0], 3);
L3 = cs_ScalProd(&Digit[g], &ORDER[0], 3);
L4 = cs_ScalProd(&Digit[j], &ORDER[0], 3);
L5 = cs_ScalProd(&Digit[m], &ORDER[0], 3);
L6 = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);
*/
for(ii = 0; ii < 6; ii++){
L[ii + 1] = cs_ScalProd(&Digit[3 * ii], &ORDER[0], 3);
}
// L[6] = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);
L[6] = cs_ScalProd(&Digit[p], &ORDER5[0], 5);
//exit(1);

/*
cs_Eq(L6, cs_Mul(L1, L2));
cs_Eq(L3, cs_Mul(Digit[f], L1));
cs_Eq(L4, cs_Mul(Digit[e], L1));
cs_Eq(L5, cs_Mul(Digit[d], L1));
cs_Eq(L6, cs_VScalProd(3, L5, L4, L3, 100, 10, 1));
*/
cs_Eq(L[6], cs_Mul(L[1], L[2]));
cs_Eq(L[3], cs_Mul(Digit[f], L[1]));
cs_Eq(L[4], cs_Mul(Digit[e], L[1]));
cs_Eq(L[5], cs_Mul(Digit[d], L[1]));
// cs_Eq(L[6], cs_VScalProd(3, L[5], L[4], L[3], 100, 10, 1));
cs_Eq(L[6], cs_ScalProd(&L[3], &REV_ORDER[0], 3));

/* cs_Eq(L6, cs_Mul(L1, L2));*/

/*
cs_NEQ(Digit[a], 0);
cs_NEQ(Digit[d], 0);
cs_NEQ(Digit[g], 0);
cs_NEQ(Digit[j], 0);
cs_NEQ(Digit[m], 0);
cs_NEQ(Digit[p], 0);
*/
for(ii = 0; ii < 6; ii++){
cs_NEQ(Digit[3 * ii], 0);
}

for (val = 0; val <= 9 ; val++){
cs_OccurConstraints(CSINT(2), val, Digit, NB_DIGITS);
}
}

/****************************************************************************/
void constraints1()
{
enum {a = 0, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t};
/***********************/
/* A B C (L1) */
/* * D E F (L2) */
/* --------- */
/* G H I (L3) */
/* J K L (L4) */
/* M N O (L5) */
/* ---------- */
/* P Q R S T (L6) */
/***********************/

int val;

Digit = cs_createCSintArray(NB_DIGITS, 0, 9);
L1 = cs_VScalProd(3, Digit[a], Digit[b], Digit[c], 100, 10, 1);
L2 = cs_VScalProd(3, Digit[d], Digit[e], Digit[f], 100, 10, 1);
L3 = cs_VScalProd(3, Digit[g], Digit[h], Digit[i], 100, 10, 1);
L4 = cs_VScalProd(3, Digit[j], Digit[k], Digit[l], 100, 10, 1);
L5 = cs_VScalProd(3, Digit[m], Digit[n], Digit[o], 100, 10, 1);
L6 = cs_VScalProd(5, Digit[p], Digit[q], Digit[r], Digit[s], Digit[t], 10000, 1000, 100, 10, 1);

cs_Eq(L6, cs_Mul(L1, L2));

cs_Eq(L3, cs_Mul(Digit[f], L1));
cs_Eq(L4, cs_Mul(Digit[e], L1));
cs_Eq(L5, cs_Mul(Digit[d], L1));
cs_Eq(L6, cs_VScalProd(3, L5, L4, L3, 100, 10, 1));
/* cs_Eq(L6, cs_Mul(L1, L2));*/

cs_NEQ(Digit[a], 0);
cs_NEQ(Digit[d], 0);
cs_NEQ(Digit[g], 0);
cs_NEQ(Digit[j], 0);
cs_NEQ(Digit[m], 0);
cs_NEQ(Digit[p], 0);

for (val = 0; val <= 9 ; val++)
cs_OccurConstraints(CSINT(2), val, Digit, NB_DIGITS);
}

/****************************************************************************/
void printSolution(CSint **allvars, int nbVars)
{
static int NbSolutions = 0;
printf("Solution %4d\n", ++NbSolutions);

cs_printf(" %D\n", L[1]);
cs_printf("* %D\n", L[2]);
cs_printf("-----\n");
cs_printf(" %D\n", L[3]);
cs_printf(" %D \n", L[4]);
cs_printf("%D \n", L[5]);
cs_printf("-----\n");
cs_printf("%D \n", L[6]);
}

/****************************************************************************/
/****************************************************************************/
int main(int argc, char **argv)
{
clock_t t0 = clock();

printf("\n-------------------- %s --------------------\n", argv[0]);
cs_init();

constraints();
//constraints1();
cs_findAll(Digit, NB_DIGITS, cs_findFreeVarNbElements, printSolution);
// cs_search(Digit, NB_DIGITS, cs_findFreeVarNbElements);
// printSolution(Digit, NB_DIGITS);

cs_printStats();
cs_end();
printf("Elapsed Time = %fs\n", (double) (clock() - t0) / CLOCKS_PER_SEC);

return 0;
}