Commit 1394c2ca authored by Amin Raslan's avatar Amin Raslan
Browse files

Replace related_work.tex

parent 54afed49
\section{Related Work}
Es gibt auch andere Constraint Solver, die Integer Arithmetic lösen können, wie:
Es gibt auch andere Constraint Solver, die Integer Arithmetic lösen können:
\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 Picat Solver. Picat ist eine Programmiersprache, die mehrere Programmierparadigmen wie logische Programmierung, imperative Programmierung und Constraintprogrammierung zusammen kombiniert und verwendet. Neben dem CP-Solver wird in Picat auch ein 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}
\end{itemize}
\ No newline at end of file
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