Can z3 check SAT and MaxSAT for three-valued logics (via the Python interface)?

[kopeckyf]

Three-valued logics, such as the three-valued Łukasiewicz logic (Ł3) or Kleene's logic are logics with a third truth valued besides True and False, often labelled Undetermined or Unknown.

Within these logics, formulas of propositional logic can become True in more cases than in standard propositional logic. For example, in Ł3, the formula a∨b is True if one of a, b is True and the other Undetermined. But Ł3 and Kleene's logic do not change the definition of satisfiability. That is, an interpretation still only satisfies a formula if the formula is True under the assignment (but not if it evaluates to the third value).

My Q of SAT-checking for these logics in z3 has the following sub-questions:

• I believe I need to start with declaring a new Boolean datatype for Undetermined. Is that possible using the z3py interface?
• How can I implement the operations of propositional logic (negation, conjunction, disjunction and implication) from a three-valued logic in z3, via z3py? (Ł3 and Kleene's logic differ only in the rules that apply for the implication)
• Can I then simply use the Solver and Optimize classes for these logics as I have for standard propositional logic? In particular, will checking satisfiability, finding a MaxSAT/optimisation solution and enumeration via the blocking models approach (all_smt()) work as in the two-valued case?

Your help is very much appreciated 😊