\newchapter{Glossary (SAT)}

\begin{itemize}

\item clause --- disjunction of one or more literals. For example: var1 OR -var2 OR var3 ... - at least one literal must be satisfied in each clause.

\item CNF (conjunctive normal form) formula --- conjunction of one or more clauses. Is a list of clauses, all of which must be satisfied.

\item literal/term --- can be variable and -variable, these are different literals.

\item pure literal --- present only as x or -x in instance. Can be eliminated at start.

\item unit clause --- clause with only one literal.

\item DIMACS --- file format, popular among SAT solvers, benchmarks, etc.
Earliest description (1993): \url{http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf}.
"DIMACS" acronym itself means "The DIMACS Implementation Challenges"\footnote{\url{http://archive.dimacs.rutgers.edu/Challenges/}}.

\end{itemize}

\newchapter{Glossary (SMT)}

\begin{itemize}

\item sort --- datatype.

\end{itemize}