Каждую осень HR просит запланировать отпуска на следующий год. Обычно люди сразу берут между майскими, кто-то подбирает даны под день народного единства, а многие просто ставят на декабрь, чтобы потом двигать можно было.

А я задался вопросом - можно ли найти оптимальный отпуск под запросы и открыл VS Code\Jupiter с F# (пока оно еще работает). Всё живёт в Jupyter-ноутбуке с ядром .NET Interactive — да, F# умеет в ноутбуки, питонисты, не ревнуйте.

Правила игры на 2027

Коротко и без претензии на юридическую консультацию:

• 28 календарных дней, один кусок — не короче 14 дней подряд (ст. 125 ТК). Остальные 14 беру по одному.

• Праздники в отпуск не входят и продлевают его (ст. 120). Выходные — входят.

• Календарь 2027: праздники 1–8 января, 23 февраля, 8 марта, 1 и 9 мая, 12 июня, 4 ноября; переносы на 22 февраля, 3 и 10 мая, 14 июня, 5 ноября и 31 декабря; рабочая суббота 20 февраля. Новогодние каникулы есть у всех — считаем с 11 января.

• Деньги: за каждый календарный день отпуска платят годовой заработок ÷ 12 ÷ 29,3 (ст. 139), за каждый неотработанный рабочий день теряешь оклад ÷ рабочие дни месяца.

Для оклада 150 000 ₽:

Посмотрите на последнюю строку ещё раз. Суббота в отпуске приносит деньги. Вы ничего не теряете, а отпускные получаете.

Производственный календарь в коде

День — это просто номер d, считая с 11 января: 0, 1, 2, … 354. Все свойства дня считаются один раз и складываются в массивы, дальше модель только смотрит в них по индексу.

module Cal =
    let first, last = DateOnly(2027, 1, 11), DateOnly(2027, 12, 31)
    let days = last.DayNumber - first.DayNumber + 1
    let date (d: int) = first.AddDays d
    let day (ddMM: string) = DateOnly.ParseExact(ddMM + ".2027", "dd.MM.yyyy").DayNumber - first.DayNumber
    let show d = (date d).ToString "dd.MM"
 
    let private key (x: DateOnly) = x.ToString "dd.MM"
    let private holidays = set [ "23.02"; "08.03"; "01.05"; "09.05"; "12.06"; "04.11" ]
    let private movedDaysOff = set [ "22.02"; "03.05"; "10.05"; "14.06"; "05.11"; "31.12" ]
    let private workingSaturday = "20.02"
 
    let private isHoliday (x: DateOnly) = holidays.Contains(key x) || x.Month = 1 && x.Day <= 8
    /// нерабочий ли день: выходной, праздник или перенесённый выходной (кроме рабочей субботы)
    let isOff (x: DateOnly) =
        key x <> workingSaturday
        && (x.DayOfWeek = DayOfWeek.Saturday || x.DayOfWeek = DayOfWeek.Sunday || isHoliday x || movedDaysOff.Contains(key x))
 
    let holiday = Array.init days (date >> isHoliday)
    let off = Array.init days (date >> isOff)
    let workdays = [| for d in 0 .. days - 1 do if not off[d] then d |]
 
    /// 14 дней отпуска с дня start: праздники пропускаем, они продлевают отпуск
    let chunk start =
        if holiday[start] then None
        else
            let ds = seq { start .. days - 1 } |> Seq.filter (fun d -> not holiday[d]) |> Seq.truncate 14 |> Seq.toArray
            if ds.Length = 14 then Some ds else None
 
printfn $"Дней: {Cal.days}, рабочих: {Cal.workdays.Length}"
// Дней: 355, рабочих: 247

Что здесь происходит:

• Производственный календарь — три множества (set) строк. Праздники, переносы и одна рабочая суббота. Ключ — строка "dd.MM". Не очень эффективно, зато сверяется с постановлением правительства глазами за десять секунд.

• Выходные и праздники - не одно и то же. holiday — праздник: в отпуск не входит и продлевает его. off — любой нерабочий день: выходной, праздник или перенос. Путать их нельзя: суббота в отпуск входит и приносит деньги, а 23 февраля — не входит и не приносит ничего.

• Рабочая суббота 20 февраля проверяется первой и побеждает всё остальное. Государство дало, государство взяло.

• workdays — номера рабочих дней по порядку.

• chunk start — дни 14-дневного куска с началом start. Праздники внутри пропускаются, поэтому кусок через 8 марта длится 15 календарных дней. Начинать отпуск с праздника нельзя — None. Сверка с реальностью: 247 рабочих дней в 2027-м, как в официальном календаре. Значит, ничего не потеряли.

Деньги за день считаются тут же, по формулам из таблицы — и сразу в копейках. Это эффективнее и дальше пригодится:

/// копейки за день отпуска: отпускные минус потерянная зарплата (ст. 139: годовой ÷ 12 ÷ 29,3)
static member val MoneyPerDay : int64[] =
    let salary = 150_000m
    let workdaysInMonth =
        Array.init 12 (fun i ->
            let m = i + 1
            Seq.init (DateTime.DaysInMonth(2027, m)) (fun j -> DateOnly(2027, m, j + 1))
            |> Seq.filter (Cal.isOff >> not) |> Seq.length)
    Array.init Cal.days (fun d ->
        if Cal.holiday[d] then 0L
        else
            let lost = if Cal.off[d] then 0m else salary / decimal workdaysInMonth[(Cal.date d).Month - 1]
            int64 (Math.Round((salary / 29.3m - lost) * 100m)))

Праздник — ноль: за него не платят и не вычитают. Выходной — чистые отпускные. Будний день — отпускные минус дневная зарплата этого месяца. Вся таблица выше — это вот эти десять строк.

Перебор умирает на пятом дне

14-дневный кусок — это одна переменная: день начала. Прогоняем Cal.chunk по всем дням года — вариантов 336, максимум находится мгновенно.

Максимум денег — +13 897 ₽ за кусок 21 февраля — 7 марта. Максимум отдыха — 18 дней с 7 февраля: туда влезают и 22-е, и 23-е, и рабочая суббота.

А дальше 14 одиночных дней. Непраздничных дней в году 349. Выбрать из них пять — 41 922 588 819 вариантов. Выбрать четырнадцать — 3,5 · 10²⁴. До выхода в отпуск не досчитаем. Даже до пенсии.

Перебор можно оптимизировать — начинать перебор с дней, примыкающих к выходным, отсекать варианты по методу ветвей и границ, и еще много вариантов. Но писать это все сложно, даже с помощью ИИ.

На помощь приходит солвер

CP-SAT — бесплатный солвер из Google OR-Tools. Для .NET это обычный NuGet-пакет. Много лет подряд он собирает медали на MiniZinc Challenge — чемпионате солверов, есть и такой.

Работа с ним выглядит так: вы не пишете алгоритм. Вы описываете задачу — какие есть переменные, что им нельзя, что хочется максимизировать, — а солвер сам ищет ответ. Как SQL: пишешь «что», а не «как».

Ответ приходит с одним из статусов:

• Optimal — план найден, и доказано, что лучше не бывает;

• Feasible — план найден, но доказать оптимальность не успел (кончился лимит времени);

• Infeasible — доказано, что ограничения противоречат друг другу. Отпуска не будет. Доказательство — главное отличие от эвристик и генетических алгоритмов. Те говорят «вроде неплохо». CP-SAT говорит «лучше нельзя, вот гарантия».

Как он обходит 10²⁴ вариантов, не перебирая их? Три приёма, работающих одновременно:

• Распространение ограничений. Выбрал кусок 21 февраля — 7 марта? Все 14 дней внутри мгновенно вычёркиваются из кандидатов в одиночные дни. Одно решение тянет за собой сотни выводов.

• Обучение на конфликтах — от SAT в названии. Зашёл в тупик — солвер выясняет почему и запоминает причину как новое правило. В этот тупик он больше не зайдёт ни с какой стороны.

• Оценки сверху. Солвер умеет быстро посчитать «больше этого точно не получится» и отрезать целые ветки поиска, не заходя в них. Как это работает — расскажу ниже.

Плюс параллельность — солвер может запускаться на нескольких ядрах. На каждом ядре свой воркер со своей стратегией, и они делятся находками друг с другом.

Что CP-SAT не умеет — и это важно, потому что дальше вся статья — борьба с этими ограничениями:

• Только целые числа. Никаких float. Поэтому все деньги в модели — в копейках, int64.

• У каждой переменной — границы. «Целое от 0 до 136» — можно. «Целое какое-нибудь» — нельзя.

• Только линейные ограничения и линейная цель: суммы переменных с постоянными коэффициентами. 3·x + 5·y ≤ 10 — да. x² или x·y — формально есть AddMultiplicationEquality, но солвер его не любит и становится медленным и грустным.

• Цель одна. «Побольше отдохнуть и не потерять денег» — придётся упаковать в одно число.

• Худший случай всё равно экспоненциальный. Задача NP-трудная, чудес не бывает. Плохая формулировка может не решиться за разумное время — проверим на себе. Зато есть удобные готовые ограничения. Нам хватит самых простых:

• AddExactlyOne(xs) — ровно одна булева переменная из списка истинна;

• AddAtMostOne(xs) — не больше одной;

• AddLinearConstraint(expr, lo, hi) — линейное выражение в диапазоне [lo, hi];

• OnlyEnforceIf(lit) — включить ограничение, только если литерал истинен. Литерал — это булева переменная или её отрицание: x или not x. Есть и тяжёлая артиллерия — интервалы без пересечений (AddNoOverlap, для расписаний), маршруты (AddCircuit, для коммивояжёра), ресурсы (AddCumulative). Для расчёта отпуска они не нужны.

Подключаем

#r "nuget: Google.OrTools, 9.15.6755"

Модель для солвера: Переменные, ограничения, цель.

Переменные булевы:

• start[t] — 14-дневный кусок начинается в день t;

• single[d] — день d взят отдельно.

Ограничения:

• начало ровно одно (AddExactlyOne);

• отдельных дней ровно 14, в праздники их брать нельзя, и день не может быть одновременно в куске и отдельным (AddAtMostOne).

Деньги — линейная сумма: каждая переменная умножается на заранее посчитанные копейки. Календарь целиком уходит в коэффициенты, модель остаётся линейной.

Главная фишка: модель ничего не знает про лето, выходные и ваши хотелки. Она спрашивает у двух предикатов DateOnly -> bool:

type Rules =
    { Chunk: DateOnly -> bool    // каким дням разрешено быть в 14-дневном куске
      Single: DateOnly -> bool   // какие дни можно брать отдельными
      Budget: decimal option }   // деньги за отпуск не меньше стольких рублей

type VacationModel(rules: Rules) =
    let model = CpModel()
    let start, single = Dictionary<int, BoolVar>(), Dictionary<int, BoolVar>()
    let takes = Array.init Cal.days (fun _ -> ResizeArray<ILiteral>())   // день календаря -> какими кусками отпуска он забирается
    let terms = ResizeArray<LinearExpr>()
    let mayChunk = Array.zeroCreate<bool> Cal.days
 
    do
        // 14 дней подряд: ровно одно начало; кусок разрешён, если разрешён каждый его день
        for t in 0 .. Cal.days - 1 do
            match Cal.chunk t with
            | Some c when c |> Array.forall (fun d -> rules.Chunk (Cal.date d)) ->
                start[t] <- model.NewBoolVar $"start{t}"
                for d in c do
                    takes[d].Add start[t] // если день d забирается 14-дневным куском начатым в t, то добавляем переменную в список
                    mayChunk[d] <- true
                terms.Add(start[t] * Array.sumBy (fun d -> Plan.MoneyPerDay[d]) c)
            | _ -> ()
        model.AddExactlyOne(Seq.cast start.Values) |> ignore
 
        // 14 отдельных дней: в праздники нельзя (ст. 120), остальное решает предикат
        for d in 0 .. Cal.days - 1 do
            if not Cal.holiday[d] && rules.Single (Cal.date d) then
                single[d] <- model.NewBoolVar $"single{d}"
                takes[d].Add single[d]
                terms.Add(single[d] * Plan.MoneyPerDay[d])
        model.AddLinearConstraint(LinearExpr.Sum single.Values, 14L, 14L) |> ignore
 
        // день — либо в куске, либо отдельный, не оба сразу
        for t in takes do model.AddAtMostOne t |> ignore
 
    let money = LinearExpr.Sum terms
    do rules.Budget |> Option.iter (fun b -> model.AddLinearConstraint(money, int64 (b * 100m), Int64.MaxValue) |> ignore)

Доверяй, но проверяй. После каждого решения план пересчитывается обычным F#, без солвера. Не сошлось — исключение.

let plan = { m.Read solver with Optimal = (status = CpSolverStatus.Optimal); Seconds = sw.Elapsed.TotalSeconds }
if solver.Value m.Money <> int64 (plan.Money * 100m) || solver.Value m.Joy <> int64 plan.Joy then
    failwith "солвер и проверка разошлись"

Ни разу не сработало, но спать спокойнее.

Хочу максимум денег

let anyDays = { Chunk = (fun _ -> true); Single = (fun _ -> true); Budget = None }
let moneyPlan = show "Деньги" (solve anyDays (fun m -> m.Money))

11,3 секунды, оптимум доказан — и +85 570 ₽ за год.

Кусок 21 февраля — 7 марта, внутри три праздника. А оставшиеся 14 дней солвер разложил… по субботам и воскресеньям. Каждая по +5 119 ₽.

По документам я в отпуске 28 дней. По факту — 16. Руководитель в восторге, бухгалтерия в замешательстве, я в унынии.

Солвер продал выходные, так дорого, как смог.

И он прав: я просил деньги — я получил деньги. Солвер не жульничает, он находит дыры в ограничениях. Значит, надо научить его, что такое отдых.

Кайф = Σ len²

Просто посчитать дни отдыха нельзя: 14 отдельных пятниц с прилипшими выходными — это 42 дня отдыха. Ровно как шесть недель подряд. Но любой, кто был в отпуске, скажет: это совершенно разные 42 дня.

Поэтому я взял сумму квадратов длин кусков отдыха и назвал её кайфом.

• Склейка всегда выгодна: (a + b)² = a² + b² + 2ab. Две недели по 10 дней — кайф 200, одна по 20 — 400.

• Каждый следующий день дороже: десятый день подряд приносит 19 кайфа, двадцатый — 39. 42 дня одним куском — 1 764, 14 кусков по три — 126. В 14 раз меньше.

И важная оговорка: кусок без единого рабочего дня отпуска не считается. Выходной в отпуске — это не отдых, а бухгалтерская запись.

member p.Joy = p.Runs |> Seq.sumBy (fun (a, b) -> (b - a + 1) * (b - a + 1))

Как засунуть квадрат в линейную модель

У CP-SAT только линейные выражения. А у меня квадрат.

Первая попытка — честная. Заводим на каждый день целую переменную len[d] — сколько дней подряд я отдыхаю к концу дня d. Правило простое:

• отдыхаю — len[d] = len[d−1] + 1;

• работаю — len[d] = 0.

А где квадрат? Его не нужно считать. Сумма первых L нечётных чисел — это L²: 1 + 3 + 5 + … + (2L − 1) = L². Значит, день, который отдыхаем, приносит 2·len[d] − 1 кайфа, а рабочий — ноль. И это одна линейная формула на все дни: 2·len[d] − rest[d]. Для рабочего дня там 0 − 0.

В CP-SAT условие «если — то» записывается через OnlyEnforceIf: ограничение включается, только когда литерал истинен. Условный код (без правила «кусок из одних выходных не считается», чтобы не загромождать):

let maxLen = 28 + Cal.days - Cal.workdays.Length       // 136: длиннее отдых не бывает
let len = Array.init Cal.days (fun d -> model.NewIntVar(0L, int64 maxLen, $"len{d}"))

// rest[d] — отдыхаю ли в день d
let rest = Array.init Cal.days (fun d ->
    let r = model.NewBoolVar $"rest{d}"
    if Cal.off[d] then model.AddLinearConstraint(r, 1L, 1L) |> ignore                 // выходной — всегда
    else model.AddLinearConstraint(r - LinearExpr.Sum takes[d], 0L, 0L) |> ignore      // будний — если в отпуске
    r)

for d in 0 .. Cal.days - 1 do
    let prev = if d > 0 then len[d - 1] :> LinearExpr else LinearExpr.Constant 0L
    model.AddLinearConstraint(len[d] - prev, 1L, 1L).OnlyEnforceIf(rest[d]) |> ignore  // отдыхаю: len[d] = len[d−1] + 1
    model.AddLinearConstraint(len[d], 0L, 0L).OnlyEnforceIf(rest[d].Not()) |> ignore   // работаю: len[d] = 0

// 1 + 3 + 5 + … + (2L − 1) = L²
let joy = LinearExpr.Sum [ for d in 0 .. Cal.days - 1 -> len[d] * 2L - rest[d] ]

Две переменные на день, всё линейно. Красиво! И не работает… За минуту солвер нашёл кайф 1 296, а верхняя оценка застряла на 6 288 — в пять раз выше. Оптимум не доказан. Почему так?

Вещественное ослабление, или как солвер врёт себе во благо

Найти хороший план — полдела. Чтобы сказать «лучше нельзя», солвер должен доказать, что ни один из 10²⁴ вариантов не даёт больше. Перебирать их он не будет. Он схитрит.

Хитрость называется LP-ослабление (LP relaxation). Солвер на время забывает, что переменные целые: булева переменная может быть не только 0 или 1, а, скажем, 0,3. «Взять в отпуск треть понедельника». Такая вещественная задача — обычное линейное программирование (LP), решается быстро. А её оптимум не меньше настоящего: вещественных планов больше, чем целых, но все целые среди них. Это и есть верхняя оценка — те самые 6 288.

Дальше солвер ветвится: берет одну задачу ограничением «пусть понедельник 3 мая — 1», вторую такую же, но с нулем. Решает ослабление в каждой ветке и отрезает ветки, где оценка уже хуже найденного плана. Когда оценка опускается до найденного плана — оптимум доказан. Чем ближе ослабление к правде, тем быстрее сходится. Если ослабление врёт в пять раз — ждать придётся долго.

А цепочка len[d] врёт безбожно. В LP нет никакого OnlyEnforceIf, условие превращается в неравенство с большим коэффициентом (big-M), примерно так:

len[d] ≤ 136 · rest[d]                          // работаю → len = 0
len[d] ≤ len[d−1] + 1 + 136 · (1 − rest[d])     // отдыхаю → не больше вчера + 1

Подставим вещественное число. Беру в отпуск понедельник на 10%: rest = 0,1. Первое неравенство разрешает len до 13,6. Второе при 1 − rest = 0,9 вообще ничего не запрещает. Получаем: десятая часть дня отпуска даёт кусок длиной 13,6 и почти 27 кайфа. В реальном (целочисленном в нашем случае) мире за такой кусок пришлось бы отдать десяток дней отпуска. В вещественном — десятую часть понедельника. Размажьте 14 дней тонким слоем по всем будням года — и оценка улетает в космос. По сути солвер начинает тупо перебирать варианты, как наш код до него.

Квадрата не существует

(Есть ощущение, что никто не понял отсылки к Матрице)

Кусок отдыха однозначно задаётся своими рабочими днями: выходные и праздники прилипают сами. Значит, можно заранее перечислить все отрезки рабочих дней W[k..m] длиной до 28, для каждого заранее знать длину куска — а значит, и квадрат. Квадрат становится константой.

Три ограничения связывают куски с отпуском: слева рабочий день не в отпуске, справа тоже, каждый рабочий день отпуска накрыт ровно одним куском. Всё. Склейки получаются сами, правило «выходной — не отдых» — тоже само, без дополнительных ограничений.

let W = Cal.workdays
let possible (d: int) = rules.Single (Cal.date d) || mayChunk[d]
let runs =
    [| for k in 0 .. W.Length - 1 do
         for m in k .. min (k + 27) (W.Length - 1) do
             if W[k..m] |> Array.forall possible then
                 let from = if k > 0 then W[k - 1] + 1 else 0
                 let until = if m < W.Length - 1 then W[m + 1] - 1 else Cal.days - 1
                 k, m, until - from + 1, model.NewBoolVar $"run{k}_{m}" |]
do
    let covering = Array.init W.Length (fun _ -> ResizeArray<ILiteral>())
    for k, m, _, run in runs do
        for i in k .. m do covering[i].Add run
        if k > 0 then model.AddAtMostOne(Seq.append takes[W[k - 1]] [ run ]) |> ignore             // слева пусто
        if m < W.Length - 1 then model.AddAtMostOne(Seq.append takes[W[m + 1]] [ run ]) |> ignore  // справа пусто
    for i in 0 .. W.Length - 1 do                                    // ровно один кусок на рабочий день
        model.AddLinearConstraint(LinearExpr.Sum covering[i] - LinearExpr.Sum takes[W[i]], 0L, 0L) |> ignore
let joy = LinearExpr.WeightedSum(seq { for _, _, _, run in runs -> run }, seq { for _, _, len, _ in runs -> int64 (len * len) })

Плюс 6 538 новых переменных — по одной на каждый возможный кусок. И то, что не доказывалось за минуту, доказывается за 11–36 секунд — смотрите тайминги ниже.

У такого подхода нет проблемы, что LP-ослабление врет. Если run[k, m] = 0,1, то и кайфа он даёт ровно 0,1 · len², и будни покрывает на 0,1. Дробный план не умеет получать больше, чем платит. Ослабление почти совпадает с правдой — и доказательство сходится за секунды.

Больше переменных — быстрее решение. Для солвера важно не количество переменных, а сложность ограничений. Не что вы считаете, а как. Это самый ценный урок данной статьи.

Не беру отпуск в выходные

Закрываем лазейку. Модель не трогаем — меняем предикат:

let workday (x: DateOnly) = not (Cal.isOff x)
let weekdays = show "Деньги без выходных" (solve { anyDays with Single = workday } (fun m -> m.MoneyThenJoy))

MoneyThenJoy — сначала деньги, при равных деньгах — кайф. Зачем? Будни одного месяца стоят одинаково, планов с максимумом денег много, и дни могут лечь вразнобой, через день. Солверу всё равно, мне — нет.

Но цель у CP-SAT одна. Выход — упаковать две цели в одно число, как телефонная книга сортирует по фамилии, а при равной фамилии — по имени: деньги × N + кайф. Если N больше любого возможного кайфа, то копейка денег всегда перевесит весь кайф, и кайф решает только при равных деньгах.

Осталось найти N. Подбирать на глаз не надо — его даёт календарь: отдыхающих дней максимум 136 (28 отпуска + 108 выходных и праздников), значит, кайф не больше 136². Берём N = 136² + 1. Сначала я взял вес с запасом — «дней в году²». И солвер перестал доказывать оптимум за две минуты: лишние порядки в коэффициентах ему только мешают. Минимально достаточный вес — лучший.

13,3 секунды. Результат: −9 885 ₽ и 36 дней отдыха подряд, с 21 февраля по 28 марта.

Почему март? Потому что будний день в марте — самый дешёвый в году. Солвер не любит море в марте. Солвер любит скидки. А кайф склеил дни в одну полосу.

Хочу максимум кайфа

let joyPlan = show "Кайф" (solve anyDays (fun m -> m.JoyThenMoney))

20,1 секунды. 39 дней подряд, с 6 февраля по 16 марта. Кайф 1 521. Цена — −42 182 ₽.

Кайф дороговат.

Кайф в бюджете

Хочу максимум кайфа, но потерять не больше 9 885 ₽ — как в варианте «без выходных». Выходные брать можно.

Результат: те же 36 дней, те же деньги. Доказанный оптимум за 31,7 секунды. Почему? Суббота ради денег занимает место будня в длинном куске: 35 дней вместо 36 — минус 71 кайф. Не окупается.

Ладно, до −20 000 ₽. 32,5 секунды — 37 дней, −16 703 ₽. 37-й день стоит 6 818 ₽. Запомним эту цифру.

Хочу к морю

Март — оптимально по деньгам, но я хочу летом. Одна строка:

let isSummer (x: DateOnly) = x.Month >= 5 && x.Month <= 9
let summer = { anyDays with Chunk = isSummer }

Все десять оптимумов доказаны. Самая долгая задача — 36 секунд. Лето решается быстрее: вариантов 14-дневного куска меньше, искать проще. А дольше всего солвер думает, когда есть бюджет: ограничение на деньги сталкивает две цели лбами.

Солвер ставит кусок на 2–16 мая — ловит 9-е и перенесённое 10-е. «Лето» по версии солвера — это майские. И стоит оно 5 383 ₽ сверху.

Хочу только август? Chunk = fun x -> x.Month = 8. Пять секунд — кусок 16–29 августа, +75 163 ₽. Море, дача, сессия, «только не в отчётный период» — всё это предикаты. Модель не меняется ни на строчку. Вот ради этого всё и затевалось.

Все планы на одной картинке

Синий — будни в отпуске, голубой — выходные внутри отдыха, оранжевый — выходные, проданные ради денег. Денежные планы рассыпаются оранжевой сыпью по субботам. Всё остальное собирается в одну синюю полосу.

Сколько стоит кайф

Самое интересное. Прогоняем бюджет от +80 000 до −45 000 ₽ и для каждого ищем максимум кайфа. 28 задач, каждая — от долей секунды до 93 секунд, все оптимумы доказаны:

• Без потерь — 32 дня подряд. Бесплатно. Просто правильно расставить даты.

• Лучшие 10 тысяч в жизни — сразу за нулём: −9 885 ₽ дают 36 дней. +4 дня за десятку.

• Дальше — грабёж. 37 дней — при −20 тысячах, 38 — при −30, 39 — при −45.

• Лето — до трёх дней меньше при том же бюджете, потолок — 38 дней.

Глаза — свидетель ненадёжный, нужен второй. Возьмём точки, где я уже теряю деньги, и проведём через них параболу методом наименьших квадратов (Fit.Polynomial из Math.NET): дни ≈ 32,43 + 0,315·x − 0,004·x², где x — потеря в тысячах. R² = 0,95 — парабола объясняет 95% разброса точек, то есть кривая и правда загибается, а не мерещится.

Производная параболы — сколько дней даёт следующая тысяча. Перевернём её — и получим цену следующего дня: у нуля ~3 200 ₽, на −20 тысячах ~6 500 ₽, у самого потолка — под 13 600 ₽.

#r "nuget: MathNet.Numerics, 5.0.0"
let coef = Fit.Polynomial(xs, ys, 2)
for x in [ 0.0; 10.0; 20.0; 30.0 ] do
    printfn $"потеря {x:F0} тыс ₽: следующий день отдыха ≈ {1000.0 / (coef[1] + 2.0 * coef[2] * x):F0} ₽"

«Максимум кайфа» — плохая цель. Хорошая цель — точка, где кривая загибается. У меня это −10 тысяч и 36 дней подряд.

Выводы

1. Солвер найдёт лазейку лучше вас. Если он отправил вас в отпуск по субботам — это баг ваших ограничений, а не солвера.

2. Формулировка важнее железа. Одна и та же сумма квадратов: «не доказал за минуту» против «доказал за 11–36 секунд».

3. Проверяйте солвер независимым кодом. Всегда.

4. CP-SAT — обычный NuGet-пакет. Булевы переменные, AddExactlyOne, AddAtMostOne, линейная цель. Никакой магии.

Солвер нашёл оптимум. Осталось одно ограничение, которое на F# не выражается:

model.Add(manager.Approves plan)

Все графики построены с помощью Plotly.NET.Interactive

#r "nuget: Plotly.NET.Interactive, 5.0.0"

Код — в ноутбуке https://gist.github.com/gandjustas/52aadbf30d82ceed4b4cf0139157ac50. Вариант на C# для тех, кто не знает F# —https://gist.github.com/gandjustas/d8ce2d36df5633bec703c0b04adb23d3.

Мои ограничения чуть сложнее и модель тоже, но первый отпуск я уже планирую на март 2027 года. А вы уже сдали даты? Признавайтесь в комментариях, сколько денег оставили на столе.

Даты в статье — не финансовая рекомендация. Перед отпуском проконсультируйтесь с бухгалтерией.

Заключение

Солверы (CP, LP, SAT) — очень крутые инструменты, о которых программисты почти забыли в эпоху ML и AI. Но они все еще могут решать множество задач гораздо эффективнее, чем рукопашный код и не требуют обучения или валидации человеком.

В каждом пакетном менеджере прячется небольшой CP-солвер, который решает какие версии пакетов подобрать чтобы учесть все ограничения. А вывод типов, как в F#, TypeScript или Rust — это уже готовый солвер.

С помощью солверов можно решать бизнес-задачи: не только составление расписаний и графиков, но и оптимизация маршрутов (Задача коммивояжёра), распределение бюджетов, оптимизация производства. Добавьте этот инструмент в свою копилку.

Спасибо всем кто дочитал до конца.