libs/ezsat/puzzle3d.cc

   1 /*
   2  *  ezSAT -- A simple and easy to use CNF generator for SAT solvers
   3  *
   4  *  Copyright (C) 2013  Claire Xenia Wolf <claire@yosyshq.com>
   5  *
   6  *  Permission to use, copy, modify, and/or distribute this software for any
   7  *  purpose with or without fee is hereby granted, provided that the above
   8  *  copyright notice and this permission notice appear in all copies.
   9  *
  10  *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11  *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12  *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13  *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14  *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15  *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16  *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17  *
  18  */
  19
  20 #include "ezminisat.h"
  21 #include <stdio.h>
  22 #include <assert.h>
  23
  24 #define DIM_X 5
  25 #define DIM_Y 5
  26 #define DIM_Z 5
  27
  28 #define NUM_124 6
  29 #define NUM_223 6
  30
  31 ezMiniSAT ez;
  32 int blockidx = 0;
  33 std::map<int, std::string> blockinfo;
  34 std::vector<int> grid[DIM_X][DIM_Y][DIM_Z];
  35
  36 struct blockgeom_t
  37 {
  38         int center_x, center_y, center_z;
  39         int size_x, size_y, size_z;
  40         int var;
  41
  42         void mirror_x() { center_x *= -1; }
  43         void mirror_y() { center_y *= -1; }
  44         void mirror_z() { center_z *= -1; }
  45
  46         void rotate_x() { int tmp[4] = { center_y, center_z, size_y, size_z }; center_y = tmp[1]; center_z = -tmp[0]; size_y = tmp[3]; size_z = tmp[2]; }
  47         void rotate_y() { int tmp[4] = { center_x, center_z, size_x, size_z }; center_x = tmp[1]; center_z = -tmp[0]; size_x = tmp[3]; size_z = tmp[2]; }
  48         void rotate_z() { int tmp[4] = { center_x, center_y, size_x, size_y }; center_x = tmp[1]; center_y = -tmp[0]; size_x = tmp[3]; size_y = tmp[2]; }
  49
  50         bool operator< (const blockgeom_t &other) const {
  51                 if (center_x != other.center_x) return center_x < other.center_x;
  52                 if (center_y != other.center_y) return center_y < other.center_y;
  53                 if (center_z != other.center_z) return center_z < other.center_z;
  54                 if (size_x != other.size_x) return size_x < other.size_x;
  55                 if (size_y != other.size_y) return size_y < other.size_y;
  56                 if (size_z != other.size_z) return size_z < other.size_z;
  57                 if (var != other.var) return var < other.var;
  58                 return false;
  59         }
  60 };
  61
  62 // geometry data for spatial symmetry constraints
  63 std::set<blockgeom_t> blockgeom;
  64
  65 int add_block(int pos_x, int pos_y, int pos_z, int size_x, int size_y, int size_z, int blockidx)
  66 {
  67         char buffer[1024];
  68         snprintf(buffer, 1024, "block(%d,%d,%d,%d,%d,%d,%d);", size_x, size_y, size_z, pos_x, pos_y, pos_z, blockidx);
  69
  70         int var = ez.literal();
  71         blockinfo[var] = buffer;
  72
  73         for (int ix = pos_x; ix < pos_x+size_x; ix++)
  74         for (int iy = pos_y; iy < pos_y+size_y; iy++)
  75         for (int iz = pos_z; iz < pos_z+size_z; iz++)
  76                 grid[ix][iy][iz].push_back(var);
  77
  78         blockgeom_t bg;
  79         bg.size_x = 2*size_x;
  80         bg.size_y = 2*size_y;
  81         bg.size_z = 2*size_z;
  82         bg.center_x = (2*pos_x + size_x) - DIM_X;
  83         bg.center_y = (2*pos_y + size_y) - DIM_Y;
  84         bg.center_z = (2*pos_z + size_z) - DIM_Z;
  85         bg.var = var;
  86
  87         assert(blockgeom.count(bg) == 0);
  88         blockgeom.insert(bg);
  89
  90         return var;
  91 }
  92
  93 void add_block_positions_124(std::vector<int> &block_positions_124)
  94 {
  95         block_positions_124.clear();
  96         for (int size_x = 1; size_x <= 4; size_x *= 2)
  97         for (int size_y = 1; size_y <= 4; size_y *= 2)
  98         for (int size_z = 1; size_z <= 4; size_z *= 2) {
  99                 if (size_x == size_y || size_y == size_z || size_z == size_x)
 100                         continue;
 101                 for (int ix = 0; ix <= DIM_X-size_x; ix++)
 102                 for (int iy = 0; iy <= DIM_Y-size_y; iy++)
 103                 for (int iz = 0; iz <= DIM_Z-size_z; iz++)
 104                         block_positions_124.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++));
 105         }
 106 }
 107
 108 void add_block_positions_223(std::vector<int> &block_positions_223)
 109 {
 110         block_positions_223.clear();
 111         for (int orientation = 0; orientation < 3; orientation++) {
 112                 int size_x = orientation == 0 ? 3 : 2;
 113                 int size_y = orientation == 1 ? 3 : 2;
 114                 int size_z = orientation == 2 ? 3 : 2;
 115                 for (int ix = 0; ix <= DIM_X-size_x; ix++)
 116                 for (int iy = 0; iy <= DIM_Y-size_y; iy++)
 117                 for (int iz = 0; iz <= DIM_Z-size_z; iz++)
 118                         block_positions_223.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++));
 119         }
 120 }
 121
 122 // use simple built-in random number generator to
 123 // ensure determinism of the program across platforms
 124 uint32_t xorshift32() {
 125         static uint32_t x = 314159265;
 126         x ^= x << 13;
 127         x ^= x >> 17;
 128         x ^= x << 5;
 129         return x;
 130 }
 131
 132 void condense_exclusives(std::vector<int> &vars)
 133 {
 134         std::map<int, std::set<int>> exclusive;
 135
 136         for (int ix = 0; ix < DIM_X; ix++)
 137         for (int iy = 0; iy < DIM_Y; iy++)
 138         for (int iz = 0; iz < DIM_Z; iz++) {
 139                 for (int a : grid[ix][iy][iz])
 140                 for (int b : grid[ix][iy][iz])
 141                         if (a != b)
 142                                 exclusive[a].insert(b);
 143         }
 144
 145         std::vector<std::vector<int>> pools;
 146
 147         for (int a : vars)
 148         {
 149                 std::vector<int> candidate_pools;
 150                 for (size_t i = 0; i < pools.size(); i++)
 151                 {
 152                         for (int b : pools[i])
 153                                 if (exclusive[a].count(b) == 0)
 154                                         goto no_candidate_pool;
 155                         candidate_pools.push_back(i);
 156                 no_candidate_pool:;
 157                 }
 158
 159                 if (candidate_pools.size() > 0) {
 160                         int p = candidate_pools[xorshift32() % candidate_pools.size()];
 161                         pools[p].push_back(a);
 162                 } else {
 163                         pools.push_back(std::vector<int>());
 164                         pools.back().push_back(a);
 165                 }
 166         }
 167
 168         std::vector<int> new_vars;
 169         for (auto &pool : pools)
 170         {
 171                 std::vector<int> formula;
 172                 int var = ez.literal();
 173
 174                 for (int a : pool)
 175                         formula.push_back(ez.OR(ez.NOT(a), var));
 176                 formula.push_back(ez.OR(ez.expression(ezSAT::OpOr, pool), ez.NOT(var)));
 177
 178                 ez.assume(ez.onehot(pool, true));
 179                 ez.assume(ez.expression(ezSAT::OpAnd, formula));
 180                 new_vars.push_back(var);
 181         }
 182
 183         printf("Condensed %d variables into %d one-hot pools.\n", int(vars.size()), int(new_vars.size()));
 184         vars.swap(new_vars);
 185 }
 186
 187 int main()
 188 {
 189         printf("\nCreating SAT encoding..\n");
 190
 191         // add 1x2x4 blocks
 192         std::vector<int> block_positions_124;
 193         add_block_positions_124(block_positions_124);
 194         condense_exclusives(block_positions_124);
 195         ez.assume(ez.manyhot(block_positions_124, NUM_124));
 196
 197         // add 2x2x3 blocks
 198         std::vector<int> block_positions_223;
 199         add_block_positions_223(block_positions_223);
 200         condense_exclusives(block_positions_223);
 201         ez.assume(ez.manyhot(block_positions_223, NUM_223));
 202
 203         // add constraint for max one block per grid element
 204         for (int ix = 0; ix < DIM_X; ix++)
 205         for (int iy = 0; iy < DIM_Y; iy++)
 206         for (int iz = 0; iz < DIM_Z; iz++) {
 207                 assert(grid[ix][iy][iz].size() > 0);
 208                 ez.assume(ez.onehot(grid[ix][iy][iz], true));
 209         }
 210
 211         printf("Found %d possible block positions.\n", int(blockgeom.size()));
 212
 213         // look for spatial symmetries
 214         std::set<std::set<blockgeom_t>> symmetries;
 215         symmetries.insert(blockgeom);
 216         bool keep_running = true;
 217         while (keep_running) {
 218                 keep_running = false;
 219                 std::set<std::set<blockgeom_t>> old_sym;
 220                 old_sym.swap(symmetries);
 221                 for (auto &old_sym_set : old_sym)
 222                 {
 223                         std::set<blockgeom_t> mx, my, mz;
 224                         std::set<blockgeom_t> rx, ry, rz;
 225                         for (auto &bg : old_sym_set) {
 226                                 blockgeom_t bg_mx = bg, bg_my = bg, bg_mz = bg;
 227                                 blockgeom_t bg_rx = bg, bg_ry = bg, bg_rz = bg;
 228                                 bg_mx.mirror_x(), bg_my.mirror_y(), bg_mz.mirror_z();
 229                                 bg_rx.rotate_x(), bg_ry.rotate_y(), bg_rz.rotate_z();
 230                                 mx.insert(bg_mx), my.insert(bg_my), mz.insert(bg_mz);
 231                                 rx.insert(bg_rx), ry.insert(bg_ry), rz.insert(bg_rz);
 232                         }
 233                         if (!old_sym.count(mx) || !old_sym.count(my) || !old_sym.count(mz) ||
 234                                         !old_sym.count(rx) || !old_sym.count(ry) || !old_sym.count(rz))
 235                                 keep_running = true;
 236                         symmetries.insert(old_sym_set);
 237                         symmetries.insert(mx);
 238                         symmetries.insert(my);
 239                         symmetries.insert(mz);
 240                         symmetries.insert(rx);
 241                         symmetries.insert(ry);
 242                         symmetries.insert(rz);
 243                 }
 244         }
 245
 246         // add constraints to eliminate all the spatial symmetries
 247         std::vector<std::vector<int>> vecvec;
 248         for (auto &sym : symmetries) {
 249                 std::vector<int> vec;
 250                 for (auto &bg : sym)
 251                         vec.push_back(bg.var);
 252                 vecvec.push_back(vec);
 253         }
 254         for (size_t i = 1; i < vecvec.size(); i++)
 255                 ez.assume(ez.ordered(vecvec[0], vecvec[1]));
 256
 257         printf("Found and eliminated %d spatial symmetries.\n", int(symmetries.size()));
 258         printf("Generated %d clauses over %d variables.\n", ez.numCnfClauses(), ez.numCnfVariables());
 259
 260         std::vector<int> modelExpressions;
 261         std::vector<bool> modelValues;
 262
 263         for (auto &it : blockinfo) {
 264                 ez.freeze(it.first);
 265                 modelExpressions.push_back(it.first);
 266         }
 267
 268         int solution_counter = 0;
 269         while (1)
 270         {
 271                 printf("\nSolving puzzle..\n");
 272                 bool ok = ez.solve(modelExpressions, modelValues);
 273
 274                 if (!ok) {
 275                         printf("No more solutions found!\n");
 276                         break;
 277                 }
 278
 279                 printf("Puzzle solution:\n");
 280                 std::vector<int> constraint;
 281                 for (size_t i = 0; i < modelExpressions.size(); i++)
 282                         if (modelValues[i]) {
 283                                 constraint.push_back(ez.NOT(modelExpressions[i]));
 284                                 printf("%s\n", blockinfo.at(modelExpressions[i]).c_str());
 285                         }
 286                 ez.assume(ez.expression(ezSAT::OpOr, constraint));
 287                 solution_counter++;
 288         }
 289
 290         printf("\nFound %d distinct solutions.\n", solution_counter);
 291         printf("Have a nice day.\n\n");
 292
 293         return 0;
 294 }
 295