SAT Competition

Úloha

Vašou úlohou je implementovať SAT solver v jazyku Python, ktorý:

• načíta formulu v tvare DIMACS CNF,
• rozhodne jej splniteľnosť,
• ak je splniteľná, vypíše SAT a model (priradenie premenných),
• ak nie je splniteľná, vypíše UNSAT,
• musí byť efektívny a zvládnuť testy do 500 premenných a 2000 klauzúl v rozumnom čase (60 sekúnd na test).

Technické požiadavky

Spustenie programu

Program musí byť spustiteľný z príkazového riadku:

python satsolver.py input.cnf output.txt

Program:

• načíta súbor z prvého argumentu príkazového riadku
• vypíše výsledok do súboru zadaného ako druhý argument príkazového riadku

Povolené a zakázané

Povolené

• Ľubovoľný algoritmus (DPLL, CDCL, backtracking, heuristiky, watched literals, clause learning, …),
• Ľubovoľné vlastné optimalizácie,
• Použitie štandardnej Python knižnice.

Zakázané

• Externé SAT knižnice,
• Použitie hotových solverov (MiniSAT, PySAT, Z3, atď.),
• Volanie externých programov,
• Použitie akýchkoľvek externých balíkov mimo štandardnej knižnice.

Porušenie pravidiel znamená hodnotenie 0 bodov.

Vstupný formát – DIMACS CNF

Vstupný súbor je v štandardnom DIMACS formáte, ktorý reprezentuje formulu v konjunktívnej normálnej forme (CNF).

Formát je nasledovný:

c komentár
p cnf <num_vars> <num_clauses>
<clause1>
<clause2>
...

Kde:

• c označuje komentár
• p cnf označuje začiatok problému a typ formátu
• <num_vars> je počet premenných
• <num_clauses> je počet klauzúl

Zároveň:

• Literály sú celé čísla
• Kladné číslo i znamená premennú x_i
• Záporné číslo -i znamená negáciu ¬x_i
• Každá klauzula končí číslom 0
• Premenné sú číslované od 1 po num_vars

Príklad vstupu

c Example
p cnf 3 2
1 -3 0
2 3 -1 0

reprezentuje formulu: $$(x_1 ∨ ¬x_3) ∧ (x_2 ∨ x_3 ∨ ¬x_1)$$

Výstupný formát

Ak je formula nesplniteľná:

UNSAT

Ak je formula splniteľná:

SAT
<l1> <l2> ... <ln> 0

kde:

• li je celé číslo
• kladné číslo znamená TRUE
• záporné číslo znamená FALSE
• každá premenná od 1 po num_vars musí byť priradená
• poradie literálov je ľubovoľné
• model musí končiť 0

Príklad výstupu

SAT
1 -2 3 0

alebo

UNSAT

Korektnosť

Pri hodnotení sa kontroluje:

• správnosť rozhodnutia (SAT / UNSAT)
• správnosť modelu (ak SAT):
  • každá klauzula musí byť splnená
  • každá premenná musí mať hodnotu

Nesprávny formát výstupu = test neúspešný.

Dátová sada vstupných formúl

Dátová sada bude obsahovat 35 formúl v DIMACS formáte rozdelených do 4 kategórií:

• Malé testy: 10 testov s 10-50 premennými a 20-200 klauzúl
• Stredné testy: 10 testov s 50-200 premennými a 200-1000 klauzúl
• Veľké testy: 10 testov s 200-500 premennými a 1000-2000 klauzúl
• Špeciálne testy: 5 testov s rôznymi štruktúrami (napr. ťažké vs. ľahké, rôzne pomery klauzúl k premenným, atď.)

Môžete použiť túto vzorovú dátovú sadu formulae.zip na testovanie a ladenie svojho solvera. Finálne hodnotenie bude založené na inom súbore testov, ktorý bude zverejnený až po odovzdaní riešení.

Formuly v tejto dátovej sade sú rôzneho charakteru, vrátane náhodných formúl, formúl s vysokou štruktúrou, a formúl z reálnych problémov. Niektoré testy môžu byť veľmi náročné, takže efektívnosť implementácie bude kľúčová.

Dátová sada bola generovaná pomocou nástroja CNFgen, ktorý umožňuje vytvárať formuly s rôznymi vlastnosťami a obtiažnosťou.

Výkonnostné požiadavky

Solver musí zvládnuť:

• formuly do 500 premenných,
• do 2000 klauzúl,
• časový limit: 60 sekúnd na test

Solver bude testovaný na rôznych sadách testov, vrátane malých, stredných a veľkých formúl. Brute force riešenie nebude postačovať.

Testy budú spustené na počítači s nasledujúcou konfiguráciou:

• CPU: 12th Gen Intel® Core™ i7-1260P (16 vlákien)
• RAM: 32.0 GiB
• GPU: Intel® Iris® Xe Graphics (ADL GT2)
• Operačný systém: Ubuntu 24.04.4 LTS

Hodnotenie

Za Solver je možné získať 15 bodov (časť skúšky) podľa nasledujúcich kritérií:

Bonus (max +5 bodov)

• Implementácia pokročilých techník (CDCL, clause learning, watched literals, atď.)
• Nadštandardná výkonnosť

Spolu: 15 bodov

Najlepšie riešenia

Tri najlepšie riešenia získajú skúšku!

Rebríček

Bude zverejnený rebríček podľa:

• počtu vyriešených testov
• celkového času

Odovzdanie

Odovzdanie v kurze Moodle musí obsahovat:

• satsolver.py
• krátky popis implementovaného algoritmu (max. 1 strana PDF)

Akademická integrita

• Riešenie musí byť samostatná práca.
• Bude použitá automatická kontrola podobnosti riešení.