+++
title = "Using a realistic SAT solver"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["2d4"]
forwardlinks = []
zettelid = "2d5"
+++

I have now implemented usage of a real SMT solver (Z3) using OCaml. It
is surprisingly easy to use this SMT solver from the OCaml code, much
easier than using the external Z3 executable. Expressions can easily be
added as various assertions, and expressions themselves can also be
built quite easily and recursively from given predicates. This makes it
simple to add a custom solver to custom predicates.

It should therefore be possible to also use the SAT solver to simplify
arbitrary predicates as well, however, there are still various problems
with extracting the expressions from the SAT solver again, as they are
in the internal expression format of the solver.