DenkiBlocks-WIP2.lua

-- Denki Blocks! Solver WIP2
--
-- usable but too slow, too many clauses and variables right now...
--

USE_WINDOWS = true
USE_LINUX = false
dofile("SAT-solver-framework.lua")
USE_MINISAT = true

-- for a small test.
-- sorry, the more complex puzzles don't work
ROWS = 4
COLUMNS = 4
BITS = 4
LevelLayout = {
"r__r",
"_y_y",
"___b",
"rXb_"
}
ColorsToConnect = {
r = {number=1,r=1,c=1}, y={number=2,r=2,c=2}, b={number=3,r=3,c=4}}
OtherColors = {}
MaximumTurns = 5


--[[
--4x49
LevelLayout = {
"________________",
"______X_________",
"________________",
"________________",
"_yByByBy________",
"_BBBBBBB________",
"_yBy_B__________",
"_BBB_ByByByBy___",
"_yBy_BBBBBBBB_X_",
"_BBB_ByByByBy___",
"_______B________",
"_______B___X____",
"______BBB_______",
"______yBy_______",
"______BBB_______",
"________________"
}
ROWS=16
COLUMNS=16
BITS=7
ColorsToConnect={y={number=1,r=5,c=2}}
OtherColors={B = {number=2,r=0,c=0}}
MaximumTurns=45
--]]

--[[
--7x13
ROWS = 16
COLUMNS = 16
BITS = 5   -- math.ceil( ln(total movable tiles) / ln(2) )

LevelLayout = {
"________________",
"__rr_yyyyyy_bb__",
"__rr________bb__",
"XXXXXXX__XXXXXXX",
"______X__X______",
"__yy__X__X__yy__",
"__yy__X__X__yy__",
"______X__X______",
"_bbbb_X__X_rrrr_",
"______X__X______",
"__yy__X__X__yy__",
"__yy__X__X__yy__",
"______X__X______",
"XX__XXX__XXX__XX",
"________________",
"________________"
}

ColorsToConnect = {
r = {number=1,r=9,c=12}, y = {number=2,r=2,c=9}, b = {number=3,r=9,c=3}}
OtherColors = {}
MaximumTurns = 70
--]]

-- ugly code, but #ColorsToConnect == 0, so we need to count by hand
TotalColors = 0
TotalColorsToConnect = 0
for _,_ in pairs(ColorsToConnect) do
    TotalColors = TotalColors + 1
    TotalColorsToConnect = TotalColorsToConnect + 1
end
for _,_ in pairs(OtherColors) do TotalColors = TotalColors + 1 end

function CheckLayout()
    local found = {}
    for r = 1, ROWS do
        assert(type(LevelLayout[r]) == "string", "type mismatch!")
        assert(string.len(LevelLayout[r]) == COLUMNS, "string does not have the right length!")
        for c = 1, COLUMNS do
            local s = string.sub(LevelLayout[r],c,c)
            assert(
                s == "_"
                or s == "X"
                or ColorsToConnect[ s ] ~= nil
                or OtherColors[ s ] ~= nil,
                "LevelLayout["..r.."]["..c.."] unknown color "..s.."!")
            found[s] = true
        end
    end
    local foundnum = {}
    for key,val in pairs(ColorsToConnect) do
        assert(found[key], "ColorsToConnect includes color "..key.." which is not in the puzzle!")
        foundnum[val.number] = true
    end
    for i = 1, TotalColorsToConnect do
        assert(foundnum[i], "color number "..i.." should exist!")
    end

    for key,val in pairs(OtherColors) do
        assert(found[key], "OtherColors includes color "..key.." which is not in the puzzle!")
        foundnum[val.number] = true
    end
    for i = 1, #OtherColors do
        assert(foundnum[TotalColorsToConnect + i], "color number "..(TotalColorsToConnect+i).." should exist!")
    end
end

function CreateCNF()
    CheckLayout()
    StartAutoWrite(100000)
    --A : Before rotation is done
    --R : which rotation should be done? < --- THIS IS THE ONLY UNRESTRICTED VARIABLE!! ALL INPUT IS DONE HERE!!
    --B : After rotation is done

    --[[
    A[1] : initial state

          R[1]        move!       R[2]        move!
    A[1] -----> B[1] -----> A[2] -----> B[2] ------> ...

    A[n] : state after n-1 finished moves.
    B[n] : check the winning condition in turn n-1, prepare the move

    --]]
    NewVar("A", {
        MaximumTurns + 1,
        ROWS,
        COLUMNS,
        -- which color? zero? free? unmovable?
           TotalColors  + 1   + 1   + 1})

    IS_ZERO = TotalColors + 1
    IS_FREE = TotalColors + 2
    IS_UNMOVABLE = TotalColors + 3
    --assert(#Var.A[1][1][1] == 6, "FAIL"..#Var.A[1][1][1])
    print("parsing layout...")
    -- Let's parse the layout!
    for r = 1, ROWS do for c = 1, COLUMNS do
        local s = string.sub(LevelLayout[r],c,c)
        if s == "_" then
            for entry = 1, #Var.A[1][r][c] do
                AddSimpleClause{Var.A[1][r][c][entry], entry == IS_FREE}
            end
        elseif s == "X" then
            for entry = 1, #Var.A[1][r][c] do
                AddSimpleClause{Var.A[1][r][c][entry], entry == IS_UNMOVABLE}
            end
        else
            local n = 0
            if ColorsToConnect[s] ~= nil then
                n = ColorsToConnect[s]
            else
                n = OtherColors[s]
            end
            assert(n ~= nil, "r="..r..",c="..c..",s="..s..", but n==nil!")
            for entry = 1, #Var.A[1][r][c] do
                if entry == IS_ZERO then
                    AddSimpleClause{Var.A[1][r][c][entry], r==n.r and c==n.c}
                else
                    AddSimpleClause{Var.A[1][r][c][entry], n.number == entry}
                end
            end
        end
    end end

    NewVar("R", {
        MaximumTurns + 1,
        2})

    NewVar("B", {
        MaximumTurns + 1,
        ROWS,
        COLUMNS,
        -- which color? zero? free? unmovable?
           TotalColors  + 1   + 1   + 1

        -- these will be necessary for every single step because of the
        -- possibility to connect multiple colors in the same turn
        --
        -- connected to zero? connection number. right less? down less?
           + 1                + BITS             + BITS      + BITS
        -- blocked? block number. right less? down less?
           + 1      + BITS        + BITS      + BITS})

    print("rotation..."..total_number_of_clauses)
    -- rotation helper function
    local function h(rot1, rot2, r1, c1, r2, c2)
        for t = 1, MaximumTurns + 1 do for entry = 1, #Var.A[1][1][1] do
            AddIfThenClause(
                "if ALL", {Var.R[t][1], rot1, Var.R[t][2], rot2, Var.A[t][r1][c1][entry], true},
                "then ALL", {Var.B[t][r2][c2][entry], true}
            )
            AddIfThenClause(
                "if ALL", {Var.R[t][1], rot1, Var.R[t][2], rot2, Var.A[t][r1][c1][entry], false},
                "then ALL", {Var.B[t][r2][c2][entry], false}
            )
        end end
    end
    for r = 1, ROWS do for c = 1, COLUMNS do
        -- rotate 0 degrees
        h(false, false, r, c, r, c)
        -- 90 degrees right
        h(false, true, r, c, c, ROWS + 1 - r)
        -- 180 degrees right
        h(true, false, r, c, ROWS + 1 - r, COLUMNS + 1 - c)
        -- 270 degrees right
        h(true, true,  r, c, COLUMNS + 1 - c, r)
    end end

    IS_CONNECTED_TO_ZERO = TotalColors + 4
    B_CONNECTION_NUMBER_OFFSET = TotalColors + 4 + 1
    B_CONNECTION_NUMBER_COMPARE_RIGHT_OFFSET = B_CONNECTION_NUMBER_OFFSET + BITS
    B_CONNECTION_NUMBER_COMPARE_DOWN_OFFSET = B_CONNECTION_NUMBER_OFFSET + BITS + BITS
    IS_BLOCKED = TotalColors + 4 + 3*BITS + 1
    B_BLOCK_NUMBER_OFFSET = TotalColors + 4 + 3*BITS + 1 + 1
    B_BLOCK_NUMBER_COMPARE_RIGHT_OFFSET = B_BLOCK_NUMBER_OFFSET + BITS
    B_BLOCK_NUMBER_COMPARE_DOWN_OFFSET  = B_BLOCK_NUMBER_OFFSET + BITS + BITS

    print("compare numbers..."..total_number_of_clauses)
    -- compare number helper function
    local function h(t,r1,c1,r2,c2,number_offset,compare_offset)
        local V1 = Var.B[t][r1][c1]
        local V2 = Var.B[t][r2][c2]

        -- n(V) := 1 * V[number_offset]   +  2 * V[number_offset+1]
        --       + 4 * V[number_offset+2] +  8 * V[number_offset+3]
        --       +16 * V[number_offset+4] + 32 * V[number_offset+5]
        --       +64 * V[number_offset+6] +128 * V[number_offset+7]
        --
        local n = number_offset
        local c = compare_offset

        -- n(V1) > n(V2) ?

        -- least significant bit
        -- for the one-bit numbers a and b, a > b if and only if a == 1, b == 0
        AddIfAndOnlyIfClause("ALL of", {V1[n], true, V2[n], false}, "if and only if", "ALL of", {V1[c], true})

        for b = 1, BITS - 1 do
            -- x + n(V1) > x + n(V2)    <=> n(V1) > n(V2)
            AddIfThenClause("if ALL", {V1[n+b], true, V2[n+b], true,   V1[c+b-1], true}, "then ALL", {V1[c+b], true})
            AddIfThenClause("if ALL", {V1[n+b], true, V2[n+b], true,   V1[c+b-1], false}, "then ALL", {V1[c+b], false})
            AddIfThenClause("if ALL", {V1[n+b], false, V2[n+b], false, V1[c+b-1], true}, "then ALL", {V1[c+b], true})
            AddIfThenClause("if ALL", {V1[n+b], false, V2[n+b], false, V1[c+b-1], false}, "then ALL", {V1[c+b], false})

            -- x + n(V1) > n(V2) if x > n(V2)
            AddIfThenClause("if ALL", {V1[n+b], true, V2[n+b], false}, "then ALL", {V1[c+b], true})
            -- n(V1) <= x + n(V2) if x > n(V1)
            AddIfThenClause("if ALL", {V1[n+b], false, V2[n+b], true}, "then ALL", {V1[c+b], false})
        end
    end
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do for c = 1, COLUMNS - 1 do
        h(t, r, c, r, c+1, B_CONNECTION_NUMBER_OFFSET, B_CONNECTION_NUMBER_COMPARE_RIGHT_OFFSET)
        h(t, r, c, r, c+1, B_BLOCK_NUMBER_OFFSET, B_BLOCK_NUMBER_COMPARE_RIGHT_OFFSET)
    end end end
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS - 1 do for c = 1, COLUMNS do
        h(t, r, c, r+1, c, B_CONNECTION_NUMBER_OFFSET, B_CONNECTION_NUMBER_COMPARE_DOWN_OFFSET)
        h(t, r, c, r+1, c, B_BLOCK_NUMBER_OFFSET, B_BLOCK_NUMBER_COMPARE_DOWN_OFFSET)
    end end end

    for t = 1, MaximumTurns + 1 do r = 1, ROWS do for b = 0, BITS-1 do
        AddSimpleClause{Var.B[t][r][COLUMNS][B_BLOCK_NUMBER_COMPARE_RIGHT_OFFSET + b], false}
    end end end
    for t = 1, MaximumTurns + 1 do c = 1, COLUMNS do for b = 0, BITS-1 do
        AddSimpleClause{Var.B[t][ROWS][c][B_BLOCK_NUMBER_COMPARE_DOWN_OFFSET + b], false}
    end end end

    -- check if the tile to the right has the same color
    NewVar("RSC", {
        MaximumTurns + 1,
        ROWS,
        COLUMNS - 1})

    -- check if the tile to the bottom has the same color
    NewVar("DSC", {
        MaximumTurns + 1,
        ROWS - 1,
        COLUMNS})

    print("check same color..."..total_number_of_clauses)
    local function h(V,t,r1,c1,r2,c2)
        AddIfThenClause(
            "if ALL", {V[t][r1][c1], true},
            "then ALL", {
                Var.B[t][r1][c1][IS_FREE], false,
                Var.B[t][r1][c1][IS_UNMOVABLE], false,
                Var.B[t][r2][c2][IS_FREE], false,
                Var.B[t][r2][c2][IS_UNMOVABLE], false})

        for col = 1, TotalColors do
            AddSimpleClause{
                V[t][r1][c1], false,
                Var.B[t][r1][c1][col], false,
                Var.B[t][r1][c1][col], true}
            AddSimpleClause{
                V[t][r1][c1], false,
                Var.B[t][r1][c1][col], true,
                Var.B[t][r2][c2][col], false}
            AddSimpleClause{
                V[t][r1][c1], true,
                Var.B[t][r1][c1][col], false,
                Var.B[t][r2][c2][col], false}
        end
    end
    -- 6420 clauses... for each turn!
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do for c = 1, COLUMNS do
        if c < COLUMNS then h(Var.RSC,t,r,c,r,c+1) end
        if r < ROWS then    h(Var.DSC,t,r,c,r+1,c) end
    end end end

    --[[
        now the "blocked" check and the "connection" check
        tile r,c is blocked if
            - tile r,c+1 is either unmovable or blocked
            or
            - it has the same color as tile r+1,c which is blocked
            or
            - it has the same color as tile r-1,c which is blocked
            or
            - it has the same color as tile r,c-1 which is blocked

        it would be a valid assignment to declare all tiles to be blocked up to now.
        to make sure that all movable tiles get moved, the following is done:

            - every tile gets a "blockedness" number
            - (1) if tile r,c+1 is unmovable, or if c == COLUMNS, and tile r,c is not free, then tile r,c is blocked
            - (2) if tiles r1,c1 and r2,c2 are neighbors of the same color, then
                    tile r1,c1 is blocked if and only if tile r2,c2 is blocked
                and tile r1,c1 is connected to the reference tile if and only if tile r2,c2 is connected to the reference tile
            - (3) if tile r,c is blocked then:
                -  c == COLUMNS
                or
                - tile r,c+1 is unmovable
                or
                - the left, upper or lower neighbor has the same color
                        and a lower blockedness number
                or
                - the right neighbor has a lower blockedness number

                  if tile r,c is connected to zero then:
                - it is the zero tile
                or
                - the left, right, top, or bottom neighbor
                   has the same color AND a lower connection number
            - (4) the reference tile of each color is connected to itself
            - (5) a free tile is never blocked or unmovable
    --]]

    print("check blocked...(1)"..total_number_of_clauses)
    --(1)
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do
        AddSimpleClause{Var.B[t][r][COLUMNS][IS_BLOCKED], true, Var.B[t][r][COLUMNS][IS_FREE], true, Var.B[t][r][COLUMNS][IS_UNMOVABLE], true}
        --(4)
        for c = 1, COLUMNS do
            AddSimpleClause{Var.B[t][r][c][IS_ZERO], false, Var.B[t][r][c][IS_CONNECTED_TO_ZERO], true}
        end
    end end
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do for c = 1, COLUMNS - 1 do
        AddIfThenClause("if ALL", {Var.B[t][r][c+1][IS_UNMOVABLE], true, Var.B[t][r][c][IS_FREE], false}, "then ALL", {Var.B[t][r][c][IS_BLOCKED], true})
        AddIfThenClause("if ALL", {Var.B[t][r][c+1][IS_BLOCKED], true, Var.B[t][r][c][IS_FREE], false}, "then ALL", {Var.B[t][r][c][IS_BLOCKED], true})
    end end end

    print("check blocked...(2)"..total_number_of_clauses)
    --(2)
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do for c = 1, COLUMNS - 1 do
        AddIfThenClause("if ALL", {Var.RSC[t][r][c], true, Var.B[t][r][c][IS_BLOCKED], true}, "then ALL", {Var.B[t][r][c+1][IS_BLOCKED], true})
        AddIfThenClause("if ALL", {Var.RSC[t][r][c], true, Var.B[t][r][c][IS_BLOCKED], false}, "then ALL", {Var.B[t][r][c+1][IS_BLOCKED], false})
        AddIfThenClause("if ALL", {Var.RSC[t][r][c], true, Var.B[t][r][c][IS_CONNECTED_TO_ZERO], true}, "then ALL", {Var.B[t][r][c+1][IS_CONNECTED_TO_ZERO], true})
        AddIfThenClause("if ALL", {Var.RSC[t][r][c], true, Var.B[t][r][c][IS_CONNECTED_TO_ZERO], false}, "then ALL", {Var.B[t][r][c+1][IS_CONNECTED_TO_ZERO], false})
    end end end
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS - 1 do for c = 1, COLUMNS do
        AddIfThenClause("if ALL", {Var.DSC[t][r][c], true, Var.B[t][r][c][IS_BLOCKED], true}, "then ALL", {Var.B[t][r+1][c][IS_BLOCKED], true})
        AddIfThenClause("if ALL", {Var.DSC[t][r][c], true, Var.B[t][r][c][IS_BLOCKED], false}, "then ALL", {Var.B[t][r+1][c][IS_BLOCKED], false})
        AddIfThenClause("if ALL", {Var.DSC[t][r][c], true, Var.B[t][r][c][IS_CONNECTED_TO_ZERO], true}, "then ALL", {Var.B[t][r+1][c][IS_CONNECTED_TO_ZERO], true})
        AddIfThenClause("if ALL", {Var.DSC[t][r][c], true, Var.B[t][r][c][IS_CONNECTED_TO_ZERO], false}, "then ALL", {Var.B[t][r+1][c][IS_CONNECTED_TO_ZERO], false})
    end end end

    print("check blocked...(3)"..total_number_of_clauses)
    --(3)
    -- many many distinct cases... so evil!
    -- there should be some better way to encode this

    -- prevent out-of-bound errors
    --
    -- if we write Var.B[t][r-1][c][number] and r == 1,
    -- we get an "attempt to index field ? (a nil value) error"
    -- even if we check that r > 1 beforehand. This can
    -- be prevented only if it is encapsulated with a function call
    --
    -- try the following minimal example:

    --[[
t = {"hi"}

-- works!
function h(b,f)
    if b then return f() else return "no!" end
end

print(t[1]..","..tostring(t[2])..h(false, function() return t[2][1] end))

-- does not work! attempt to index field ? (a nil value)
function h(b,f)
    if b then return f else return "no!" end
end

print(t[1]..","..tostring(t[2])..h(false, t[2][1]))
    --]]

    function OOB_catcher(b, f)
        if b then return f() else return nil end
    end

    -- how beautiful, 7 loops!
    -- there will be some duplicate clauses, it is easier
    -- to let the solver remove them than to handle this here.
    for t = 1, MaximumTurns + 1 do
    for r = 1, ROWS do
    for c = 1, COLUMNS do

    for _,b1 in pairs{true,false} do
    for _,b2 in pairs{true,false} do
    for _,b3 in pairs{true,false} do

        -- there is one reference tile of each color.
        -- if the puzzle is solved, all tiles are connected to the reference tile
        --
        -- if a tile is connected to the reference tile,
        --      - it is the reference tile itself
        --   OR - it is connected to a tile with a lower connection number.
        -- it would make sense that the reference tile has connection number zero but that isnt enforced.
        for _,b4 in pairs{true,false} do
            local function h(cl, a1, a2)
                cl[#cl+1] = a1
                cl[#cl+1] = a2
            end

            local cl1 = {Var.B[t][r][c][IS_CONNECTED_TO_ZERO], true}
            if r > 1 then h(cl1, Var.DSC[t][r-1][c], b1) end
            if r < ROWS then h(cl1, Var.DSC[t][r][c], b2) end
            if c > 1 then h(cl1, Var.RSC[t][r][c-1], b3) end
            if c < COLUMNS then h(cl1, Var.RSC[t][r][c], b4) end

            local cl2 = {Var.B[t][r][c][IS_ZERO], true}
            --[[up   ]] if r > 1 and b1 then h(cl2, Var.B[t][r-1][c][B_CONNECTION_NUMBER_COMPARE_DOWN_OFFSET + BITS - 1], false) end
            --[[down ]] if r < ROWS and b2 then h(cl2, Var.B[t][r][c][B_CONNECTION_NUMBER_COMPARE_DOWN_OFFSET + BITS - 1], true) end
            --[[left ]] if c > 1 and b3 then h(cl2, Var.B[t][r][c-1][B_CONNECTION_NUMBER_COMPARE_RIGHT_OFFSET + BITS - 1], false) end
            --[[right]] if c < COLUMNS and b4 then h(cl2, Var.B[t][r][c][B_CONNECTION_NUMBER_COMPARE_RIGHT_OFFSET + BITS - 1], true) end

            AddIfThenClause("if ALL", cl1, "then ONE", cl2)
        end
        -- if a tile is blocked then:
        --     - the tile to its right is unmovable
        --  OR - its right neighbor is not free and has a lower blockedness number
        --  OR - its left, top, or bottom neighbor has the same color AND a lower blockedness number
        if c < COLUMNS then
            local function h(cl, a1, a2)
                cl[#cl+1] = a1
                cl[#cl+1] = a2
            end

            for _,b4 in pairs{true,false} do
                local cl1 = {Var.B[t][r][c][IS_BLOCKED], true}
                if r > 1 then h(cl1, Var.DSC[t][r-1][c], b1) end
                if r < ROWS then h(cl1, Var.DSC[t][r][c], b2) end
                if c > 1 then h(cl1, Var.RSC[t][r][c-1], b3) end
                h(cl1, Var.B[t][r][c+1][IS_FREE], b4)

                local cl2 = {Var.B[t][r][c+1][IS_UNMOVABLE], true}
                if r > 1 and b1    then h(cl2, Var.B[t][r-1][c][B_BLOCK_NUMBER_COMPARE_DOWN_OFFSET + BITS - 1], false) end -- less or equal is enough to prevent loops
                if r < ROWS and b2 then h(cl2, Var.B[t][r][c][B_BLOCK_NUMBER_COMPARE_DOWN_OFFSET + BITS - 1], true) end
                if c > 1 and b3    then h(cl2, Var.B[t][r][c-1][B_BLOCK_NUMBER_COMPARE_RIGHT_OFFSET + BITS - 1], false) end
                if not b4          then h(cl2, Var.B[t][r][c][B_BLOCK_NUMBER_COMPARE_RIGHT_OFFSET + BITS - 1], true) end

                AddIfThenClause("if ALL", cl1, "then ONE", cl2)
            end
        end

    end end end end end end

    --(5)
    for t = 1, MaximumTurns + 1 do for r = 1, ROWS do for c = 1, COLUMNS do
        AddSimpleClause{Var.B[t][r][c][IS_FREE], false,    Var.B[t][r][c][IS_UNMOVABLE], false}
        AddSimpleClause{Var.B[t][r][c][IS_BLOCKED], false, Var.B[t][r][c][IS_FREE], false}
    end end end

    print("move!..."..total_number_of_clauses)
    -- now make the move!
    for t = 1, MaximumTurns do
    for r = 1, ROWS do
    for entry = 1, #Var.A[1][1][1] do
    for _,b in pairs{true, false} do

        for c = 1, COLUMNS do
            -- a blocked tile or an unmovable tile stays in place
            for _,e1 in pairs{IS_BLOCKED, IS_UNMOVABLE} do
                AddIfThenClause("if ALL", {Var.B[t][r][c][e1], true, Var.B[t][r][c][entry], b},
                    "then ALL", {Var.A[t+1][r][c][entry], b})
            end

            -- otherwise:
                -- if the tile to the left is neither blocked nor unmovable, move!

            if c > 1 then
                AddIfThenClause(
                    "if ALL", {
                    Var.B[t][r][c][IS_UNMOVABLE], false,
                    Var.B[t][r][c][IS_BLOCKED], false,
                    Var.B[t][r][c-1][IS_UNMOVABLE], false,
                    Var.B[t][r][c-1][IS_BLOCKED], false,
                    Var.B[t][r][c-1][entry], b},
                    "then ALL", {
                    Var.A[t+1][r][c][entry], b}
                )

                -- if the tile to the left is blocked or unmovable, this tile becomes free!
                if b then
                    AddIfThenClause(
                        "if ALL", {
                        Var.B[t][r][c][IS_UNMOVABLE], false,
                        Var.B[t][r][c][IS_BLOCKED], false,
                        Var.B[t][r][c-1][IS_UNMOVABLE], true},
                        "then ALL", {
                        Var.A[t+1][r][c][entry], entry == IS_FREE}
                    )
                    AddIfThenClause(
                        "if ALL", {
                        Var.B[t][r][c][IS_UNMOVABLE], false,
                        Var.B[t][r][c][IS_BLOCKED], false,
                        Var.B[t][r][c-1][IS_BLOCKED], true},
                        "then ALL", {
                        Var.A[t+1][r][c][entry], entry == IS_FREE}
                    )
                end
            else
                -- if there is no tile to the left, there is new free space!
                if b then
                    AddIfThenClause(
                        "if ALL", {
                        Var.B[t][r][c][IS_UNMOVABLE], false,
                        Var.B[t][r][c][IS_BLOCKED], false},
                        "then ALL", {
                        Var.A[t+1][r][c][entry], entry == IS_FREE}
                    )
                end
            end
        end

    end end end end

    print("winning condition check!.."..total_number_of_clauses)
    -- finally, check the winning condition. so easy now!
    local V = Var.B[MaximumTurns+1]
    for r = 1, ROWS do for c = 1, COLUMNS do
        local cl = {V[r][c][IS_FREE], true, V[r][c][IS_UNMOVABLE], true, V[r][c][IS_CONNECTED_TO_ZERO], true}
        for col = TotalColorsToConnect + 1, TotalColors do
            cl[#cl+1] = V[r][c][col]
            cl[#cl+1] = true
        end
        AddSimpleClause(cl)
    end end
    print("done!.."..total_number_of_clauses)
end

function MovementPattern()
    local num = {
        [false] = {[false] = 0, [true]  = 1},
        [true] = {[false] = 2, [true] = 3 }}
    local name = {[0] = "right", "up", "left", "down"}

    --[[
    -- this is how R was used
    for r = 1, ROWS do for c = 1, COLUMNS do
        -- rotate 0 degrees
        h(false, false, r, c, r, c)
        -- 90 degrees right
        h(false, true, r, c, c, ROWS + 1 - r)
        -- 180 degrees right
        h(true, false, r, c, ROWS + 1 - r, COLUMNS + 1 - c)
        -- 270 degrees right
        h(true, true,  r, c, COLUMNS + 1 - c, r)
    end end --]]

    now = 0
    ret = {}
    for t = 1, #Sol.R do
        now = (now + num[Sol.R[t][1]][Sol.R[t][2]]) % 4
        ret[#ret+1] = name[now]
    end
    return ret
end

CreateCNF()
WriteSATfile()
if USE_PICOSAT then
    os.execute("picosat satfile.cnf >solutionfile")
elseif USE_MINISAT then
    os.execute("minisat satfile.cnf solutionfile")
end
ParseSolution()
for i,m in ipairs(MovementPattern()) do
    for r = 1, ROWS do
        local s = ""
        for c = 1, COLUMNS do
            for entry = 1, #Sol.A[1][1][1] do
                if Sol.A[i][r][c][entry] then s = s .. entry else s = s .. " " end
                end
            s = s.."|"
        end
        print(s)
    end
    print (i..": "..m)
    for r = 1, ROWS do
        local s = ""
        for c = 1, COLUMNS do
            for entry = 1, #Sol.A[1][1][1] do
                if Sol.B[i][r][c][entry] then s = s .. entry else s = s .. " " end
            end
            if c < COLUMNS then if Sol.RSC[i][r][c] then  s = s.."---" else s = s .. " ; " end end
        end
        print(s)
        s = " "
        spaces = #Sol.A[1][1][1]+3
        for c = 1, COLUMNS do
            if r < ROWS then
                if Sol.DSC[i][r][c] then s = s .. "|" end
            else
                s = s .. " "
            end
            if Sol.B[i][r][c][IS_BLOCKED] then s = s .. "B" else s = s .. " " end
            local n = 0
            local f = 1
            for b = 0, BITS - 1 do
                if Sol.B[i][r][c][B_BLOCK_NUMBER_OFFSET + b] then n = n + f end
                f = f * 2
            end
            s = s..n
            s = s .. string.rep(" ", c*spaces-2-string.len(s)).."/ "
        end

        print(s)
        print()
    end
    print()
end