% z3

\subsection{Introduction to z3}

The z3 tool is a \textit{Satisfiability Modulo Theories} (SMT) prover~\cite{z3-01} developed by Microsoft Research and released as an open source project. It is useful to solve all the problems that fall under the \textit{Satisfiabiliy Modulo Theories} (SMT) problem which are a subsection of the \textit{Boolean Satisfiability} (SAT) problem.
It integrates different decision procedures and additional theories as equality reasoning, arithmetic, fixed-size bit-vector and quantifier.

It exposes different APIs in several programming language like C, C++ and Java. In this thesis work the version 4.8.7 for 64-bit machines is implemented.

The framework z3 receives a set of boolean and arithmetic formulas through its interfaces and it translates them into a SMTLIB2 file, in this way it provides a common background for all the SMT theories described in the Figure~\ref{fig:z3_solver}.
The first operation is apply tactics like ``Preprocessing'' or ``Cube \& Conquer'', this avoid the computational time to explode and to discard suboptimal solutions.
After this operation, z3 chooses and exploits a specific solver (e.g. SAT, SMT) to get a solution, or the best solution if the problem asks for an optimal result.

For the optimization phase, this solver provide the optimizer engine called \textit{z3Opt}.

\hfill
\begin{figure}[H]
	\centerline{\includegraphics[width=0.95\textwidth]
		{Z3Solver2.png}}
	\caption{Z3 architecture.
		\label{fig:z3_solver}}
\end{figure}

\subsection{SAT problem}

The SAT (propositional satisfiability) problem, is a well-known problem in computer science. The task of a SAT problem is to decide if a specific combination of boolean variables that compose a set of propositional formulas exists to assurance the satisfiability of the formulas.
This means that a problem could be solved in different ways and it could exist more then one solution.
The SAT problem finds any solution that allows the problem to be satisfiable.

This type of problem is \textit{non deterministic polynomial time}, which means, despite the\break correctness of the formulas could be evaluated in a polynomial time, the time to find a\break solution increases with a non polynomial shape with the size of the problem. So it can be classified as \textit{NP-complete}.
\pagebreak

\subsection{SMT problem}

The SAT problem is limited to boolean logic, so to represent others theories as integers, real numbers, lists and others, a generalization is done with the SMT problem. 
\textit{Satisfiability Modulo Theories} is an instance of a Boolean satisfiability problem in which some the binary variables are replaced by predicates over a set of non-binary variables~\cite{SMT}.

This allows to express more complex problems that can exploit, instead of boolean propositional formulas, a set of binary predicates made of not boolean variables. This made the SMT language more expressive then the SAT boolean language.

The structure depicted in Figure \ref{fig:z3_solver} shows that z3 tool offers SMT solver with different efficient search methods exploiting pruning algorithms and also heuristic combinations of methods called tactics. 

\subsection{MaxSMT problem}

In computational complexity theory the \textit{Maximum Satisfiability Modulo Theories} (MaxSMT) problem is defined as an extension of the SMT problem, where the goal is not just to find a solution, which guarantees the problem to be satisfiable, but the best solution which optimizes the variable values to achieve the maximum satisfiability of the clauses.

The main difference between the simple SMT problem is that each clause has a weight, so the consequence is to find a solution which, among all the satisfiable ones found, maximizes the number of satisfied clauses with the minimal cost.

In the the context of optimization the MaxSMT problem allows different clauses to be\break expressed as:
\begin{itemize}
	\item 
	\textit{soft constraints}, they are relaxable clauses ($ s_{i} \in S $), which means they could be not satisfied but with a ``penalty'';
	
	\[ maximize \sum_{i = 1}^{S} w_{i} * s_{i}\] where $w_{i}$ is the weight of the clauses and the $s_{i}$ is the soft constraint to be satisfied;
	
	\item
	\textit{hard constraints}, they are clauses that must be satisfied.
	
	\[subject \; to \; h_{j}, \; with \; \forall j \in [1, H]\]
\end{itemize}

The z3 tool could be used as library in a Java project as the following source code (Figure~\ref{fig:z3-code}), given as output the values of the binary variables as shown in Figure~\ref{fig:z3-ouput}.

\begin{figure}[ht]
	\figuretitle{z3 source code}
	\HRule
\begin{lstlisting}[numbers=left,stepnumber=1, language=Java]
Context ctx = new Context();
Optimize opt = ctx.mkOptimize();

// boolean variables creation
BoolExpr b1 = ctx.mkBoolConst("b1");
BoolExpr b2 = ctx.mkBoolConst("b2");
BoolExpr b3 = ctx.mkBoolConst("b3");
BoolExpr b4 = ctx.mkBoolConst("b4");

BoolExpr expr1 = ctx.mkAnd(ctx.mkOr(b1, b2), b3);
BoolExpr expr2 = ctx.mkNot(b4);

// soft constraints
opt.AssertSoft(b1, 1, "group");
opt.AssertSoft(b2, 3, "group");
opt.AssertSoft(expr2, 5, "group");

// hard constraints
opt.Assert(expr1);
opt.Assert(expr2);

// model computationg
opt.Check();
Model model = opt.getModel();
\end{lstlisting}
	\HRule
	\caption{z3 used as library in a Java project.
		\label{fig:z3-code}}
\end{figure}

\begin{figure}[ht]
	\figuretitle{z3 output}
	\HRule
	\begin{lstlisting}
(define-fun b1 () Bool true)
(define-fun b2 () Bool true)
(define-fun b4 () Bool true)
(define-fun b3 () Bool true)
	\end{lstlisting}
	\HRule
	\caption{z3 outcome after the computation of the optimizazion model.
		\label{fig:z3-ouput}}
\end{figure}