Commit 11843180 authored by Amin Raslan's avatar Amin Raslan
Browse files

Update related_work.tex

parent 4a0d7bb1
\section{Related Work}
\ No newline at end of file
\section{Related Work}
Es gibt auch andere Constraint Solver, die Integer Arithmetic lösen können, wie:
\begin{itemize}
\item Picat Solver. Picat ist eine neue Programmiersprache, die mehrere Programmierparadigmen wie logische Programmierung, imperative Programmierung und Constraintprogrammierung zusammen kombiniert und verwendet. Neben dem CP-Solver wird in Picat auch einen SAT-Solver unterstützt, der fast die selbe Funktion hat wie der CP-Solver \cite{picat}.
\item Z3, ein SMT-Solver von Microsoft Research der in verschiedenen Verifizierungen und Analyseanwendungen verwendet wird \cite{z3}.
\item Kodkod, ein SAT-basierter Constraint-Solver, der unter Anderem für Logik erster Ordnung verwendet wird. Er bietet automatisierte Argumentationshilfe für erfüllbare und unerfüllbare Probleme. Kodkod wird unter Anderem für Codeprüfung, Testfallgenerierung, und deklarative Ausführung und Konfiguration \cite{kodkod}.
\end{itemize}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment