// SatSolver.cpp : This file contains the 'main' function. Program execution begins and ends there.
//

#include "pch.h"
#include <array>
#include <vector>
#include <bitset>
#include <fstream>

using namespace  std;

const auto ROWS = 4;
const auto COLUMNS = 4;
const auto O = false;
const auto X = true;
const bool CONFIGURATION[ROWS][COLUMNS] = {
    {X, O, O, O},
    {O, X, X, X},
    {O, X, X, O},
    {X, O, X, O}
};

const size_t VAR_NUM = 9;

constexpr auto numberOfSetBits(uint32_t i) {
    i = i - ((i >> 1) & 0x55555555);
    i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
    return (((i + (i >> 4)) & 0x0F0F0F0F) * 0x01010101) >> 24;
}

constexpr auto assembleMask(const uint8_t params, const bool e) {
    return ~(uint32_t(params & 0xF0) << 1 | (params & 0xF) | e << 4);
}

//делаем шаг вперёд
std::vector<std::vector<int>> run1step(std::vector<std::vector<int>> ar)
{
    int xlen = ar.size();
    int ylen = ar[0].size();
    std::vector<std::vector<int>> result(xlen);
    for (int i = 0; i < xlen; i++)
    {
        result[i] = vector<int>(ylen);
    }
    for (int x = 0; x < xlen; x++)
    {
        for (int y = 0; y < ylen; y++)
        {
            bool isleft = (y == 0);
            bool isright = (y == ylen - 1);
            bool isup = (x == 0);
            bool isdown = (x == xlen - 1);

            int ncount = (isleft ? 0 : ar[x][y - 1]) +
                (isleft || isup ? 0 : ar[x - 1][y - 1]) +
                (isup ? 0 : ar[x - 1][y]) +
                (isup || isright ? 0 : ar[x - 1][y + 1]) +
                (isright ? 0 : ar[x][y + 1]) +
                (isright || isdown ? 0 : ar[x + 1][y + 1]) +
                (isdown ? 0 : ar[x + 1][y]) +
                (isdown || isleft ? 0 : ar[x + 1][y - 1]);

            result[x][y] = ((ncount == 3 || (ar[x][y] == 1 && ncount == 2)) ? 1 : 0);
        }
    }
    return result;
}

//увеличиваем поле на одну клетку по краям
std::vector<std::vector<int>> lor(std::bitset<VAR_NUM> addpat)
{
    vector<vector<int>> result(5);
    for (int i = 0; i < 5; i++)
    {
        result[i] = vector<int>(5);
    }
    int count = 0;

    for (int x = 0; x < 5; x++)
    {
        for (int y = 0; y < 5; y++)
        {
            if (1 <= x && x < 4 && 1 <= y && y < 4)
            {
                result[x][y] = addpat[count++];
            }
            else
            {
                result[x][y] = 0;
            }
        }
    }
    return result;
}

//проверяем на удовлетворение условий
bool check(int y, int x, vector<vector<int>> runF)
{
    int goalWidth = COLUMNS;
    int goalHeight = ROWS;
    if (x == 0 && y == 0)
    {
        if (runF[0][0] == 0 && runF[1][0] == 0 && runF[2][0] == 0 && runF[0][1] == 0 && runF[1][1] == 0 && runF[2][1] == 0
            && runF[0][2] == 0 && runF[1][2] == 0)
        {
            return true;
        }
    }
    if (y == 0)
    {
        if (x == goalWidth - 1)
        {
            if (runF[2][0] == 0 && runF[3][0] == 0 && runF[4][0] == 0 && runF[2][1] == 0 && runF[3][1] == 0 && runF[4][1] == 0 &&
                runF[3][2] == 0 && runF[4][2] == 0)
            {
                return true;
            }
        }
        else
        {
            if (runF[2][0] == 0 && runF[2][1] == 0)
            {
                return true;
            }
        }
    }
    else if (y == goalHeight - 1)
    {
        if (x == 0)
        {
            if (runF[0][2] == 0 && runF[1][2] == 0 && runF[0][3] == 0 && runF[1][3] == 0 && runF[2][3] == 0 && runF[0][4] == 0 &&
                runF[1][4] == 0 && runF[2][4] == 0)
            {
                return true;
            }
        }
        else if (x == goalWidth - 1)
        {
            if (runF[3][2] == 0 && runF[4][2] == 0 && runF[2][3] == 0 && runF[3][3] == 0 && runF[4][3] == 0 && runF[2][4] == 0 &&
                runF[3][4] == 0 && runF[4][4] == 0)
            {
                return true;
            }
        }
        else
        {
            if (runF[2][3] == 0 && runF[2][4] == 0)
            {
                return true;
            }
        }
    }
    else
    {
        if (x == 0)
        {
            if (runF[0][2] == 0 && runF[1][2] == 0)
            {
                return true;
            }
        }
        else if (x == goalWidth - 1)
        {
            if (runF[3][2] == 0 && runF[4][2] == 0)
            {
                return true;
            }
        }
        else
        {
            return true;
        }
    }
    return false;
}

int main()
{
    auto out = std::ofstream("output.txt");
    auto outDimacs = std::ofstream("dimacs.cnf");

    // строим маски КНФ
    std::vector<std::bitset<VAR_NUM>> cnfMasksLive;
    std::vector<std::bitset<VAR_NUM>> cnfMasksDead;
    for (uint32_t i = 0; i < 1 << 8; i++) {
        const auto sb = numberOfSetBits(i);
        if (sb != 3) {
            cnfMasksLive.emplace_back(assembleMask(i, false));
            if (sb != 2)
                cnfMasksLive.emplace_back(assembleMask(i, true));
            else
                cnfMasksDead.emplace_back(assembleMask(i, true));
        }
        else {
            cnfMasksDead.emplace_back(assembleMask(i, true));
            cnfMasksDead.emplace_back(assembleMask(i, false));
        }
    }

    // пишем КНФ и DIMACS
    const auto liveNum = std::count_if(&CONFIGURATION[0][0], &CONFIGURATION[ROWS - 1][COLUMNS - 1], [](const bool val) { return val; });
    const auto varNum = (ROWS + 2)*(COLUMNS + 2); // пока не считаем
    outDimacs << "p cnf " << varNum << ' ' << cnfMasksLive.size() * liveNum << '\n';
    // КНФ клеток конфигурации
    for (size_t i = 0; i < ROWS; i++)
    {
        for (size_t j = 0; j < COLUMNS; j++)
        {
            const auto & masks = CONFIGURATION[i][j] ? cnfMasksLive : cnfMasksDead;
            for (const auto &mask : masks) {
                auto runF = run1step(lor(mask));
                if (!check(j, i, runF))
                    continue;

                out << '(';
                for (size_t k = 0; k < VAR_NUM; k++) {
                    if (!mask.test(k)) {
                        out << '~';
                        outDimacs << '-';
                    }

                    const int32_t literal = 1 + COLUMNS + 2 + 1 + (i + k / 3 - 1)*(COLUMNS + 2) + (j + k % 3 - 1);
                    outDimacs << literal << " ";
                    out << "x" << literal;
                    if (k != VAR_NUM - 1)
                        out << '|';
                }
                outDimacs << "0\n";
                out << ')';
            }
        }
    }
    // КНФ внешних клеток

    system("pause");
}