[Python][SAT] Optimizing production of a cardboard toy using SAT-solver

[Python][SAT] Optimizing production of a cardboard toy using SAT-solver

[Python][SAT] Optimizing production of a cardboard toy using SAT-solver

(The following text has been copypasted to the SAT/SMT by example.)

This is a do-it-yourself toy horse I once bought, made of cardboard parts:

All parts came in 3 plates (pardon my cheap smartphone):

And the assembly manual:

Now the question: can we put all the parts needed on smaller plates? To save some cardboard material?

I "digitized" all parts using usual notebook:

I don't know a real size of a square in notebook, probably, ~5mm. I would call it "one [square] unit".

Then I took the same piece of Python code I used before (click here and Ctrl-F for "tiling puzzle"). That code used Z3, and I rewrote it for generic SAT. (The source code.)

It was easy: there are just (a big) pack of boolean variables and AMO1/ALO1 constraints, or, as I called them before, POPCNT1.

Also, my idea is based on Donald Knuth's Dancing Links paper (I translated it to SAT).

Thanks to parallelized Plingeling, I could find a solution for a 40*30 [units] plate in minutes:

(The source code, it uses SAT_lib library and Plingeling).

Probably this is smallest plate possible, however, I didn't checked even smaller. You can decrease dimensions and run it again and again...

Now the question: the toy factory wants to ship all parts in several (smaller) plates. Like, 3 of them. Because one plate is impractical for shipping, handling, etc.

To put all parts on 3 plates, I can just add 2 borders between them:

board=["*"*BOARD_SMALL_WIDTH + " " + "*"*BOARD_SMALL_WIDTH + " " + "*"*BOARD_SMALL_WIDTH]*BOARD_SMALL_HEIGHT

Smallest (3) plates I found: 16*27 [units]:

This is slightly better than what was produced by the toy factory (20*30 [units], as measured by my notebook).

But keep in mind, how coarse my "units" are (~5mm). You can "digitize" better if you use millimeter paper, but such a problem would be more hard for SAT solver, of course.

What I also did: this problem required huge AMO1/ALO1 constraints (several thousands boolean variables). Naive quadratic encoding can't manage this, also, CNF instances growing greatly.

I used "commander" encoding this time. For example, you need to add AMO1/ALO1 constraint to 100 variables. Divide them by 10 parts. Add naive/quadratic AMO1/ALO1 for each of these 10 parts. Add OR for each parts. Then you get 10 OR result. Each OR result is "commander", like, commander of a squad. Join them together with quadratic AMO1/ALO1 constraint again.

I do this recursively, so it looks like a multi-tiered tree of "commanders". Also, changing these constants (5 and 10) influences SAT solver's perfomance significantly, probably, tuning is required for each type of task...

(The constants defines breadth and depth of a tree.)

    # naive/pairwise/quadratic encoding
    def AtMost1_pairwise(self, lst):
        for pair in itertools.combinations(lst, r=2):
            self.add_clause([self.neg(pair[0]), self.neg(pair[1])])

    # "commander" (?) encoding
    def AtMost1_commander(self, lst):
        parts=my_utils.partition(lst, 5)
        c=[]
        for part in parts:
            if len(part)<10:
                self.AtMost1_pairwise(part)
                c.append(self.OR_list(part))
            else:
                c.append(self.AtMost1_commander(part))
        self.AtMost1_pairwise(c)
        return self.OR_list(c)

    def AtMost1(self, lst):
        if len(lst)<=10:
            self.AtMost1_pairwise(lst)
        else:
            self.AtMost1_commander(lst)

    # previously named POPCNT1
    # make one-hot (AKA unitary) variable
    def make_one_hot(self, lst):
        self.AtMost1(lst)
        self.OR_always(lst)

( src )

---

→ [list of blog posts]