| 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.
|
|---|