MaxSAT and its applications

Speaker(s)

Michał Gajda

Affiliation

MIMUW

Language of the talk

English

Date

Dec. 19, 2025, 12:15 p.m.

Room

room 5450

Title in Polish

MaxSAT i jego zastosowania

Seminar

Seminar Semantics, Logic, Verification and its Applications

---

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.

---

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.

---