\myheading{\ac{SAT}-solvers}

\leveldown{}

\renewcommand{\CURPATH}{basics/SAT}

SMT vs. SAT is like high level \ac{PL} vs. assembly language.
The latter can be much more efficient, but it's hard to program in it.

SAT is abbreviation of ``Boolean satisfiability problem''.
The problem is to find such a set of variables, which, if plugged into boolean expression, will result in ``true''.

\input{\CURPATH/CNF}
\input{\CURPATH/2bit}
\input{\CURPATH/picosat}
\input{\CURPATH/MaxSAT}
\input{\CURPATH/list}

\levelup{}