MaxSAT and its applications

Prelegent(ci)

Michał Gajda

Afiliacja

MIMUW

Język referatu

angielski

Termin

19 grudnia 2025 12:15

Pokój

p. 5450

Tytuł w języku polskim

MaxSAT i jego zastosowania

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

Największa Spełnialność (MaxSAT) korzysta z rozwiązywaczy
spełnialności (SAT) do optymalizacji dyskretnej. Zasadą jest
maksymalizacja liczby jednocześnie spełnionych reguł „opcjonalnych”
(bo reguły obowiązkowe muszą być spełnione zawsze.)
Umożliwia to rozwiązywanie problemów NP-trudnych, takich jak pokrycie
zbiorów czy TSP. W dziedzinie tej regularnie oceniane są najlepsze
algorytmy [MaxSAT]. Ostatnie oceny algorytmików ujawniły również,
że MaxSAT jest motorem najszybszych rozwiązań [PACE] w wielu
innych dziedzinach. Wybrałem kilka porównań wydajności, aby pokazać używane
algorytmy.

---

Maximum Satisfiability (MaxSAT) uses satisfiability solvers (SAT) for
discrete optimization. The principle is to maximize the number of
simultaneously satisfied "optional" rules (because mandatory rules
must always be satisfied). This enables solving NP-hard problems such
as set covering and TSP. The field regularly evaluates the best
algorithms [MaxSAT]. Recent algorithm evaluations have also revealed
that MaxSAT drives the fastest solutions [PACE] in many
fields. I've selected a few performance comparisons to show the
algorithms used.

---