#include <iostream>
#include <bdd.h>

using namespace std;

#define N 9
#define M 4
#define LOG_N 4
#define N_VAR M*N*LOG_N
#define K 19

#define COL_N 3

typedef const bdd (&property)[N][N];

// n1 = 2
// n2 = 4
// n3 = 5
// n4 = 4

bdd bound_2(property p1, int v1, property p2, int v2)
{
    bdd res = bddtrue;
    for (int i = 0; i < N; ++i)
    {
        res &= !(p1[i][v1] ^ p2[i][v2]);
    }
    return res;
}

// Рассматривается правый сосед (объект расположенный справа сверху)
bdd bound_3_right_up(property p, int v, property p_n, int v_n)
{
    bdd res = bddtrue;

    int step = COL_N - 1;

    for (int i = 0; i < N; ++i)
    {
        // Элементы первого столбца или нижней строки
        // не могут быть соседями справа
        if (i % COL_N == 0 || i + COL_N >= N)
            res &= !p_n[i][v_n];

        // Элементы первой строки или последнего столбца
        // не могут иметь соседа справа
        if (i < COL_N || i % COL_N == COL_N - 1)
            res &= !p[i][v];

        if (i >= COL_N && i % COL_N < COL_N - 1)
            res &= !(p[i][v] ^ p_n[i-step][v_n]);
    }

    return res;
}

// Рассматривается левый сосед (объект расположенный слева сверху)
bdd bound_3_left_up(property p, int v, property p_n, int v_n)
{
    bdd res = bddtrue;

    int step = COL_N + 1;

    for (int i = 0; i < N; ++i)
    {
        // Элементы последнего столбца или нижней строки
        // не могут быть соседями слева
        if (i % COL_N == COL_N - 1 || i + COL_N >= N)
            res &= !p_n[i][v_n];

        // Элементы первой строки или первого столбца
        // не могут иметь соседа слева
        if (i < COL_N || i % COL_N == 0)
            res &= !p[i][v];

        if (i >= COL_N && i % COL_N > 0)
            res &= !(p[i][v] ^ p_n[i-step][v_n]);
    }

    return res;
}

bdd bound_4(property p, int v, property p_n, int v_n)
{
    bdd temp1 = bound_3_left_up (p, v, p_n, v_n);
    bdd temp2 = bound_3_right_up(p, v, p_n, v_n);
    return temp1 | temp2;
}

ostream& out = cout;

void fun(char* varset, int size);

int main()
{
    bdd_init(10000000, 1000000);

    bdd_setvarnum(N_VAR);

    bdd p[M][N][N];

    unsigned I = 0;
    for (unsigned i = 0; i < N; i++)
    {
        for (unsigned j = 0; j < N; j++)
        {
            for (int m = 0; m < M; m++)
            {
                p[m][i][j] = bddtrue;
                for (unsigned k = 0; k < LOG_N; k++) p[m][i][j] &= ((j >> k) & 1) ? bdd_ithvar(I + LOG_N * m + k) : bdd_nithvar(I + LOG_N * m + k);
            }
        }
        I += LOG_N*M;
    }

    bdd task = bddtrue;

    // Ограничение 6:
    for (unsigned i = 0; i < N; i++)
    {
        bdd temp[M];
        for (int m = 0; m < M; m++)
            temp[m] = bddfalse;
        for (unsigned j = 0; j < N; j++)
            for (int m = 0; m < M; m++)
                temp[m] |= p[m][i][j];
        for (int m = 0; m < M; m++)
            task &= temp[m];
    }


    // Ограничение 1:
    task &= p[0][0][0];
    task &= p[0][1][1];

    task &= p[1][4][5];
    task &= p[0][6][6];



    // Ограничение 2:
    task &= bound_2(p[0], 4, p[3], 7);
    task &= bound_2(p[0], 6, p[1], 7);
    task &= bound_2(p[2], 4, p[3], 5);
    task &= bound_2(p[0], 0, p[1], 1);



    // Ограничение 3:
    task &= bound_3_right_up(p[0], 3, p[0], 1);
    task &= bound_3_right_up(p[1], 4, p[1], 2);
    task &= bound_3_left_up (p[2], 7, p[3], 4);
    task &= bound_3_left_up (p[0], 8, p[3], 7);
    task &= bound_3_left_up (p[3], 2, p[3], 7);



    // Ограничение 4:
    task &= bound_4(p[0], 4, p[0], 0);
    task &= bound_4(p[1], 5, p[2], 4);
    task &= bound_4(p[0], 7, p[3], 8);
    task &= bound_4(p[1], 8, p[1], 4);



    // Ограничение 7:
    for (int i = 0; i < N; ++i)
    {
        if (i % 2 == 0)
        {
            bdd temp = bddfalse;
            for (int j1 = 0; j1 < N; ++j1)
            {
                for (int j2 = 0; j2 < N; ++j2)
                    for (int j3 = 0; j3 < N; ++j3)
                        for (int j4 = 0; j4 < N; ++j4)
                            if (j1 + j2 + j3 + j4 <= K)
                                temp |= (p[0][i][j1] & p[1][i][j2] & p[2][i][j3] & p[3][i][j4]);
            }
            task &= temp;
        }
    }



    // Ограничение 5:
    for (unsigned j = 0; j < N; j++)
        for (unsigned i = 0; i < N - 1; i++)
            for (unsigned k = i + 1; k < N; k++)
            {
                cout << j << " " << i << " " << k << endl;
                for (unsigned m = 0; m < M; m++)
                    task &= p[m][i][j] >> !p[m][k][j];
            }


    unsigned satcount = (unsigned)bdd_satcount(task);
    out<<satcount<<" solutions:\n"<<endl;
    if (satcount)
        bdd_allsat(task, fun);

    bdd_done();

    getchar();

    return 0;
}


char var[N_VAR];

void print(void)
{
    for (unsigned i = 0; i < N; i++)
    {
        out<<i<<": ";
        for (unsigned j = 0; j < N; j++)
        {
            unsigned J = i*N*LOG_N + j*LOG_N;
            unsigned num = 0;
            for (unsigned k = 0; k < LOG_N; k++) num += (unsigned)(var[J + k] << k);
            out<<num<<' ';
        }
        out<<endl;
    }
    out<<endl;
}

void build(char* varset, unsigned n, unsigned I)
{
    if (I == n - 1)
    {
        if (varset[I] >= 0)
        {
            var[I] = varset[I];
            print();
            return;
        }
        var[I] = 0;
        print();
        var[I] = 1;
        print();
        return;
    }
    if (varset[I] >= 0)
    {
        var[I] = varset[I];
        build(varset, n, I + 1);
        return;
    }
    var[I] = 0;
    build(varset, n, I + 1);
    var[I] = 1;
    build(varset, n, I + 1);
}

void fun(char* varset, int size)
{
    build(varset, size, 0);
}