#include "ezminisat.h"
#include <stdio.h>
#include <assert.h>

Include dependency graph for puzzle3d.cc:

Data Structures
struct	blockgeom_t

Macros
#define	DIM_X 5

#define	DIM_Y 5

#define	DIM_Z 5

#define	NUM_124 6

#define	NUM_223 6

Functions
int	add_block (int pos_x, int pos_y, int pos_z, int size_x, int size_y, int size_z, int blockidx)

void	add_block_positions_124 (std::vector< int > &block_positions_124)

void	add_block_positions_223 (std::vector< int > &block_positions_223)

uint32_t	xorshift32 ()

void	condense_exclusives (std::vector< int > &vars)

int	main ()

Variables
ezMiniSAT	ez

int	blockidx = 0

std::map< int, std::string >	blockinfo

std::vector< int >	grid [DIM_X][DIM_Y][DIM_Z]

std::set< blockgeom_t >	blockgeom

Macro Definition Documentation

#define DIM_X 5

Definition at line 24 of file puzzle3d.cc.

#define DIM_Y 5

Definition at line 25 of file puzzle3d.cc.

#define DIM_Z 5

Definition at line 26 of file puzzle3d.cc.

#define NUM_124 6

Definition at line 28 of file puzzle3d.cc.

#define NUM_223 6

Definition at line 29 of file puzzle3d.cc.

Function Documentation

int add_block	(	int	pos_x,
		int	pos_y,
		int	pos_z,
		int	size_x,
		int	size_y,
		int	size_z,
		int	blockidx
	)

Definition at line 65 of file puzzle3d.cc.

 {
     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;
 }

Here is the call graph for this function:

Here is the caller graph for this function:

void add_block_positions_124 ( std::vector< int > & block_positions_124 )

Definition at line 93 of file puzzle3d.cc.

 {
     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++));
     }
 }

Here is the call graph for this function:

Here is the caller graph for this function:

void add_block_positions_223 ( std::vector< int > & block_positions_223 )

Definition at line 108 of file puzzle3d.cc.

 {
     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++));
     }
 }

Here is the call graph for this function:

Here is the caller graph for this function:

void condense_exclusives ( std::vector< int > & vars )

Definition at line 132 of file puzzle3d.cc.

 {
     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);
 }

Here is the call graph for this function:

Here is the caller graph for this function:

int main ( )

Definition at line 187 of file puzzle3d.cc.

 {
     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;
 }

Here is the call graph for this function:

uint32_t xorshift32 ( )

Definition at line 124 of file puzzle3d.cc.

                       {
     static uint32_t x = 314159265;
     x ^= x << 13;
     x ^= x >> 17;
     x ^= x << 5;
     return x;
 }

Here is the caller graph for this function:

Variable Documentation

std::set<blockgeom_t> blockgeom

Definition at line 63 of file puzzle3d.cc.

int blockidx = 0

Definition at line 32 of file puzzle3d.cc.

std::map<int, std::string> blockinfo

Definition at line 33 of file puzzle3d.cc.

ezMiniSAT ez

Definition at line 31 of file puzzle3d.cc.

std::vector<int> grid[DIM_X][DIM_Y][DIM_Z]

Definition at line 34 of file puzzle3d.cc.

Data Structures

Macros

Functions

Variables

Macro Definition Documentation

Function Documentation

Variable Documentation