Zig, SMT, Z3 un visādi citi termini
Nākamajā piektdienā, 24. jūlijā, sākas šīgada ICFP programmēšanas sacensību vīkends, mūsu komanda startē ik gadu un gaida šo notikumu tā kā daži gaida mesijas atnākšanu, tomēr es gan par to uzrakstīt saņemos reti: 2022, 2024 un viss.
Nedēļa pirms sacensībām ir lielisks brīdis tikt galā ar urdošu tieksmi: iemācīties mazliet apvaldīt kādu SMT solveri, jo visi feinākie sarežģītu uzdevumu risinājumi galu galā, izrādās, izmanto kādu no tiem.
SMT solveris
SMT risinātājs ir matemātiska programma/bibliotēka, kurai iedot kādas matemātiskas formulas un apgalvojumus, un tā izdos risinājumu vai pateiks, ka tāda nav. Risināmās problēmas (es nāku no pasaules, kur “problēma” un “uzdevums” ir sinonīmi, un tā ir šejienes redpolitika) piemērs varētu būt “x > 5, y < 10, x * y = 48; kāds varētu būt x un y veselos skaitļos?”, un, pateicoties super-sarežģītām matemātiskām teorijām, spēj risināt komplicētus uzdevumus apbrīnojamā ātrumā.
(piezīmes uz malām: varbūt esi dzirdējis par SAT solveriem, un tad te kaut kādi SMT solveri, kas tie ir? SAT solveri darbojas TIKAI ar loģiskiem apgalvojumiem, viņi neko nezina par skaitļiem un jēdzieniem “lielāks / mazāks”; tie meklē piemērotus risinājumus loģiskiem apgalvojumiem kā “x & ~y &z”, kur x, y un z ir tikai būla algebra, true/false. SMT slēdz klāt pārējo matemātikas mašinēriju, lai varētu risināt praktiskākus uzdevumus, bet, kas interesanti, apakšā viena no galvenajām sastāvdaļām vienalga ir SAT).
Es izmantošu Z3, kas, kaut arī nāk no Microsoft Research dzīlēm, tomēr ir pilnīgi atvērts, un pieejams visās tradicionālajās platformās gan C bibliotēkas formā, gan ar visādiem baindingiem augstāka līmeņa valodām.
Papildus Z3 bibliotēkai libz3.so, kuru es programmiski izmantošu vēlāk, projektā ir arī ekzešņiks z3, ar kuru var atrisināt kādus uzdevumus vnk tāpat, aprakstot savu problēmu. Noklusētais dialekts, kurā jāapraksta uzdevumi, saucas SMTLIB2 un tas ir lispīgs un ar kaudzi iekavām: ja neesi saskāries ar šādu pierakstu, tad tas var izskatīties neierasti.
Augstākminētais piemēriņš z3 uzdevuma valodā varētu izskatīties šādi (aiz semikola te un arī turpmāk ir koda komentāri):
(declare-fun x () Int) ; pasludina, ka X būs vesels skaitlis
(declare-fun y () Int) ; pasludina, ka Y būs vesels skaitlis
(assert (> x 5)) ; X jābūt > 5
(assert (< y 10)) ; Y jābūt < 10
(assert (= (* x y) 48)) ; X*Y jābūt 48
(check-sat) ; mēģina atrast atbildi
(get-model) ; parāda rezultātu
Saglabājot to failā un palaižot ar z3, būs šāds rezultāts, kurā solveris stāsta, ka, lūk, viena iespējamā atbilde: x=6, y=8:
$ z3 sample-48.smt
sat
(
(define-fun x () Int
6)
(define-fun y () Int
8)
)
Ja izrādīsies, ka atbildes nav (piemēram, samainot prasību, lai x*y = 47), unsat indicē, ka aprakstītajiem pieņēmumiem nav risinājuma (“unsatisfiable”):
$ z3 sample-47.smt
unsat
(error "line 7 column 11: model is not available")
Risināmā problēma
Risinot pagājušā gada ziemassvētku koda adventi, es iesprūdu 10. dienas otrajā daļā. Uzdevums, ļoti saīsināta piemēra izskatā: tev ir vairāki kloķi (piemērā — seši), katrs ieslēdz vienu vai dažādas lampiņas. Pirmais kloķis (3) ieslēgs lampiņu numur 3, otrais kloķis (1,3) ieslēgs lampiņas nr 1 un 3, utt:
(3) (1,3) (2) (2,3) (0,2) (0,1) {3,5,4,7}
Un nepieciešams paraustīt šos kloķus tā, lai — {3,5,4,7} — pirmā lampiņa tiktu ieslēgta trīs reizes, otrā — piecas, trešā — četras un pēdējā — septiņas. Šo konkrēto piemēru varētu atrisināt arī ar vieglu pārlasi, atrodot, ka optimāls variants būtu paraustīt (3) vienreiz, (1,3) trīsreiz, (2,3) trīsreiz, (0,2) vienreiz un (0,1) divreiz, tomēr īstā uzdevuma parametri ir tādi, ka optimālo klikšķu skaita meklēšana ar kādu pārlases variāciju būs stundām ilga, un atbildei jāatrisina kādi simtseptiņdesmit šādi uzdevumi:
(0,1,2,5,6,7,8) (1,4,6,7,8) (0,5,7) (0,1,2,6,7) (0,1,2,3,5,7,8) (0,1,5,7) (0,1,3,7,8)
{138,150,10,13,17,127,25,155,38}
Šis būs brīnišķīgs uzdevums, ko iedot z3 solverim.
Risinājums SMTLIBā
Lai katram slēdzītim atbilst viena kastīte, kas saturēs skaitu, cik reizes tas tiks paraustīts, x1…x7:
(declare-fun x1 () Int) ; x1 (0,1,2,5,6,7,8)
(declare-fun x2 () Int) ; x2 (1,4,6,7,8)
(declare-fun x3 () Int) ; x3 (0,5,7)
(declare-fun x4 () Int) ; x4 (0,1,2,6,7)
(declare-fun x5 () Int) ; x5 (0,1,2,3,5,7,8)
(declare-fun x6 () Int) ; x6 (0,1,5,7)
(declare-fun x7 () Int) ; x7 (0,1,3,7,8)
Papildus jāpasludina, ka šie skaitļi būs lielāki vai vienādi par nulli, citādi risinātājs atradīs kādus negatīvus skaitļus, bet mums nederēs risinājumi, kur kloķīši raustīti negatīvu skaitu reižu:
; ...
(assert (>= x1 0))
(assert (>= x2 0))
(assert (>= x3 0))
(assert (>= x4 0))
(assert (>= x5 0))
(assert (>= x6 0))
(assert (>= x7 0))
Tagad ķēpīgākais. Mums ir deviņas lampiņas, un katru ieslēdz kāds konkrēts slēdzītis, piemēram, pirmo lampiņu ieslēdz kloķīši 1, 3, 4, 5, 6 un 7, un kopsummai jābūt 138, un jā, es šo rakstīju ar roku:
; ...
(assert (= 138 (+ x1 x3 x4 x5 x6 x7))) ; 0
(assert (= 150 (+ x1 x2 x4 x5 x6 x7))) ; 1
(assert (= 10 (+ x1 x4 x5))) ; 2
(assert (= 13 (+ x5 x7))) ; 3
(assert (= 17 x2)) ; 4
(assert (= 127 (+ x1 x3 x5 x6))) ; 5
(assert (= 25 (+ x1 x2 x4))) ; 6
(assert (= 155 (+ x1 x2 x3 x4 x5 x6 x7))) ; 7
(assert (= 38 (+ x1 x2 x5 x7))) ; 8
(check-sat)
(get-model)
Nu var laist galā sanākušo skriptu un priecāties par rezultātu, 0, 11, 112, 8, 17, 5, 2, kopā 155 slēdzīšu paraustīšanas reizes:
$ z3 aoc.z3
sat
(
(define-fun x4 () Int
0)
(define-fun x7 () Int
11)
(define-fun x6 () Int
112)
(define-fun x1 () Int
8)
(define-fun x2 () Int
17)
(define-fun x3 () Int
5)
(define-fun x5 () Int
2)
)
Izrādās, ka tas šai gadījumā ir arī optimālais rezultāts, bet kā varētu pārliecināties, ka labāku nav? Pirmais risinājums vēl nezina, vai atbilde ir optimāla, bet, zinot vienu labu atbildi, mēs varam pievienot vēl vienu assertu, un tādā veidā pasludināt, ka mums interesē tikai labāki rezultāti, un laist meklēšanu vēlreiz.
; ...
(assert (< (+ x1 x2 x3 x4 x5 x6 x7) 155) ; UNSAT
; ...
Risinājums dabā
Kā jau minēju, lai pabeigtu koda adventes desmito dienu, šādu atrisināmo uzdevumu ir simtu septiņdesmit, un šis risinājums, ar roku rakstīt z3 skriptu, won’t cut it.
Bet, šos visus assertus var arī veidot programmiski, izmantojot Z3 bibliotēku savā iemīļotajā programmēšanas valodā.
Es ķēros pie Zig. Man pēdējā laikā sanāk daudz laika pavadīt zema līmeņa C pasaulē un ARM dzelžu un SDK izpētē, un jau biju dzirdējis, ka Zig ir ļoti dzelžiem pietuvināta programmēšanas valoda, kas, among other things, ļauj super-viegli sadarboties ar C bibliotēkām (tu tikai parādi programmai z3.h hēdera failu, un tā to ielasa un bez liekas runas izveido visas datu struktūras pieejamas un uzreiz lietojamas). Tai ir eksplicīts un manuāls atmiņas menedžments, kurš mani nekaitina!
Te ir mans risinājums: https://github.com/einars/advent-of-code/blob/main/2025.10/src/main.zig, jau atzīmētas ir rindiņas, kuras attiecas uz paša solvera veidošanu.
Detaļās baigi neiešu, tā jau paldies, ka tik tālu izlasīji. Zig bibliotēkas izsaukumi kodā sākas ar c.Z3_, un tās lietošana ir mazliet verbosa. Lai definētu X, vispirms nepieciešams izveidot abstraktu simbolu ar Z3_mk_string_symbol. Tikai pēc tam var izveidot pašu kastīti Z3_mk_const ar šādu nosaukumu, norādot vēl abstrakto pasauli, kurā tas dzīvos (int_sort, veselo skaitļu pasaule).
Lai uztaisītu summu, visi interesējošie mainīgie ir jāsalipina masīvā, un tad jāsauc Z3_mk_add ar šo sarakstu; salīdzināšanām ir savas mazās funkcijiņas, etc.
To visu uzķert un saprast, un uzrakstīt paņēma kādu brītiņu, bet rezultātā visus simtu septiņdesmit uzdevumus dators atrisina iespaidīgās 0.3 sekundēs!
Ko tālāk
Kad rokā ir āmurs, visa pasaule sāk izskatīties pēc naglām, un arī šis mans jaunais āmurs nu, šķiet, daudz kur atradīs pielietojumu, kur vajag un kur ne.
Mājasdarbam: pamēģini atrisināt šo bērnu rēbusu no PSRS žurnāla “Квант” 1984. gada aprīļa numura, kur katrs burts atbilst vienam ciparam, izmantojot Z3. Lai pateiktu, ka visi mainīgie ir dažādi, ērti būs lietot formu “distinct”:
(assert (distinct v a g o n s t))
