Created
March 7, 2024 10:48
-
-
Save maweki/55435470df5e70735a6ea69ebae1961e to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
from pysat.formula import * | |
from collections import namedtuple | |
P = namedtuple('P', ['x', 'y', 'z']) | |
boxes = {} | |
depth = 7 | |
width = 3 | |
height = 3 | |
for x in range(depth): | |
for y in range(width): | |
for z in range(height): | |
boxes[(x,y,z)] = Atom(P(x,y,z)) | |
constraints = [] | |
# side view | |
X = True | |
O = False | |
side_view = [ | |
[X,X,X,X,O,O,O], | |
[X,X,X,X,X,X,O], | |
[X,X,X,X,X,X,X], | |
] | |
for x in range(depth): | |
for z in range(height): | |
if side_view[-z-1][x]: | |
constraints.append(Or(*[boxes[(x,y,z)] for y in range(width)])) | |
else: | |
constraints.append(Neg(Or(*[boxes[(x,y,z)] for y in range(width)]))) | |
# back view | |
for y in range(width): | |
for z in range(height): | |
constraints.append(Or(*[boxes[(x,y,z)] for x in range(depth)])) | |
# top view | |
for y in range(width): | |
for x in range(depth): | |
constraints.append(Or(*[boxes[(x,y,z)] for z in range(height)])) | |
# gravity | |
for x in range(depth): | |
for y in range(width): | |
for z in range(height-1): | |
constraints.append(Implies(boxes[(x,y,z+1)], boxes[(x,y,z)])) | |
f = And(*constraints) | |
from pysat.solvers import Solver | |
with Solver(bootstrap_with=f) as solver: | |
while solver.solve(): | |
model = solver.get_model() | |
atoms = Formula.formulas((b for b in model if b > 0), atoms_only=True) | |
boxes_needed = len(atoms) | |
print("Solution with", boxes_needed, "boxes found") | |
print(atoms) | |
print("="*80) | |
from pysat.card import CardEnc | |
solver.append_formula(CardEnc.atmost(f.literals(boxes.values()), boxes_needed-1, vpool=Formula.export_vpool())) | |
import matplotlib.pyplot as plt | |
import numpy as np | |
# Prepare some coordinates | |
x, y, z = np.indices((depth, depth, depth)) | |
cubes = [((atom.object.x == x) & (atom.object.y == y) & (atom.object.z == z) ) for atom in atoms] | |
# Combine the objects into a single boolean array | |
voxelarray = cubes[0] | |
for cube in cubes[1:]: | |
voxelarray |= cube | |
# Plot | |
fig, ax = plt.subplots(subplot_kw={"projection": "3d"}) | |
ax.voxels(voxelarray, edgecolor='k') | |
ax.set(xticklabels=[], yticklabels=[], zticklabels=[]) | |
plt.show() |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment