SAT решавачи¶

Судоку¶

Прикажимо сада како можемо искористити SAT решавач да решимо логичку загонетку Судоку. Ова загонетка захтева да се поље димензије \(9 \times 9\) попуни бројевима од 1 до 9 тако да су у свакој врсти, у свакој колони и у сваком троуглу димензије \(3 \times 3\) бројеви различити. Потребно је да кодирамо овај проблем коришћењем исказне логике. Означимо поља табеле са \(A_{ij}\) за \(1 \leq i, j \leq 9\). На сваком пољу може бити уписан било који број од 1 до 9. Основни искази ће бити означени са \(p_{ijv}\) за \(1 \leq i, j, v \leq 9\) и означаваће да је на пољу \(A_{ij}\) уписана вредност \(v\). Сваки од ових исказа може бити или тачан или нетачан. Потребно је да одредимо и везе између исказа које ће осигурати да ће њихове истинитосне вредности одређивати исправно решење загонетке Судоку.

За почетак, на сваком пољу треба да пише тачно једна вредност, што значи да за сваки пар \(i\) и \(j\) од 1 до 9 тачно једна од променљивих \(p_{ij1}, \ldots, p_{ij9}\) треба да има вредност тачно. Ово можемо кодирати следећим формулама:

Свака од ових импликација се може разбити на 8 мањих импликација, а затим се трансформацијом \(p \Rightarrow q\) у \(\neg p \vee q\) може добити следећи низ клаузула (генеришу се засебно клаузуле за свако \(i, j\) од 1 до 9):

На сличан начин треба да кодирамо услове да ће за сваку врсту \(i\) и сваку вредност \(v\) од 1 до 9 тачно једна променљива \(p_{i1v}, p_{i2v}, \ldots, p_{i9v}\) бити тачна, а затим услове да ће за сваку колону \(j\) и сваку вредност \(v\) од 1 до 9 тачно једна променљива \(p_{1jv}, p_{2jv}, \ldots, p_{9jv}\) бити тачна. На крају је потребно додати и услове за сваки од квадрата димензије \(3\times 3\). Сваки од 9 квадрата се може задати паром индекса \((k, l)\) између 0 и 2 (нпр. \((0, 0)\) означава горњи леви квадрат, а \((2, 2)\) доњи десни). За сваки квадрат \((k, l)\) и сваку вредност \(v\) између 1 и 9, тачно једна од променљивих

треба да буде тачна.

У загонетнки Судоку обично су задате вредности које су уписане у нека поља (и то често тако да се гарантује да се остала поља могу попунити на јединствен начин, тј. да постоји само једно тачно решење загонетке). Задате вредности једноставно кодирамо тако што решавачу дамо једночлане клаузуле које садрже само променљиве за које унапред знамо да су тачне. Наредни програм у језику C# кодира загонетку Судоку у формату DIMACS, који је стандардни улазни формат SAT решавача. Имплементација је прилично праволинијска. Потребно је пресликати променљиве \(p_{ijv}\) на бројеве од \(1\) до \(9^3 = 729\). Најједноставнији начин да се то уради је да се индекси \(ijv\) тумаче као цифре (увећане за 1) у основи 9, тј. да се свака променљива \(p_{ijv}\) преслика у број \((i-1) + 9\cdot (j-1) + 81\cdot (v-1) + 1\). Тада је и декодирање једноставно (и своди се на одређивање вредности цифара у основи 9):

Програм генерише 81 услов јединствености броја на пољу (за 81 поље), 81 услов јединствености броја у врсти (за 9 врста и по 9 бројева), 81 услов јединствености броја у колони (за 9 колона и по 9 бројева) и 81 услов јединствености броја у малом квадрату (за 9 малих квадрата и по 9 бројева). Сваки услов јединствености има једну позитивну клаузулу са 9 литерала и \({9 \choose 2} = 36\) негативних клаузула са по 2 литерала. Укупан број општих клаузула је зато \(4 \cdot 81 \cdot 37\), а њима се додају у једночлане клаузуле за свако унапред попуњено поље.

Коначна верзија програма дата је у наставку.

// ispisuje DIMACS zaglavlje
static void Zaglavlje(int BrojPromenljivih, int BrojKlauzula)
{
   Console.WriteLine("p cnf {0} {1}", BrojPromenljivih, BrojKlauzula);
}

// ispisuje klauzulu kao red u formatu DIMACS
static void Klauzula(int[] promenljive)
{
   foreach(int p in promenljive)
      Console.Write(p + " ");
   Console.WriteLine(0);
}

// kodira se uslov da je tacno jedna od promenljivih iz datog niza tacna
static void TacnoJedna(int[] promenljive)
{
    // klauzula koja dovodi do toga da bar jedna promenljiva iz niza
    // mora biti tacna
    Klauzula(promenljive);
    // klauzule koje za svaki par promenljivih zabranju da su obe
    // promenljive istovremeno tacne
    int[] kl = new int[2];
    for (int i = 0; i < promenljive.Length; i++)
        for (int j = i + 1; j < promenljive.Length; j++) {
            kl[0] = -promenljive[i];
            kl[1] = -promenljive[j];
            Klauzula(kl);
        }
}

// trojke (i, j, v) se kodiraju brojevima između 1 i 729
static int P(int i, int j, int v)
{
    return (i-1) + 9*(j-1) + 81*(v-1) + 1;
}

static void Main()
{
    // ucitavamo vrednosti na zadatim poljima
    List<int> zadate = new List<int>();
    string linija;
    while ((linija = Console.ReadLine()) != null)
    {
        string[] delovi = linija.Split();
        int i = int.Parse(delovi[0]);
        int j = int.Parse(delovi[1]);
        int v = int.Parse(delovi[2]);
        zadate.Add(P(i, j, v));
    }

    // stampamo DIMACS zaglavlje
    Zaglavlje(729, 4*81*37 + zadate.Count);

    // jedinstvenost vrednosti na svakom polju
    int[] promenljive = new int[9];
    for (int i = 1; i <= 9; i++)
       for (int j = 1; j <= 9; j++)
       {
           for (int v = 1; v <= 9; v++)
              promenljive[v-1] = P(i, j, v);
           TacnoJedna(promenljive);
       }

    // jedinstvenost vrednosti u svakoj vrsti
    for (int i = 1; i <= 9; i++)
       for (int v = 1; v <= 9; v++)
       {
           for (int j = 1; j <= 9; j++)
              promenljive[j-1] = P(i, j, v);
           TacnoJedna(promenljive);
       }

    // jedinstvenost vrednosti u svakoj koloni
    for (int j = 1; j <= 9; j++)
       for (int v = 1; v <= 9; v++)
       {
           for (int i = 1; i <= 9; i++)
              promenljive[i-1] = P(i, j, v);
           TacnoJedna(promenljive);
       }

    // jedinstvenost vrednosti u svakom kvadratu 3x3
    for (int k = 0; k < 3; k++)
       for (int l = 0; l < 3; l++)
          for (int v = 1; v <= 9; v++)
          {
              for (int a = 1; a <= 3; a++)
                 for (int b = 1; b <= 3; b++)
                     promenljive[3*(a-1)+(b-1)] = P(3*k+a, 3*l+b, v);
              TacnoJedna(promenljive);
          }

    // ispisujemo zadate promenljive
    foreach (int p in zadate)
    {
        int[] kl = {p};
        Klauzula(kl);
    }
}

Програм учитава унапред попуњене вредности. На пример, судоку загонетка:

. . . . . . . . 3
9 . . 3 . 2 . . .
6 8 . . . . . 5 .
1 . . . . 5 . . 9
5 . . 7 . . . 6 2
. . 4 . 1 . 5 3 8
3 4 . 8 . . 7 . .
. . 1 9 . . . . .
. 5 . . 7 3 . . .

се описује улазом:

1 9 3
2 1 9
2 4 3
2 6 2
3 1 6
3 2 8
3 8 5
4 1 1
4 6 5
4 9 9
5 1 5
5 4 7
5 8 6
5 9 2
6 3 4
6 5 1
6 7 5
6 8 3
6 9 8
7 1 3
7 2 4
7 4 8
7 7 7
8 3 1
8 4 9
9 2 5
9 5 7
9 6 3

Ако унесемо тај улаз када покренемо наш програм, добијамо исказну формулу sudoku1.cnf. Њеним решавањем помоћу SAT решавача добијамо задовољавајућу валуацију у којој су тачне следеће променљиве (све остале променљиве су нетачне):

  4  11  26  30  42  52  59  64  81
 90  91 103 114 125 128 138 151 158
169 175 183 191 203 216 224 231 235
244 259 267 279 281 293 301 314 318
329 342 344 352 367 373 384 390 404
408 420 432 436 442 458 461 473 484
492 503 505 518 531 534 547 553 560
575 579 590 601 607 613 630 632 645
650 662 673 683 687 699 703 720 724

Њиховим декодирањем добијамо следеће решење:

4 2 7 5 6 8 9 1 3
9 1 5 3 4 2 6 8 7
6 8 3 1 9 7 2 5 4
1 3 2 6 8 5 4 7 9
5 9 8 7 3 4 1 6 2
7 6 4 2 1 9 5 3 8
3 4 9 8 5 1 7 2 6
8 7 1 9 2 6 3 4 5
2 5 6 4 7 3 8 9 1

Вама препуштамо да сами напишете програм који ће приказати решење на основу решења добијеног од SAT решавача (програм треба да прочита решење, издвоји позитивне бројеве, декодира сваки од њих и да на основу тога формира и испише Судоку матрицу). Покушајте и да проширите формулу клаузулом која ће забранити добијање овог решења, да поново покренете SAT решавач и на тај начин да проверите да ли је ово решење јединствено.

Приметимо да је решавање Судоку загонетке свођењем на SAT веома декларативно. У програму смо само морали да опишемо (клаузулама) услове које решење мора да задовољава, а не и алгоритам како се до решења долази (SAT решавач је коришћењем веома ефикасних метода до тог решења дошао практично моментално).

Уместо да C# програм исписује излазну датотеку у формату DIMACS, која се онда шаље спољашњем SAT решавачу, могуће је SAT решавач покренути директно из C# програма преко API, које SAT решавачи обично нуде. Препуштамо ти да, на пример, инсталираш библиотеку Microsoft.Solver.Foundation (за то можеш користити NuGet), да проучиш како се она користи и да прилагодиш претходни програм тако да коришћењем ове библиотеке решава Судоку и приказује његово решење.