summaryrefslogtreecommitdiff
path: root/libs/ezsat/puzzle3d.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-06-07 10:38:35 +0200
committerClifford Wolf <clifford@clifford.at>2013-06-07 10:38:35 +0200
commit3371563f2f14ce0d6bc7798d0fc802b54aae93c8 (patch)
treeae171f088f8dcf7760c014bc75f9fae84ee1fa25 /libs/ezsat/puzzle3d.cc
parentc32b9186815d0f129d923749a3c668c32f343c53 (diff)
Added ezSAT library
Diffstat (limited to 'libs/ezsat/puzzle3d.cc')
-rw-r--r--libs/ezsat/puzzle3d.cc293
1 files changed, 293 insertions, 0 deletions
diff --git a/libs/ezsat/puzzle3d.cc b/libs/ezsat/puzzle3d.cc
new file mode 100644
index 00000000..1655e697
--- /dev/null
+++ b/libs/ezsat/puzzle3d.cc
@@ -0,0 +1,293 @@
+/*
+ * ezSAT -- A simple and easy to use CNF generator for SAT solvers
+ *
+ * Copyright (C) 2013 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "ezminisat.h"
+#include <stdio.h>
+#include <assert.h>
+
+#define DIM_X 5
+#define DIM_Y 5
+#define DIM_Z 5
+
+#define NUM_124 6
+#define NUM_223 6
+
+ezMiniSAT ez;
+int blockidx = 0;
+std::map<int, std::string> blockinfo;
+std::vector<int> grid[DIM_X][DIM_Y][DIM_Z];
+
+struct blockgeom_t
+{
+ int center_x, center_y, center_z;
+ int size_x, size_y, size_z;
+ int var;
+
+ void mirror_x() { center_x *= -1; }
+ void mirror_y() { center_y *= -1; }
+ void mirror_z() { center_z *= -1; }
+
+ 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]; }
+ 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]; }
+ 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]; }
+
+ bool operator< (const blockgeom_t &other) const {
+ if (center_x != other.center_x) return center_x < other.center_x;
+ if (center_y != other.center_y) return center_y < other.center_y;
+ if (center_z != other.center_z) return center_z < other.center_z;
+ if (size_x != other.size_x) return size_x < other.size_x;
+ if (size_y != other.size_y) return size_y < other.size_y;
+ if (size_z != other.size_z) return size_z < other.size_z;
+ if (var != other.var) return var < other.var;
+ return false;
+ }
+};
+
+// geometry data for spatial symmetry constraints
+std::set<blockgeom_t> blockgeom;
+
+int add_block(int pos_x, int pos_y, int pos_z, int size_x, int size_y, int size_z, int blockidx)
+{
+ char buffer[1024];
+ snprintf(buffer, 1024, "block(%d,%d,%d,%d,%d,%d,%d);", size_x, size_y, size_z, pos_x, pos_y, pos_z, blockidx);
+
+ int var = ez.literal();
+ blockinfo[var] = buffer;
+
+ for (int ix = pos_x; ix < pos_x+size_x; ix++)
+ for (int iy = pos_y; iy < pos_y+size_y; iy++)
+ for (int iz = pos_z; iz < pos_z+size_z; iz++)
+ grid[ix][iy][iz].push_back(var);
+
+ blockgeom_t bg;
+ bg.size_x = 2*size_x;
+ bg.size_y = 2*size_y;
+ bg.size_z = 2*size_z;
+ bg.center_x = (2*pos_x + size_x) - DIM_X;
+ bg.center_y = (2*pos_y + size_y) - DIM_Y;
+ bg.center_z = (2*pos_z + size_z) - DIM_Z;
+ bg.var = var;
+
+ assert(blockgeom.count(bg) == 0);
+ blockgeom.insert(bg);
+
+ return var;
+}
+
+void add_block_positions_124(std::vector<int> &block_positions_124)
+{
+ block_positions_124.clear();
+ for (int size_x = 1; size_x <= 4; size_x *= 2)
+ for (int size_y = 1; size_y <= 4; size_y *= 2)
+ for (int size_z = 1; size_z <= 4; size_z *= 2) {
+ if (size_x == size_y || size_y == size_z || size_z == size_x)
+ continue;
+ for (int ix = 0; ix <= DIM_X-size_x; ix++)
+ for (int iy = 0; iy <= DIM_Y-size_y; iy++)
+ for (int iz = 0; iz <= DIM_Z-size_z; iz++)
+ block_positions_124.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++));
+ }
+}
+
+void add_block_positions_223(std::vector<int> &block_positions_223)
+{
+ block_positions_223.clear();
+ for (int orientation = 0; orientation < 3; orientation++) {
+ int size_x = orientation == 0 ? 3 : 2;
+ int size_y = orientation == 1 ? 3 : 2;
+ int size_z = orientation == 2 ? 3 : 2;
+ for (int ix = 0; ix <= DIM_X-size_x; ix++)
+ for (int iy = 0; iy <= DIM_Y-size_y; iy++)
+ for (int iz = 0; iz <= DIM_Z-size_z; iz++)
+ block_positions_223.push_back(add_block(ix, iy, iz, size_x, size_y, size_z, blockidx++));
+ }
+}
+
+// use simple built-in random number generator to
+// ensure determinism of the program across platforms
+uint32_t xorshift32() {
+ static uint32_t x = 314159265;
+ x ^= x << 13;
+ x ^= x >> 17;
+ x ^= x << 5;
+ return x;
+}
+
+void condense_exclusives(std::vector<int> &vars)
+{
+ std::map<int, std::set<int>> exclusive;
+
+ for (int ix = 0; ix < DIM_X; ix++)
+ for (int iy = 0; iy < DIM_Y; iy++)
+ for (int iz = 0; iz < DIM_Z; iz++) {
+ for (int a : grid[ix][iy][iz])
+ for (int b : grid[ix][iy][iz])
+ if (a != b)
+ exclusive[a].insert(b);
+ }
+
+ std::vector<std::vector<int>> pools;
+
+ for (int a : vars)
+ {
+ std::vector<int> candidate_pools;
+ for (size_t i = 0; i < pools.size(); i++)
+ {
+ for (int b : pools[i])
+ if (exclusive[a].count(b) == 0)
+ goto no_candidate_pool;
+ candidate_pools.push_back(i);
+ no_candidate_pool:;
+ }
+
+ if (candidate_pools.size() > 0) {
+ int p = candidate_pools[xorshift32() % candidate_pools.size()];
+ pools[p].push_back(a);
+ } else {
+ pools.push_back(std::vector<int>());
+ pools.back().push_back(a);
+ }
+ }
+
+ std::vector<int> new_vars;
+ for (auto &pool : pools)
+ {
+ std::vector<int> formula;
+ int var = ez.literal();
+
+ for (int a : pool)
+ formula.push_back(ez.OR(ez.NOT(a), var));
+ formula.push_back(ez.OR(ez.expression(ezSAT::OpOr, pool), ez.NOT(var)));
+
+ ez.assume(ez.onehot(pool, true));
+ ez.assume(ez.expression(ezSAT::OpAnd, formula));
+ new_vars.push_back(var);
+ }
+
+ printf("Condensed %d variables into %d one-hot pools.\n", int(vars.size()), int(new_vars.size()));
+ vars.swap(new_vars);
+}
+
+int main()
+{
+ printf("\nCreating SAT encoding..\n");
+
+ // add 1x2x4 blocks
+ std::vector<int> block_positions_124;
+ add_block_positions_124(block_positions_124);
+ condense_exclusives(block_positions_124);
+ ez.assume(ez.manyhot(block_positions_124, NUM_124));
+
+ // add 2x2x3 blocks
+ std::vector<int> block_positions_223;
+ add_block_positions_223(block_positions_223);
+ condense_exclusives(block_positions_223);
+ ez.assume(ez.manyhot(block_positions_223, NUM_223));
+
+ // add constraint for max one block per grid element
+ for (int ix = 0; ix < DIM_X; ix++)
+ for (int iy = 0; iy < DIM_Y; iy++)
+ for (int iz = 0; iz < DIM_Z; iz++) {
+ assert(grid[ix][iy][iz].size() > 0);
+ ez.assume(ez.onehot(grid[ix][iy][iz], true));
+ }
+
+ printf("Found %d possible block positions.\n", int(blockgeom.size()));
+
+ // look for spatial symmetries
+ std::set<std::set<blockgeom_t>> symmetries;
+ symmetries.insert(blockgeom);
+ bool keep_running = true;
+ while (keep_running) {
+ keep_running = false;
+ std::set<std::set<blockgeom_t>> old_sym;
+ old_sym.swap(symmetries);
+ for (auto &old_sym_set : old_sym)
+ {
+ std::set<blockgeom_t> mx, my, mz;
+ std::set<blockgeom_t> rx, ry, rz;
+ for (auto &bg : old_sym_set) {
+ blockgeom_t bg_mx = bg, bg_my = bg, bg_mz = bg;
+ blockgeom_t bg_rx = bg, bg_ry = bg, bg_rz = bg;
+ bg_mx.mirror_x(), bg_my.mirror_y(), bg_mz.mirror_z();
+ bg_rx.rotate_x(), bg_ry.rotate_y(), bg_rz.rotate_z();
+ mx.insert(bg_mx), my.insert(bg_my), mz.insert(bg_mz);
+ rx.insert(bg_rx), ry.insert(bg_ry), rz.insert(bg_rz);
+ }
+ if (!old_sym.count(mx) || !old_sym.count(my) || !old_sym.count(mz) ||
+ !old_sym.count(rx) || !old_sym.count(ry) || !old_sym.count(rz))
+ keep_running = true;
+ symmetries.insert(old_sym_set);
+ symmetries.insert(mx);
+ symmetries.insert(my);
+ symmetries.insert(mz);
+ symmetries.insert(rx);
+ symmetries.insert(ry);
+ symmetries.insert(rz);
+ }
+ }
+
+ // add constraints to eliminate all the spatial symmetries
+ std::vector<std::vector<int>> vecvec;
+ for (auto &sym : symmetries) {
+ std::vector<int> vec;
+ for (auto &bg : sym)
+ vec.push_back(bg.var);
+ vecvec.push_back(vec);
+ }
+ for (size_t i = 1; i < vecvec.size(); i++)
+ ez.assume(ez.ordered(vecvec[0], vecvec[1]));
+
+ printf("Found and eliminated %d spatial symmetries.\n", int(symmetries.size()));
+ printf("Generated %d clauses over %d variables.\n", ez.numCnfVariables(), int(ez.cnf().size()));
+
+ std::vector<int> modelExpressions;
+ std::vector<bool> modelValues;
+
+ for (auto &it : blockinfo)
+ modelExpressions.push_back(it.first);
+
+ int solution_counter = 0;
+ while (1)
+ {
+ printf("\nSolving puzzle..\n");
+ bool ok = ez.solve(modelExpressions, modelValues);
+
+ if (!ok) {
+ printf("No more solutions found!\n");
+ break;
+ }
+
+ printf("Puzzle solution:\n");
+ std::vector<int> constraint;
+ for (size_t i = 0; i < modelExpressions.size(); i++)
+ if (modelValues[i]) {
+ constraint.push_back(ez.NOT(modelExpressions[i]));
+ printf("%s\n", blockinfo.at(modelExpressions[i]).c_str());
+ }
+ ez.assume(ez.expression(ezSAT::OpOr, constraint));
+ solution_counter++;
+ }
+
+ printf("\nFound %d distinct solutions.\n", solution_counter);
+ printf("Have a nice day.\n\n");
+
+ return 0;
+}
+