Optimize your diet via SMT

Are you struggling with what to eat today? Sometimes it is tough to decide, especially if you are hungry and find out there is nothing left in your fridge. I want to show you how it is possible to develop your dish planner and let the computer automatically optimizes your meals according to your daily nutrition intake.

For this program, we use SMT solvers. SMT solvers try to figure out which variable assignment satisfies a given logic formula. If a logic formula is satisfiable, it returns the assigned variables (in our case, your meals). PySMT is a very user-friendly interface for Python developers to encode and solve these kinds of SMT problems. In this post, I give you a small introduction into the field of Satisfiability Modulo Theories by providing you an SMT solver for figuring out what you could eat today.

Ethiopian cuisine

Steps

To solve this problem we have to do the following steps:

  1. Create a data set with your favorite dishes (dish name, number of calories, etc. etc.)
  2. Research your daily nutrition intake
  3. Encode a propositional logic formula based on this data set
  4. Let the SMT-solver decide what you should eat

1. Your personalized dish data set

To get your personalized data set, you must figure out how much nutritions are in your dishes. Thanks to the internet there are a variety of websites that provide you with a lot of recipes and the number of nutritions. My favorite ones are:

If you don’t have time to create your data set, I prepared a data set for you. There are many tastes out there, and so I just looked for the most famous food in the world. I ended up with a subset of dishes from CNN travel, and I hope you like it (a lot of them I didn’t know before).

2. Your daily nutrition intake

So how many calories should you eat today? Well, if you’re like me and have got already eaten 3 dishes, much chocolate and haven’t done any sport today, you should probably eat anything. But OK, let’s say the SMT solver should tell you how much you should eat tomorrow. For finding out the exact number of calories you can google for something like “calories calculator” and you may end up on:

On these websites, you can easily calculate your needed number of calories.

3. Formula Encoding

So how can we tell our overweight/optimization problem to our computer? Just with these 4 simple constraints:

(I) \(\sum_{i=1}^{|D|} x_i \cdot d_{i2} \leq (C + \alpha)\\\)

(II) \(\sum_{i=1}^{|D|} x_i \cdot d_{i2} \leq (C – \alpha)\\\)

(III) \(\sum_{i=1}^{|D|} x_i = k\)

(IV) \(\bigwedge\limits_{i}^E x_i = 0\)

\( D \) is a set of dishes. \( d_i \in D \) is a tuple \((dish, calories)\) and represents a single dish \(i\).

\(x \in \{ 0, 1 \}\) is an SMT variable that gets automatically assigned by the SMT solver. If \(x_i = 1\), then we will eat this dish the next day. \(k \in \mathbb{N}\) is the number of dishes per day.

\( C \in \mathbb{R} \) is the allowed number of daily calories. \( \alpha \in \mathbb{R} \) is the allowed deviation of \(C\).

\(B\subseteq \mathbb{N}\) is a set of disabled dish indices for the next calculation.

(I) and (II) make sure that our dishes give us the predefined number of calories. (III) makes sure that we get \(k\) dishes per day. (IV) allows us to exclude specific dishes for the next day.

4. Coding

You can find the full code in my GitHub-Repository. This method builds from lines 15 – 53, all the constraints from Section 3. The SMT solving happens at line 55. If a solution is found, it returns the dishes for cooking.

def nutrition_calculator(dishes, number_of_calories, number_of_dishes, disabled_dishes = [], alpha = 100):
    '''
        This method creates a dish plan based on the daily allowed calories
        and the number of dishes.
        Args:
            dishes, pandas data frame. Each row looks like this: (dish name, calories, proteins).
            number_of_calories, the daily number of calories.
            number_of_dishes, the daily number of dishes.
            disabled_dishes, list of row indizes from dishes which are not allowed in the current calculation.
            alpha, the allowed deviation of calories
        Returns:
            row indizes from dishes data frame. These dishes can be eaten today.
    '''
    # Upper and lower calory boundaries
    calories_upper_boundary = Int(int(number_of_calories + alpha))
    calories_lower_boundary = Int(int(number_of_calories - alpha))
    # List of SMT variables
    x = []
    # List of all x_i * d_i2
    x_times_calories = []
    # List of all x_i € {0,1}
    x_zero_or_one = []
    # List of disabled dishes
    x_disabled_sum = []
    for index, row in dishes.iterrows():
        x.append(Symbol('x' + str(index), INT))
        # x_i * d_i2
        x_times_calories.append(Times(x[-1], Int(row.calories)))
        # x_i € {0,1}
        x_zero_or_one.append(Or(Equals(x[-1], Int(0)), Equals(x[-1], Int(1))))
        # Disable potential dishes
        if index in disabled_dishes:
            x_disabled_sum.append(x[-1])
    x_times_calories_sum = Plus(x_times_calories)
    x_sum = Plus(x)
    if len(x_disabled_sum) == 0:
        x_disabled_sum = Int(0)
    else:
        x_disabled_sum = Plus(x_disabled_sum)
    formula = And(
        [
            # Makes sure that our calories are above the lower boundary
            GE(x_times_calories_sum, calories_lower_boundary),
            # Makes sure that our calories are below the upper boundary
            LE(x_times_calories_sum, calories_upper_boundary),
            # Makes sure that we get number_of_dishes dishes per day
            Equals(x_sum, Int(int(number_of_dishes))),
            # Makes sure that we don't use the disabled dishes
            Equals(x_disabled_sum, Int(0)),
            # Makes sure that each dish is maximal used once
            And(x_zero_or_one)
        ]
    )
    # SMT solving
    model = get_model(formula)
    # Get indizes
    if model:
        result_indizes = []
        for i in range(len(x)):
            if(model.get_py_value(x[i]) == 1):
                result_indizes.append(i)
        return result_indizes
    else:
        return None

Extensions & More

We can easily add two further constraints to support e.g. proteins in our encoding:

(V) \(\sum_{i=1}^{|D|} x_i \cdot d_{i3} \leq (P + \beta)\\\)

(VI) \(\sum_{i=1}^{|D|} x_i \cdot d_{i3} \leq (P – \beta)\\\)

\( P \in \mathbb{R} \) is the allowed number of proteins. \( \beta \in \mathbb{R} \) is the allowed deviation of \(P\). Don’t forget to update our set of dishes \(D\) and extend our tuple \(d_i\) to \((dish, calories, proteins)\).

If you want to learn more about SMT solving, check out the following links: