In this thesis, we address the problem of finding sets that do not contain
an arithmetic progression. We will describe the more well-known problem of
finding the largest such set, after which we will focus on finding the smallest
such saturated set. We will present our custom solver for finding the smallest
set, along with some improvements. We will also present a model for the given
problem, which we will use to solve with SAT, ILP, SMT (Z3), and MiniZinc
solvers. The obtained results will be presented and the different solvers
will be compared. We will also model the problem of finding the largest
subset without an arithmetic progression and compare it to the search for
the smallest subset. Finally, we will describe some possible improvements for
our solver and for our problem model.
|
