296 lines
8.8 KiB
C++
296 lines
8.8 KiB
C++
|
/*
|
||
|
|
* 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.numCnfClauses(), ez.numCnfVariables());
|
||
|
|
|
||
|
|
std::vector<int> modelExpressions;
|
||
|
|
std::vector<bool> modelValues;
|
||
|
|
|
||
|
|
for (auto &it : blockinfo) {
|
||
|
|
ez.freeze(it.first);
|
||
|
|
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;
|
||
|
|
}
|
||
|
|
|