--- date: May 23, 2026 author: Fabien Chouteau tags: lang --- # Розв'язання судоку за допомогою AdaSAT > Фаб'єн Шуто, 8 липня 2025 р. > > Переклад статті з [AdaCore Blog](https://www.adacore.com/blog/solving-sudoku-with-adasat). У бібліотеці семантичного аналізу Ada від AdaCore, Libadalang, система типів представлена як набір логічних обмежень або рівнянь, написаних мовою програмування, орієнтованою на предметну область (DSL), з нашого метакомпілятора [Langkit](https://github.com/AdaCore/langkit). Ці обмеження моделюють, як типи пов'язані один з одним (наприклад, сумісність, перетворення, підтипи тощо). Замість реалізації процедурної або на основі правил перевірки типів, Libadalang перетворює ці обмеження в логічну форму та вирішує їх декларативно. Це забезпечує більшу гнучкість, зручність підтримки та формальне мислення. Спочатку розв'язання обмежень у Libadalang здійснювалося кількома спеціалізованими розв'язувачами, створеними спеціально для різних частин системи типів. Ці реалізації були адаптованими та дещо нестабільними. Кілька років тому новіший підхід замінив їх на серверну частину, засновану на розв'язувачах на основі задовільності (SAT), яка пропонує кілька переваг: * Надійність та продуктивність: Сучасні розв'язувачі SAT є високооптимізованими та можуть ефективно обробляти великі набори обмежень. * Формалізм: Вираження обмежень у вигляді формул пропозиційної логіки краще узгоджується з інструментами верифікації та формальними методами. * Гнучкість: Інфраструктура на основі SAT може розвиватися разом із розвитком системи типів, без переписування всієї логіки розв'язувача. Якщо вам цікава ця робота, команда опублікувала статтю на 21-му Міжнародному семінарі з Satisfiability Modulo Theories (теорій задовільності за модулем): застосування SMT у метакомпіляторі: [Application of SMT in a Meta-Compiler: A Logic DSL for Specifying Type Systems](https://ceur-ws.org/Vol-3429/short7.pdf) [Ромен Беге, Рафаель Аміяр]. Розв'язувач SAT, який використовується Libadalang, реалізовано в окремій бібліотеці під назвою [AdaSAT](https://github.com/AdaCore/AdaSAT). У цій публікації блогу я використаю методи, описані в статті Інес Лінс та Джоела Уакніна, для реалізації розв'язувача судоку за допомогою AdaSAT: [Sudoku as a SAT Problem](https://sat.inesc-id.pt/~ines/publications/aimath06.pdf). ## Судоку як задача SAT Під час розв'язання тестів SAT задача виражається в кон'юнктивній нормальній формі (КНФ), кон'юнкції (логічне І) кількох речень, які є диз'юнкціями (логічне АБО) одного або кількох літералів. Наприклад, наступна формула складається з 3 речень: (A ∨ B) ∧ (¬A ∨ C ∨ D) ∧ (¬B ∨ ¬C) Розв'язувач SAT систематично оцінює комбінації значень істинності, щоб встановити, чи всі речення можуть бути виконані одночасно, або, якщо виникають суперечності, визначаючи задовільність задачі загалом. ### Як можна змоделювати головоломку судоку таким чином? Нам потрібно побудувати велику формулу для розв'язувача SAT з різними умовами, що обмежують головоломку. Щоб виразити речення, ми вважатимемо, що кожне можливе значення для кожної клітинки є змінною (9 змінних на клітинку). Наприклад, змінна V111 покаже, чи містить верхня ліва клітинка значення 1, V568, чи містить клітинка в рядку 5, стовпці 6 значення 8 тощо. З 9 стовпцями, 9 рядками та 9 можливими значеннями на клітинку ми маємо 729 змінних. Після того, як ми пропустимо формулу через розв'язувач, ми отримаємо логічне значення для кожної з цих змінних. Має бути рівно 81 значення True, по одному для кожної клітинки. Наприклад, якщо значення в рядку 1, стовпці 1 дорівнює 9, то за правилами судоку виконуються такі умови: 1. V119 is True V119 є правдою 2. V1j9 є хибним для j /= 1 (немає інших 9 у стовпці 1) 3. Vi19 є хибним для i /= 1 (немає інших 9 у рядку 1) 4. Vij9 є хибним, коли i в 2..3 та j в 2..3 (немає інших 9 у верхній лівій сітці з 9 квадратів) ### Як нам обмежити проблему? Спочатку ми розглянемо одну комірку (наприклад, 1, 1), у нас є 9 різних змінних: V111, V112, V113, …, V119. Ми знаємо, що принаймні одна з цих змінних має бути істинною, оскільки клітинка містить принаймні одне значення. V111 ∨ V112 ∨ V113 ∨ V114 ∨ … ∨ V119 Це дає нам один вираз для формули. Давайте подивимося, як його оголосити. В AdaSAT змінні ідентифікуються додатними числами за допомогою типу `AdaSAT.Variable`, тому ми визначаємо функцію для кодування `Vi,j,d` (де `i` – рядок, `j` – стовпець, а `d` – значення комірки) в унікальне значення ідентифікатора `AdaSAT.Variable`. ```ada type Col_Id is range 1 .. 9; type Row_Id is range 1 .. 9; type Value is range 1 .. 9; function V (I : Row_Id; J : Col_Id; D : Value) return AdaSAT.Variable is (81 * (AdaSAT.Variable (I) - 1) + 9 * (AdaSAT.Variable (J) - 1) + AdaSAT.Variable (D)); ``` V111 буде змінною з ідентифікатором 1, V112 буде змінною з ідентифікатором 2, V568 буде змінною з ідентифікатором 377, V999 – змінною з ідентифікатором 729. AdaSAT надає об'єкти для легкого створення речень та формул ```ada Clause : AdaSAT.Builders.Clause_Builder; Formula : AdaSAT.Builders.Formula_Builder; ``` Для кожної клітинки ми додаємо до формули речення, як описано вище: ```ada for I in Row_Id loop for J in Col_Id loop for D in Value loop -- Denotes (at least) one of the 9 digits (1 clauses) Clause.Add (+V (I, J, D)); end loop; Formula.Add (Clause.Build); end loop; end loop; ``` Далі, ми також знаємо, що лише одна з цих змінних може бути істинною, оскільки кожна клітинка може містити лише одне значення. Існує оптимізований спосіб вказати «не більше одного з» в AdaSAT. Він вимагає, щоб ідентифікатори змінних були суміжними, що стосується ідентифікаторів змінних можливих значень однієї клітинки. Наприклад, ідентифікатори від 1 (V111) до 9 (V119) для верхньої лівої клітинки. ```ada for I in Row_Id loop for J in Col_Id loop Formula.Add_At_Most_One (V (I, J, 1), V (I, J, 9)); end loop; end loop; ``` Ви зрозуміли ідею. Потім нам потрібно додати речення, які вказують, що всі комірки в рядку та стовпці мають різні значення, і що всі комірки в квадраті 3x3 також мають різні значення. Я не копіюватиму тут повний код; ви можете переглянути репозиторій GitHub для отримання додаткової інформації: [github.com/Fabien-Chouteau/sudoku_sat](https://github.com/Fabien-Chouteau/sudoku_sat). ## Як вказати вхідну сітку? Але щоб розв'язати сітку, нам все одно потрібно вказати відомі значення з початку нашої головоломки судоку. Для цього ми просто додаємо для кожного відомого значення умовне утримання, яке стверджує, що відповідна змінна є істинною: ```ada Input_Grid : constant Grid := [[0, 2, 0, 0, 0, 0, 0, 0, 0], [0, 0, 0, 6, 0, 0, 0, 0, 3], [0, 7, 4, 0, 8, 0, 0, 0, 0], [0, 0, 0, 0, 0, 3, 0, 0, 2], [0, 8, 0, 0, 4, 0, 0, 1, 0], [6, 0, 0, 5, 0, 0, 0, 0, 0], [0, 0, 0, 0, 1, 0, 7, 8, 0], [5, 0, 0, 0, 0, 9, 0, 0, 0], [0, 0, 0, 0, 0, 0, 0, 4, 0]]; for I in Row_Id loop for J in Col_Id loop if Input_Grid (I, J) /= 0 then Clause.Add (+V (I, J, Value (Input_Grid (I, J)))); Formula.Add (Clause.Build); end if; end loop; end loop; ``` І нарешті, ми можемо попросити AdaSAT розгадати нашу головоломку ось так: ```ada declare First_Variable_Id : constant AdaSAT.Variable := V (Row_Id'First, Col_Id'First, Value'First); Last_Variable_Id : constant AdaSAT.Variable := V (Row_Id'Last, Col_Id'Last, Value'Last); Model : AdaSAT.Model (First_Variable_Id .. Last_Variable_Id); begin Model := [others => AdaSAT.Unset]; if AdaSAT.Helpers.DPLL_Solve (Formula.Build, Model) then Put_Line ("PASS"); else Put_Line ("FAIL"); end if; ``` ***Модель*** – це масив змінних типу `Variable_Value`, які можуть мати значення `True`, `False` або `Unset`. Кожен елемент масиву відповідає одній із 729 змінних, що використовуються в нашій формулі. Ми ініціалізуємо всі значення як `Unset`. І нарешті, ми викликаємо `DPPL_Solve` (DPLL – назва алгоритму [wikipedia:DPLL_algorithm](https://en.wikipedia.org/wiki/DPLL_algorithm)). Функція повертає значення `True`, якщо формула задовільна, що завжди має бути так, оскільки головоломка судоку завжди задовільна (за умови коректної вхідної сітки), а алгоритм DPLL називається «повним». Після цього масив `Model` містить значення `True` або `False` для кожної зі змінних. Ми можемо отримати значення для кожної комірки, переглянувши змінні, встановлені на `True`. ```ada Model (V (Col, Row, Val)) = AdaSAT.True ``` Отже, ось як ми друкуємо сітку результатів: ```ada Put_Line ("-------------------------"); for Row in Row_Id loop Put ("|"); for Col in Col_Id loop for Val in Value loop if Model (V (Row, Col, Val)) = AdaSAT.True then Put (Val'Img); end if; end loop; if Col mod 3 = 0 then Put (" |"); end if; end loop; New_Line; if Row mod 3 = 0 then Put_Line ("-------------------------"); end if; end loop; Put_Line (AdaSAT.Image (Model)); ``` Результат: ``` ------------------------- | 1 2 6 | 4 3 7 | 9 5 8 | | 8 9 5 | 6 2 1 | 4 7 3 | | 3 7 4 | 9 8 5 | 1 2 6 | ------------------------- | 4 5 7 | 1 9 3 | 8 6 2 | | 9 8 3 | 2 4 6 | 5 1 7 | | 6 1 2 | 5 7 8 | 3 9 4 | ------------------------- | 2 6 9 | 3 1 4 | 7 8 5 | | 5 4 8 | 7 6 9 | 2 3 1 | | 7 3 1 | 8 5 2 | 6 4 9 | ------------------------- ``` Як бачите, AdaSAT справді простий у використанні та може бути легко інтегрований у ваш власний проект, наприклад, якщо вам потрібно [запланувати спортивні заходи](https://www.satisfiability.org/SAT04/programme/74.pdf). Якщо ви новачок у SAT і хочете дізнатися більше, рекомендую це відео: [A Peek Inside SAT Solvers - Jon Smock](https://youtu.be/d76e4hV1iJY). ----