Trying to simplify this boolean expression.
(not (and (or (not e) (not f) (not h))
(or (not f) (not h) d)
(or (not e) (not h) c)
(or (not h) d c)
(or (not e) (not f) (not g) a)
(or (not f) d (not g) a)
(or (not e) (not f) a i)
(or (not f) d a i)
(or (not e) c (not g) a)
(or d c (not g) a)
(or (not e) c a i)
(or d c a i)
(or (not e) (not f) a b)
(or (not f) d a b)
(or (not e) c a b)
(or d c a b)))
This should be reduced to a boolean expression like this in cnf form.
(and
(or (not a) h)
(or (not b) (not i) g h)
(or (not c) f)
(or (not d) e))
I've been trying to achieve this by using "ctx-solver-simplify" and "tseitin-cnf" tactic. If only "ctx-solver-simplify" is applied, no simplification is performed for this case. When both these tactics are applied by then("tseitin-cnf", "ctx-solver-simplify"), a result is returned which contains lots of auxiliary variables. Which is also not the reduced form expected.
Is there a way to simplify this expression to the expected output?
EDIT: Asked the same question in Z3 github repo and got a really nice working response. Here is the issue.
Z3's simplification engine is not a good choice for these sorts of problems. It'll indeed "simplify" the expression, but it'll almost never match what a human would consider 'simple'. Many "obvious" simplifications will not be applied, as they simply do not matter from the SAT solver's perspective. You can search stack-overflow for many similar questions, and while z3 tactics can be used to great effect, they are not designed for what you are trying to do.
If you're looking for "minimal" (in a heuristic sense) simplification, you should look at other tools. For instance, sympy comes with a set of routines that does a decent job of conversion to canonical forms and simplification: https://stackoverflow.com/a/64626278/936310