Zython (python-wrapper для minizinc) после года разработки

Более года назад я начал создавать python обёртку для minizinc. Minizinc — это, пожалуй, самый популярный инструмент программирования в ограничениях. Вы можете найти больше информации о том, что такое программирование с ограничениями, minizinc, и для чего они используются в предыдущей статье.

При своём первом релизе в январе 2021 года zython поддерживал объявление переменных и параметров, массивы, все типы решения satisfy, maximize, minimize, (соответственно для поиска решения, которое удовлетворяет заданным условиям, или которое максимизирует/минимизирует заданную величину), множество предопределенных операций и ограничений (и, конечно, CI). Он мог решить множество моделей, некоторые из которых были указаны в документации.

Но также в zython отсутствовали некоторые функции minizinc: поддержка вещественного типа (float), а так же множеств и типов перечеслений (enum). Я начал с поддержки float.

Добавление поддержки вещественного типа данных

Этот тип кажется естественным и необходимым для «обычных» парадигм программирования. Я не могу назвать ни одного популярного языка без его поддержки (пожалуй, только brainfuck). Но в программировании с ограничениями данный тип не так важен, значительное число задач можно решить обойдясь только целыми числами, многие алгоритмы разрабатывались только для дискретных моделей.

Дело в том, что в парадигме программирования в ограничениях, программист задаёт не алгоритм решения, а описывает модель, решение находит специальная программа-решатель (solver). Не каждая такая программа поддерживает тип float (может быть, даже не большинство из них). Например, solver по умолчанию gecode не поддерживает их полностью, поэтому необходимо было добавить способ, которым пользователь мог бы указать "решатель" (конечно, я понял это только после того, как я реализовал переменные с плавающей запятой).

Давайте посмотрим, как вы можете использовать переменную с плавающей запятой, решив простое уравнение:

import zython as zn


class Model(zn.Model):    
  def __init__(self, a, b, c, d, e, f):        
    self.x = zn.var(float)        
    self.constraints = [a ** 5 * self.x + b ** 4 * self.x +
                        c ** 3 * self.x + d ** 2 * self.x +
                        e * self.x + f == 0]
    
m = Model(2, 3, 4, 5, 6, 7)
result = m.solve_satisfy(solver="cbc")
print(result["x"])  # -0.03365384615384615

Перечисления (enum) и множества (set)

Добавление перечислений и множеств было более сложной задачей: я начал с добавления перечислений, потом понял, что без множеств они совершенно бесполезны, и начал добавлять множества. Эта задача привела к масштабному рефакторингу (который ещё не совсем завершён), но и улучшила код, а главное — теперь каждый может использовать перечисления и наборы в zython. Ниже я приведу пример из документации библиотеки:

Давайте представим, что вам предстоит сразиться с Майком Тайсоном (не волнуйтесь, у вас есть неделя на подготовку). Вы должны выучить несколько боксерских приемов, каждый из них имеет силу, но вы должны потратить некоторое время, чтобы выучить его, и немного денег, чтобы нанять тренера.

Приём	Power	Time to learn	Money to learn
Джеб(jab)	1	1	3
Кросс(cross)	2	2	3
Апперкот(uppercut)	1	1	3
Оверхенд(overhand)	2	2	2
Хук(hook)	3	1	1

Модель для нахождения наиболее оптимальных ударов:

import enum
import zython as zn


class Moves(enum.Enum):
    jab = enum.auto()
    cross = enum.auto()
    hook = enum.auto()
    uppercut = enum.auto()
    slip = enum.auto()


class Model(zn.Model):
    def __init__(
            self,
            moves,
            time_available: int,
            money_available: int,
            power: list[int],
            time: list[int],
            money: list[int],
    ):
        self.time_available = time_available
        self.money_available = money_available
        self.power = zn.Array(power)
        self.time = zn.Array(time)
        self.money = zn.Array(money)
        self.to_learn = zn.Set(zn.var(moves))
        self.constraints = [
            zn.sum(self.to_learn, lambda move: self.time[move])
                < self.time_available,
            zn.sum(self.to_learn, lambda move: self.money[move])
                < self.money_available,
        ]


model = Model(
    Moves,
    5,
    10,
    [1, 2, 1, 2, 3],
    [1, 2, 1, 3, 1],
    [3, 4, 3, 2, 1],
)
result = model.solve_maximize(
    zn.sum(model.to_learn,
           lambda move: model.power[move])
)
print(f"Moves to learn: {result['to_learn']}, "
      f"power: {result['objective']}")

Другие изменения

Два описанных выше изменения не единственные, которые были добавлены в zython. Я добавил поддержку increasing, decreasing и allequal ограничений, параметр except_0 для ограниченияalldifferent. В прошлом году была выпущена новая версия Python, так что теперь zython поддерживает cpython 3.7 - 3.10. Так же было добавлено предупреждение (warning) на случай, если minizinc не найден в $PATH, я надеюсь, что данное изменение поможет в установке и интеграции zython в ваш код.

Вывод

Этот год был непростым (ну не только для меня, для всех), но мне как-то удалось найти время, чтобы улучшить zython, который становится все лучше и лучше с каждой версией[citation needed]. Это интересный опыт, и если вы когда-нибудь задумывались о запуске собственного проекта, вам стоит попробовать.