Search code examples
z3

Prime Implicant in z3


I look for a solution to find (minimum) prime implicant for a formula in QF_AUBV logic using z3 solver. is it possible to get such a partial prime implicant from z3 solver?


Solution

  • Yes, but there is no function that will do that job. You may have to use quantifiers (to axiomatize the notion of implicants) and/or repeated SAT queries (to minimize implicants).