| Meno: | Adam |
|---|---|
| Priezvisko: | Fremal |
| Názov: | Comparing solvers for combinatorial problems |
| Vedúci: | doc. RNDr. Ján Mazák, PhD. |
| Rok: | 2026 |
| Kµúčové slová: | SAT solving, ILP, SMT, CP-SAT, benchmarking, parallel execution, combinatorial problems |
| Abstrakt: | This thesis presents a software framework for benchmarking solvers of combinatorial problems on a common set of inputs. It compares the SAT, ILP, SMT, and constraint- programming (CP-SAT) paradigms on equal terms through standard text interfaces, and treats the encoding of a problem as a first-class comparison dimension alongside the solver. Each solver runs as an isolated subprocess under a time limit with its CPU and memory use measured. The framework is designed to be extensible: adding a solver that reuses a known format is a configuration change, and a new solver family needs only a small parser. After a run it reports the result for every instance and flags any case where two solvers disagree on satisfiability. We apply the framework to the Hamiltonian cycle and the circular chromatic index and find that the best solver and encoding are problem-dependent. On one instance family an older solver solves nearly every instance while the 2025 SAT Competition winners solve almost none, yet on another the winners are fastest. |
Súbory bakalárskej práce:
| main-en.pdf |
Súbory prezentácie na obhajobe: