Assume False

Recreating Recipes Using SMT

z3

python

draft

This post is a draft, so it will likely change in the future. Also, I make no guarantees that the post is currently coherent, legible, or enjoyable to read. Read at your own risk :)

I love snacks, in fact I love them so much that I have attained the holy status of “snack monster” in my household. If my wife and I go on roadtrips, we usually end up buying our own bags of snacks and labelling them so that I don’t accidentally eat all the snacks before she gets some. Unfortunately, all this snacking comes at a cost. Literally. It costs money to buy snacks. This post is about how I used Z3, an SMT solver, to derive recipes for one of my favorite snacks.

The Target Snack

I will not out the exact snack here that I like, but there is a local business where I live that makes a protein bite style snack. If you google protein bite you will be greeted with many such snacks, but the basic idea of the snack is that you make a small uncooked ball of chocolate chips, peanut butter, honey, and protien powder and then you let it sit overnight to harden and shazam, you have yourself a snack.

These sound easy to make by yourself and typically they are, but I’ve tried making variations on my own that replicate the macros of the specific version available in my town, and they always end up gross. Likely I just have the wrong combination of ingredients and perhaps an incorrect mixing style. To correct the first problem of incorrect ingredient balance, I decided that I could write a program using the Z3 SMT solver and python to determine exactly what ratio of ingredients I could use!

Setting up an Example Problem

I haven’t really used an SMT solver for anything before, but I’m aware of the basic concept. You specify a formula, and Z3 determines if it can assign a specific value to each variable in the formula and have the formula result in true. If it can assign each variable a value, then the equation is said to be satisfied, or sat. If you can’t assign a variable a value, the equation is unsatisfied, or unsat.

For example, let’s say we have two floating point variables, \(x\) and \(y\). One possible formula we could make with these variables would be the following:

\[x \le y \wedge x \ge 5 \wedge y \le 6\]

An SMT solver asks itself if there is a possible assignment to \(x\) and \(y\) that would satisfy this equation. In this case, there is at least one possible assignment:

\[x = 5, y = 5\]

So Z3 returns sat and gives us these values for the assignment. If we change the formula slightly, we can see that there will not be a possible solution as \(x\) must be greater than 5 and \(y\) must be less than 4. Let’s see what happens when we pass this formula to the computer though.

\[x \le y \wedge x > 5 \wedge y < 4\]

Z3 returns “no solution” indicating that there is not a possible assignment of real number to \(x\) or \(y\) that can satify this formula. For reference, here’s how I encoded this problem into Z3 using python.

1
2
3
4
5
6
7
8
9
10

from z3 import *

x = Real('X')
y = Real('Y')

solve(And(And(x <= y, x >= 5), y <= 6))
# Output: [Y = 5, X = 5]

solve(And(And(x <= y, x > 5), y < 5))
# Output: no solution

Now Onto… Recipes?

I know what you’re thinking, “that’s really cool, but how in the world are you going to steal recipes with it?” Well, let’s try to talk through it together.

First, we need to define what a “recipe” is going to be to the SMT solver. This is going to be quite different from what we as humans view as a recipe, but it will maintain the same purpose.

Macro Triple
A triple \(\langle F, C, P \rangle\) where \(F\) is fat in grams, \(C\) is carbs in grams, and \(P\) is protein in grams.
Recipe
A combination of ingredients that when combined together result in a equivalently proportioned macro triple to the target recipe. We can represent a target recipe by the following equation. \[\sum_{i=0}^{n} k_i I_i = R\]
  • \(n\) is the number of ingredients,
  • \(I_i\) is the macro triple for each ingredient in the recipe
  • \(k_i\) is the coeffiecient that represents how many multiples of the ingredient we will use in the recipe, and
  • \(R\) is the macro triple for the target recipe.

To put this into the SMT solver we’re first going to need some constraints. First off, we need to make sure that the ingredient coeffiecients can’t be zero. If we had only two ingredients, and one of them had the same macros as the target recipe, then the SMT solver might just say that for our “recipe” we only need the one ingredient.

Ingredient Macros
Bacon \(b = \langle 10, 0, 2 \rangle\)
Eggs \(e = \langle 5, 0, 3 \rangle\)
\[R = \langle 20, 0, 4 \rangle\]

Given the above ingredients and the target recipe, then the SMT solver may just decide that assignments for \(k_b\) and \(k_e\) are 2 and 0.

\[\begin{align*} R = \langle 20, 0, 4 \rangle &= \sum_{i=0}^{n} k_i I_i\\ &= k_b b + k_e e \\ &= 2 \langle 10, 0, 2 \rangle + 0 \langle 5, 0, 3 \rangle \\ &= \langle 20, 0, 4 \rangle \\ \end{align*}\]

So our first constraint will be all \(k_i\) must be greater than 0.

\[\forall k, k > 0\]

At the moment I can’t think of any other constraints, so we’ll keep going from here.

Recipes As a Formula

Now that we have an abstract mathematical way of representing our recipes, we need to be able to encode these recipes as formulas that we can pass to Z3. Z3 has no concept of a macro triple, so we’ll need to figure out how we can tell the Z3 solver what that is. The good news is that it’s actually pretty easy. Basically, we just need to make the transformation from this:

\[\sum_{i=0}^{n} k_i I_i = R\]

To this:

\[\sum_{i=0}^{n} k_i F_i = R_F\\ \sum_{i=0}^{n} k_i C_i = R_C\\ \sum_{i=0}^{n} k_i P_i = R_P\\\]

All we are doing here is splitting out the ingredient triple into each of its separate components, and sharing the coeffiecients for each portion of the triple. We’re also going to make the transistion into coding land here.

Representing the Recipe in Python

We’ll start by creating a small python class to represent a macro triple. This will be the core data structure we’ll use to store the ingredients and the target recipe. Our class will have the three key data values we need, fat, carbs, and protien, and we’ll also add a name to each triple to differentiate triples from one another. We’ll use this later to generate names for our coeffiecients.

1
2
3
4
5
6

class MacroTriple:
    def __init__(self, name, fat, carbs, protien, gramsPerServing):
        self.name = name
        self.fat = fat / gramsPerServing
        self.carbs = carbs / gramsPerServing
        self.protien = protien / gramsPerServing

Next, we’ll need a way to generate our recipe formula. To do this we’ll need a list of MacroTriples for the ingredients and a MacroTriple for the target recipe. Based off our equations from above, we’ll need to generate a constraint for each ingredient (\(k_i > 0\)) and create the sum of coeffiecients that are equal to the target recipe.

To create all this we’ll introduce the concept of a Z3 solver. A solver is an object that we can add formulas to in different places and then we can call the check() method on the object to find satisfying assignments (or show that the formula is unsat).

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

import z3 

def recipeFormula(ingredients, target):
    s = z3.Solver()

    # initial constraint
    k0 = z3.Real(f"k_{ingredients[0].name}")
    s.add(k0 > 0)

    # initial equations 
    fatEquation = k0 * ingredients[0].fat
    carbsEquation = k0 * ingredients[0].carbs
    protienEquation = k0 * ingredients[0].protien

    # the rest of the equation and constraints 
    for ingredient in ingredients[1::]:
        kn = z3.Real(f"k_{ingredient.name}")
        s.add(kn > 0)

        fatEquation += kn * ingredient.fat
        carbsEquation += kn * ingredient.carbs
        protienEquation += kn * ingredient.protien

    # adding the final equations to the solver 
    s.add(fatEquation == target.fat)
    s.add(carbsEquation == target.carbs)
    s.add(proteinEquation == target.protien)

    return s

Now that we have this formula we can start generating recipes! First, we’ll need to set
up the list of ingredients.

Protien Bites Ingredients

Using the ingredients from the bag as a starting point, I grabbed all the macros of the ingredients from Cronometer, a macro tracking app, and I entered them into my python file.

1
2
3
4
5
6
7

Ingredients = [
        MacroTriple("Pb", 46.9, 25.0, 21.9, 100),
        MacroTriple("Honey", 0, 82.4, 0.3, 100),
        MacroTriple("Oats", 5.9, 68.7, 13.5, 100),
        MacroTriple("Protien", 0, 8, 20, 34),
        MacroTriple("ChocChips", 29.2, 66.7, 4.2, 100),
    ]

Next we need to set up the target recipe, which also is conveniently on the bag.

1

Target = MacroTriple("Bites", 5, 11, 4, 1)

Finally, we create the recipe formula, call check() on it to find a satisfying assignment and then print it to get our recipe!

1
2
3

formula = recipeFormula(Ingredients, Target)
formula.check()
print(formula.model())

When we run this we get:

1
2
3
4
5

[K_Pb = 8.915?,
 K_Oats = 11.399?,
 K_Honey = 0.5,
 K_Protien = 0.826?,
 K_ChocChips = 0.5]

We can read this recipe as 8.9 grams of peanut butter, 11.4 grams of oats, and so on. Right off the bat this recipe looks a little strange, and definitely gives me the sense that the peanut butter and oats will overpower everything else. To fix this I added two parameters to the recipeFormula function, min_bound and max_bound. These build off the same idea as the constraint we added early that all \(k\) must be greater than 0. Now we can use these bound variables to additionally specifiy that \(\texttt{min_bound} < k < \texttt{max_bound}\).

Final Bites

This brings me to the end of this blog post, but not to the end of my recipe generating. After I attempt to construct some of these recipes I’ll update this post with the results.

If you’d like to explore the code yourself, check it our on my GitHub.

Additional Optimizations to the Recipe Generator

In the US, ingredients on labels are listed in descending weight order, so we could add an additional constraint that the weight of all ingredients must be ordered to get more precise recipes.