yoshiscookies.lua

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

-- use a -1 to add a "yoshi" tile

--[[
puzzle_to_solve = {
{1,5,4,5,2},
{4,2,1,4,5},
{5,1,4,5,1},
{2,4,5,2,4},
{4,1,2,5,2}
}
--]]

puzzle_to_solve = {
{1,1,1,1,1,2},
{2,2,2,2,5,3},
{3,3,3,3,5,4},
{4,4,4,4,5,1}
}

-- how many steps can be performed?
steps = 9

-- playing field has 8 rows and 8 columns
-- 5 different tile types can appear on the field
-- "yoshi" counts as all tile types at once,
-- and sets an extra bit.
original_rows = #puzzle_to_solve
original_cols = #puzzle_to_solve[1]
original_ttypes = 5

if original_rows < original_cols then original_rows = original_cols end
if original_rows > original_cols then original_cols = original_rows end
assert(original_rows == original_cols, "sorry, some part of the code requires original_rows==original_cols")
assert(original_rows >= 2 and original_cols >= 2, "puzzles with only one row or one column are pointless...")
assert(original_ttypes >= 2, "there must be at least 2 different tiles!")

rows = original_rows
cols = original_cols
ttypes = original_ttypes + 1

NewVar("rotate",{steps, rows})
NewVar("rotate_colbit",steps)
NewVar("rotate_directionbit",steps)
NewVar("always_true")
UnitClause(Var.always_true, true)
NewVar("always_false")
UnitClause(Var.always_false, false)
NewVar("playingfield", {steps+1, rows, cols, ttypes})
NewVar("AtLeastTwoRows", steps)
NewVar("AtLeastTwoRows_help", {steps, cols})
NewVar("AtLeastTwoCols", steps)
NewVar("AtLeastTwoCols_help", {steps, rows})
NewVar("row_is_in_use", {steps+1, rows+1})
NewVar("col_is_in_use", {steps+1, cols+1})
NewVar("delete_row_help", {steps, rows, original_ttypes})
NewVar("delete_row", {steps, rows})
NewVar("delete_col_help", {steps, cols, original_ttypes})
NewVar("delete_col", {steps, cols})
NewVar("rotate_is_allowed", steps)

-- initialize with the given pattern
for r = 1, rows do for c = 1, cols do for ttype = 1, ttypes do
    if r <= #puzzle_to_solve and c <= #puzzle_to_solve[1] then
        local is_of_this_type = (puzzle_to_solve[r][c] == ttype or puzzle_to_solve[r][c] == -1)
        UnitClause(Var.playingfield[1][r][c][ttype], is_of_this_type)
    else
        UnitClause(Var.playingfield[1][r][c][ttype], true)
    end
end end end

for step = 1, steps+1 do

    -- Var.row_is_in_use
    for r = 1, rows do
        cl = NewClause()
        for c = 1, cols do
            ExtendClause(cl, Var.playingfield[step][r][c][ttypes], false)
        end
        AddIfAndOnlyIfClause(
            "ALL of",{
            Var.row_is_in_use[step][r], true},
            "if and only if",
            "ONE of",
            cl
        )
    end
    UnitClause(Var.row_is_in_use[step][rows+1], false)

    -- Var.col_is_in_use
    for c = 1, cols do
        cl = NewClause()
        for r = 1, rows do
            ExtendClause(cl, Var.playingfield[step][r][c][ttypes], false)
        end
        AddIfAndOnlyIfClause(
            "ALL of",{
            Var.col_is_in_use[step][c], true},
            "if and only if",
            "ONE of",
            cl
        )
    end
    UnitClause(Var.col_is_in_use[step][cols+1], false)

end


for step = 1, steps do

print("writing clauses for step "..step.." of "..steps.."...")

-- disallow undoing a rotation
if step >= 2 then
for r = 1, rows do
for _,colbit in pairs{true,false} do
for _,dbit in pairs{true,false} do

    AddIfThenClause(
        "if ALL",{
        Var.rotate[step][r], true,
        Var.rotate_colbit[step], colbit,
        Var.rotate_directionbit[step], dbit},
        "then ONE",{
        Var.rotate[step-1][r], false,
        Var.rotate_colbit[step-1], not colbit,
        Var.rotate_directionbit[step-1], dbit}
    )
end end end end

-- Var.AtLeastTwoCols
cl_over_all_c = NewClause()
for ignore_c = 1, cols do
    cl_help = NewClause()
    for c = 1, cols do
        if c ~= ignore_c then
            ExtendClause(cl_help, Var.col_is_in_use[step][c], true)
        end
    end
    AddIfAndOnlyIfClause(
        "ALL of",{
        Var.AtLeastTwoCols_help[step][ignore_c], true},
        "if and only if",
        "ONE of",
        cl_help
    )

    ExtendClause(cl_over_all_c, Var.AtLeastTwoCols_help[step][ignore_c], true)
end
AddIfAndOnlyIfClause(
    "ALL of",{
    Var.AtLeastTwoCols[step], true},
    "if and only if",
    "ALL of",
    cl_over_all_c
)

-- Var.AtLeastTwoRows[step]==true <=> at least 2(Var.col_is_in_use[step][c], c = 1, cols)
cl_over_all_r = NewClause()
for ignore_r = 1, rows do
    cl_help = NewClause()
    for r = 1, rows do
        if r ~= ignore_r then
            ExtendClause(cl_help, Var.row_is_in_use[step][r], true)
        end
    end
    AddIfAndOnlyIfClause(
        "ALL of",{
        Var.AtLeastTwoRows_help[step][ignore_r], true},
        "if and only if",
        "ONE of",
        cl_help
    )

    ExtendClause(cl_over_all_r, Var.AtLeastTwoRows_help[step][ignore_r], true)
end
AddIfAndOnlyIfClause(
    "ALL of",{
    Var.AtLeastTwoRows[step], true},
    "if and only if",
    "ALL of",
    cl_over_all_r
)


-- Var.delete_row
for r = 1, rows do
    cl_delete_row_r = NewClause()

    for ttype = 1, original_ttypes do
        cl_help = NewClause()
        ExtendClause(cl_help, Var.AtLeastTwoCols[step], true) -- don't delete if there is no second column
        ExtendClause(cl_help, Var.row_is_in_use[step][r], true) -- don't delete an already empty row
        for c = 1, cols do
            ExtendClause(cl_help, Var.playingfield[step][r][c][ttype], true) -- if all tiles on a row are of the same type, delete it.
        end

        AddIfAndOnlyIfClause(
            "ALL of",
            cl_help,
            "if and only if",
            "ALL of",{
            Var.delete_row_help[step][r][ttype], true}
        )

        ExtendClause(cl_delete_row_r, Var.delete_row_help[step][r][ttype], true)
    end

    AddIfAndOnlyIfClause(
        "ONE of",
        cl_delete_row_r,
        "if and only if",
        "ALL of",{
        Var.delete_row[step][r], true}
    )

end

-- Var.delete_col
for c = 1, cols do
    cl_delete_col_c = NewClause()

    for ttype = 1, original_ttypes do
        cl_help = NewClause()
        ExtendClause(cl_help, Var.AtLeastTwoRows[step], true)
        ExtendClause(cl_help, Var.col_is_in_use[step][c], true)
        for r = 1, rows do
            ExtendClause(cl_help, Var.playingfield[step][r][c][ttype], true)
        end

        AddIfAndOnlyIfClause(
            "ALL of",
            cl_help,
            "if and only if",
            "ALL of",{
            Var.delete_col_help[step][c][ttype], true}
        )

        ExtendClause(cl_delete_col_c, Var.delete_col_help[step][c][ttype], true)
    end

    AddIfAndOnlyIfClause(
        "ONE of",
        cl_delete_col_c,
        "if and only if",
        "ALL of",{
        Var.delete_col[step][c], true,
        }
    )

--  UnitClause(Var.delete_col[step][c], false)
end

-- rotate is only allowed if nothing is to be deleted (helper variable setup)
cl = NewClause()
for r = 1, rows do
    ExtendClause(cl, Var.delete_row[step][r], false)
end
for c = 1, cols do
    ExtendClause(cl, Var.delete_col[step][c], false)
end
AddIfAndOnlyIfClause(
    "ALL of",{
    Var.rotate_is_allowed[step], true},
    "if and only if",
    "ALL of",
    cl
)

-- allow only one rotate at once
for r1 = 1, rows-1 do for r2 = r1+1, rows do
    AddSimpleClause({
        Var.rotate[step][r1], false,
        Var.rotate[step][r2], false}
    )
end end
-- disallow rotate if something is deleted
cl = NewClause()
for r = 1, rows do
    ExtendClause(cl, Var.rotate[step][r], false)
end
AddIfThenClause(
    "if ONE",{
    Var.rotate_is_allowed[step],false},
    "then ALL",
    cl
)
-- disallow rotating an empty row, and
-- disallow rotating rows if there is only one column
for r = 1, rows do
    AddIfThenClause(
        "if ALL",{
        Var.rotate[step][r], true,
        Var.rotate_colbit[step], false},
        "then ALL",{
        Var.row_is_in_use[step][r], true,
        Var.AtLeastTwoCols[step], true}
    )
end
-- disallow rotating an empty col
for c = 1, cols do
    AddIfThenClause(
        "if ALL",{
        Var.rotate[step][c], true,
        Var.rotate_colbit[step], true},
        "then ALL",{
        Var.col_is_in_use[step][c], true,
        Var.AtLeastTwoRows[step], true}
    )
end

-- take care about all "trivial" cases of rotation...
for ttype = 1, ttypes do for r = 1, rows do for c = 1, cols do
    AddIfThenClause(
        "if ONE",{
        Var.row_is_in_use[step][r], false,
        Var.col_is_in_use[step][c], false},
        "then ALL",{
        Var.playingfield[step+1][r][c][ttype], true}
    )

    for _,b in pairs({true, false}) do
        -- if rotate doesn't match row and column number,
        -- then nothing is rotated!

        AddIfThenClause(
            "if ALL", {
            Var.rotate_is_allowed[step], true,
            Var.rotate[step][r], false,
            Var.rotate[step][c], false,
            Var.playingfield[step][r][c][ttype], b},
            "then ALL", {
            Var.playingfield[step+1][r][c][ttype], b}
        )
        -- if rotate_colbit==true, and rotate[c]==false
        -- then nothing is rotated
        AddIfThenClause(
            "if ALL", {
            Var.rotate_is_allowed[step], true,
            Var.rotate_colbit[step], true,
            Var.rotate[step][c], false,
            Var.playingfield[step][r][c][ttype], b},
            "then ALL", {
            Var.playingfield[step+1][r][c][ttype], b}
        )

        -- if rotate_colbit==false, and rotate[r]==false
        -- then nothing is rotated
        AddIfThenClause(
            "if ALL", {
            Var.rotate_is_allowed[step], true,
            Var.rotate_colbit[step], false,
            Var.rotate[step][r], false,
            Var.playingfield[step][r][c][ttype], b},
            "then ALL", {
            Var.playingfield[step+1][r][c][ttype], b}
        )
    end
end end end

-- take care about all non-trivial cases

-- rotate a ROW
-- (a few thousand clauses...)
for ttype = 1, ttypes do
for r = 1, rows do
for c = 1, cols do
for new_c = 1, cols do
for _,b in pairs({true,false}) do
if c ~= new_c then

    -- rotate a row RIGHT
    cl = {
        Var.row_is_in_use[step][r], true,
        Var.col_is_in_use[step][c], true,
        Var.rotate[step][r], true,
        Var.rotate_colbit[step], false,
        Var.rotate_directionbit[step], false}

    if new_c > c then
        for k = c + 1, new_c - 1 do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
    else
        for k = 1, new_c - 1 do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
        for k = c + 1, cols do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
    end
    ExtendClause(cl, Var.col_is_in_use[step][new_c], true)
    ExtendClause(cl, Var.playingfield[step][r][c][ttype], b)
    AddIfThenClause(
        "if ALL",
        cl,
        "then",{
        Var.playingfield[step+1][r][new_c][ttype], b}
    )

    -- rotate a row LEFT
    cl = {
        Var.row_is_in_use[step][r], true,
        Var.col_is_in_use[step][c], true,
        Var.rotate[step][r], true,
        Var.rotate_colbit[step], false,
        Var.rotate_directionbit[step], true}

    if new_c < c then
        for k = new_c + 1, c - 1 do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
    else
        for k = 1, c - 1 do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
        for k = new_c + 1, cols do
            ExtendClause(cl, Var.col_is_in_use[step][k], false)
        end
    end
    ExtendClause(cl, Var.col_is_in_use[step][new_c], true)
    ExtendClause(cl, Var.playingfield[step][r][c][ttype], b)
    AddIfThenClause(
        "if ALL",
        cl,
        "then",{
        Var.playingfield[step+1][r][new_c][ttype], b}
    )

end end end end end end

-- rotate a COL
-- (a few thousand clauses...)
for ttype = 1, ttypes do
for r = 1, rows do
for c = 1, cols do
for new_r = 1, rows do
for _,b in pairs({true,false}) do
if r ~= new_r then

    -- rotate a col DOWN
    cl = {
        Var.row_is_in_use[step][r], true,
        Var.col_is_in_use[step][c], true,
        Var.rotate[step][c], true,
        Var.rotate_colbit[step], true,
        Var.rotate_directionbit[step], false}

    if new_r > r then
        for k = r + 1, new_r - 1 do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
    else
        for k = 1, new_r - 1 do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
        for k = r + 1, rows do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
    end
    ExtendClause(cl, Var.row_is_in_use[step][new_r], true)
    ExtendClause(cl, Var.playingfield[step][r][c][ttype], b)
    AddIfThenClause(
        "if ALL",
        cl,
        "then",{
        Var.playingfield[step+1][new_r][c][ttype], b}
    )

    -- rotate a col UP
    cl = {
        Var.row_is_in_use[step][r], true,
        Var.col_is_in_use[step][c], true,
        Var.rotate[step][c], true,
        Var.rotate_colbit[step], true,
        Var.rotate_directionbit[step], true}

    if new_r < r then
        for k = new_r + 1, r - 1 do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
    else
        for k = 1, r - 1 do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
        for k = new_r + 1, rows do
            ExtendClause(cl, Var.row_is_in_use[step][k], false)
        end
    end
    ExtendClause(cl, Var.row_is_in_use[step][new_r], true)
    ExtendClause(cl, Var.playingfield[step][r][c][ttype], b)
    AddIfThenClause(
        "if ALL",
        cl,
        "then",{
        Var.playingfield[step+1][new_r][c][ttype], b}
    )

end end end end end end

for ttype = 1, ttypes do for r = 1, rows do for c = 1, cols do
    AddIfThenClause(
        "if ONE", {
        Var.delete_row[step][r], true,
        Var.delete_col[step][c], true},
        "then ALL",{
        Var.playingfield[step+1][r][c][ttype], true}
    )
end end end

for ttype = 1, ttypes do for r = 1, rows do for c = 1, cols do for _,b in pairs{true,false} do
    AddIfThenClause(
        "if ALL", {
        Var.rotate_is_allowed[step], false,
        Var.delete_row[step][r], false,
        Var.delete_col[step][c], false,
        Var.playingfield[step][r][c][ttype], b},
        "then ALL",{
        Var.playingfield[step+1][r][c][ttype], b}
    )
end end end end

end

--UnitClause(Var.rotate[1][6], true)
--UnitClause(Var.rotate_colbit[1], true)
--UnitClause(Var.rotate_directionbit[1], false)

for r = 1, rows do
    UnitClause(Var.row_is_in_use[steps+1][r], false)
end
for c = 1, cols do
    UnitClause(Var.col_is_in_use[steps+1][c], false)
end

WriteSATfile()
if USE_PICOSAT then
    os.execute("picosat satfile.cnf >solutionfile")
elseif USE_MINISAT then
    os.execute("minisat satfile.cnf solutionfile")
end
ParseSolution()
--PrintSolution()
for step = 1, steps do
    print("step "..step..": ")
    print()
    s = "STATE   : "
    for c = 1, cols do
        if Sol.col_is_in_use[step][c]==false then
            s = s .. " empty "
        else
            if Sol.delete_col[step][c] then
                s = s .. "del"
            else
                s = s .. "   "
            end
            if Sol.rotate[step][c] and Sol.rotate_colbit[step] then
                if Sol.rotate_directionbit[step]==true then
                    s = s .. " r^ "
                else
                    s = s .. " rV "
                end
            else
                s = s .. "    "
            end
        end
        s = s .. ": "
    end
    print(s)
    s = "--------:"
    for c = 1, cols do s = s .. "--------:" end
    print(s)
    for r = 1, rows do
        s = ""
        if Sol.row_is_in_use[step][r]==false then
            s = s .. " empty "
        else
            if Sol.delete_row[step][r] then
                s = s .. "del"
            else
                s = s .. "   "
            end
            if Sol.rotate[step][r] and not Sol.rotate_colbit[step] then
                if Sol.rotate_directionbit[step]==false then
                    s = s .. " r> "
                else
                    s = s .. " <r "
                end
            else
                s = s .. "    "
            end
        end
        s = s .. " : "
        for c = 1, cols do
            for ttype = 1, ttypes do
                if Sol.playingfield[step][r][c][ttype] then s = s .. ttype else s = s .. " " end
            end
            s = s .. " : "
        end
        print(s)

        s = "--------:"
        for c = 1, cols do s = s .. "--------:" end
        print(s)
    end
end

print("step "..(steps+1)..":")
print()

for r = 1, rows do
    s = ""
    for c = 1, cols do
        for ttype = 1, ttypes do
            if Sol.playingfield[steps+1][r][c][ttype] then s = s .. ttype else s = s .. " " end
        end
        s = s .. " "
    end
    print(s)
end