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
mirror_xblockgeom_t42 void mirror_x() { center_x *= -1; }
mirror_yblockgeom_t43 void mirror_y() { center_y *= -1; }
mirror_zblockgeom_t44 void mirror_z() { center_z *= -1; }
45
rotate_xblockgeom_t46 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]; }
rotate_yblockgeom_t47 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]; }
rotate_zblockgeom_t48 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
operator <blockgeom_t50 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
add_block(int pos_x,int pos_y,int pos_z,int size_x,int size_y,int size_z,int blockidx)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
add_block_positions_124(std::vector<int> & block_positions_124)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
add_block_positions_223(std::vector<int> & block_positions_223)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
xorshift32()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
condense_exclusives(std::vector<int> & vars)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
main()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
296