diff --git a/ReverseGameOfLife/Program.cs b/ReverseGameOfLife/Program.cs new file mode 100644 index 0000000..566dfcb --- /dev/null +++ b/ReverseGameOfLife/Program.cs @@ -0,0 +1,72 @@ +//inspired by https://www.youtube.com/watch?v=g8pjrVbdafY + +using SATInterface; +using SATInterface.Solver; + +string[] final = [ + "...xx..xx..xx...", + "..x.x..xx..x.x..", + ".x............x.", + "x....x.........x", + "xx...x........xx", + ".....x..........", + "........xxx.....", + ".....x..........", + "xx...x........xx", + "x....x.........x", + ".x............x.", + "..x.x..xx..x.x..", + "...xx..xx..xx...", +]; + +const int W = 40; +const int H = 40; +const int T = 5; + +var m = new Model(new Configuration() { Solver = new Kissat() }); + +var v = new BoolExpr[W, H, T]; +for (var y = 0; y < H; y++) + for (var x = 0; x < W; x++) + if (x == 0 || y == 0 || x == W - 1 || y == H - 1) + for (var t = 0; t < T; t++) + v[x, y, t] = false; + else + v[x, y, 0] = m.AddVar(); + +for (var t = 1; t < T; t++) + for (var y = 1; y < H - 1; y++) + for (var x = 1; x < W - 1; x++) + { + var neighbours = m.Sum( + v[x - 1, y - 1, t - 1], v[x, y - 1, t - 1], v[x + 1, y - 1, t - 1], + v[x - 1, y, t - 1], v[x + 1, y, t - 1], + v[x - 1, y + 1, t - 1], v[x, y + 1, t - 1], v[x + 1, y + 1, t - 1] + ); + v[x, y, t] = ((v[x, y, t - 1] & neighbours == 2) | neighbours == 3).Flatten(); + } + +for (var y = 0; y < H; y++) + for (var x = 0; x < W; x++) + { + var dst = false; + var sx = x - (W - final[0].Length) / 2; + var sy = y - (H - final.Length) / 2; + if (sx >= 0 && sy >= 0 && sx < final[0].Length && sy < final.Length) + dst = final[sy][sx] == 'x'; + + m.AddConstr(dst ? v[x, y, T - 1] : !v[x, y, T - 1]); + } + +m.Solve(); + +for (var t = 0; t < T; t++) +{ + Console.WriteLine("---------------------------------------"); + for (var y = 0; y < H; y++) + { + for (var x = 0; x < W; x++) + Console.Write(v[x, y, t].X ? 'x' : '.'); + Console.WriteLine(); + } +} \ No newline at end of file diff --git a/ReverseGameOfLife/ReverseGameOfLife.csproj b/ReverseGameOfLife/ReverseGameOfLife.csproj new file mode 100644 index 0000000..054e573 --- /dev/null +++ b/ReverseGameOfLife/ReverseGameOfLife.csproj @@ -0,0 +1,14 @@ + + + + Exe + net8.0 + enable + enable + + + + + + + diff --git a/SATInterface.sln b/SATInterface.sln index e9e84a6..2b730ec 100644 --- a/SATInterface.sln +++ b/SATInterface.sln @@ -31,6 +31,8 @@ Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "ParkerSquare", "ParkerSquar EndProject Project("{9A19103F-16F7-4668-BE54-9A1E7A4F7556}") = "EternityII", "EternityII\EternityII.csproj", "{A8951974-B4BE-4E97-B2B1-62E15014AD89}" EndProject +Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "ReverseGameOfLife", "ReverseGameOfLife\ReverseGameOfLife.csproj", "{21A2C414-A699-4876-9CB7-654D80BC75E3}" +EndProject Global GlobalSection(SolutionConfigurationPlatforms) = preSolution Debug|Any CPU = Debug|Any CPU @@ -89,6 +91,10 @@ Global {A8951974-B4BE-4E97-B2B1-62E15014AD89}.Debug|Any CPU.Build.0 = Debug|Any CPU {A8951974-B4BE-4E97-B2B1-62E15014AD89}.Release|Any CPU.ActiveCfg = Release|Any CPU {A8951974-B4BE-4E97-B2B1-62E15014AD89}.Release|Any CPU.Build.0 = Release|Any CPU + {21A2C414-A699-4876-9CB7-654D80BC75E3}.Debug|Any CPU.ActiveCfg = Debug|Any CPU + {21A2C414-A699-4876-9CB7-654D80BC75E3}.Debug|Any CPU.Build.0 = Debug|Any CPU + {21A2C414-A699-4876-9CB7-654D80BC75E3}.Release|Any CPU.ActiveCfg = Release|Any CPU + {21A2C414-A699-4876-9CB7-654D80BC75E3}.Release|Any CPU.Build.0 = Release|Any CPU EndGlobalSection GlobalSection(SolutionProperties) = preSolution HideSolutionNode = FALSE diff --git a/SATInterface/kissat.dll b/SATInterface/kissat.dll index 5c5f899..6b76c20 100644 Binary files a/SATInterface/kissat.dll and b/SATInterface/kissat.dll differ