After reading the previous questions Getting a “good” unsat core and getting a new unsat core , it’s currently impossible for me to get several different unsaturated kernels with z3. Do you have any suggestions to reduce the number of incompatible kernels? I am using z3 C ++ api to test the feasibility of constraints on linear real arithmetic. I found that by adding this line of code p.set(":auto-config",false) , as suggested in Getting a "good" untrusted kernel , the size of the inactive kernel becomes smaller.
Another question is about the z3 simplex algorithm. I used CPLEX to solve my application before using z3. CPLEX supports the extraction of IIS (irreducible impracticable set), which is like the unsaturated kernel in z3. We can set the decision algorithm "auto", "primal", "dual" in CPLEX. I found that when switching the solution algorithm IIS CPLEX may be different. Does z3 support the installation of various decision algorithms when the logic is set to QF_LRA?
source share