orange-boxes.py

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()