understanding expressions within z3 (hacking mus.cpp)

[oferst]

Trying to develop group-mus in mus.cpp,
In get_mus1, the initial core is a vector of expressions defined in m_lit2expr.
For group-mus, I need expressions of other assertions in the same group, even if they are not in the core.
I retrieve them from m_solver.get_assertions()
When I build a expr_ref_vector based on assertions from that list, even if they are unsat,
m_solver.check_sat(mus);
still returns SAT.
When I print the expressions in mus:
for (auto e : mus) {
m_pp_util.display_expr(verbose_stream(), e);
indeed they seem fine and contradictory, although they look different than those that appear in m_lit2expr (they seem to be just the labels).
Any idea why am I getting SAT ?
Ofer

[NikolajBjorner]

If you need soft constraints that are not in the core, you need to change the call site and add a feature to add them.
A relevant call site (for testing) should be in smt/smt_solver.cpp.

m_solver.check_sat( inconsistent-formulas ) should be unsat.
Maybe you are using some code path that wasn't exercised in other use cases.
You can double check by adding inconsistent-formulas as assertions.
If the version with the assumptions is sat but the version with assertions is unsat the issue should be below your layer.

for (auto* e : mus)
     verbose_stream() << mk_pp(e, m) << "\n";

[oferst]

This indeed solved the problem. Thank you.

Do you want this contribution in Z3 ?
I added an option
(set-option :smt.core.hlminimize true)

there is no way that I am aware of to specify the group number within smt2, so I just embedded the group name inside the assertion name, e.g., this one is in group 10:
(assert (! (>= (* 1 x1310) 1) :named gr10_c5))

-- Ofer

[NikolajBjorner]

The question of integration in z3 is based on whether the functionality helps a good use case (use it or lose it) and can be packaged to be usable across clients. The external API seeks to support use cases that are more customized and benefits from more agile development. So far, all the core-based maxsat functionality could be coded externally (even with better algorithms), but I include it for one-stop out of the box experience.

Can you specify what the grouping feature does? I am not quite sure what it is. I can guess it means that soft assertions are tagged by a group identifier and there is a preference to find cores within some groups than others.

Using string tags is perhaps fine for prototyping, but I tend to hit issues when maintaining code with embedded assumptions.

For example, they could be weighted soft constraints. Soft constraints already supports language for being tagged and weighted.
There is an implicit ordering between tagged soft constraints based on the order they are first introduced.

There are also two core minimization modules internally: the SAT solver includes its own core minimization module (src/sat/sat_mus).
Not great for evolving the overall functionality.

[oferst]

Group MUS was researched and used heavily in the propositional case -- see some references below mostly from EDA.
The use case is when users have control over high-level constraints, that translate to many assertions each. They can turn on or off the high-level constraint, not the individual assertions. And this is why they need a minimal core of high-level constraints. For example, in a bounded planning setting, you have an obstacle that translates to a constraint in each time frame; but you can either keep it or remove it for all the time frames together.

Example:

(assert (! (> x1 x2) :named gr1_c1)) ; group 1
(assert (! (> x2 x3) :named gr1_c2)) ; group 1
(assert (! (> x3 x1) :named gr1_c3)) ; group 1
(assert (! (> x2 x1) :named gr2_c4)) ; group 2

Here a mus is constraints 1 + 4. A minimal hl-mus, however, is group 1, consisting of constraints 1,2,3.

This capability is reducible to normal mus, simply by putting all the assertions of a group in a big conjunction, hence making it a single assert.
For other reasons, for example keeping the capability to find a normal mus as well, and readability, it might be more convenient to support group-mus natively.

Some references:

M. H. Liffiton and K. A. Sakallah /Algorithms for computing minimal unsatisfiable subsets of constraints

Z. S. Andraus, M. H. Liffiton, and K. A. Sakallah, “Refinement strategies
for verification methods based on datapath abstraction,” in ASP-DAC,
F. Hirose, Ed. IEEE, 2006, pp. 19–24.

S.-Y. Huang and K.-T. Cheng, Formal equivalence checking and design debugging. Norwell, MA, USA: Kluwer Academic Publishers, 1998.

Z. Khasidashvili, D. Kaiss, and D. Bustan, “A compositional theory for post-reboot observational equivalence checking of hardware,” in FMCAD. IEEE, 2009, pp. 136–143.

Alex Nadel / Boosting Minimal Unsatisfiable Core Extraction

Ofer Guthmann, Ofer Strichman, Anna Trostanetski / Minimal unsatisfiable core extraction for SMT

[oferst]

This indeed solved the problem. Thank you. Do you want this contribution in Z3 ? I added an option (set-option :smt.core.hlminimize true) there is no way that I am aware of to specify the group number within smt2, so I just embedded the group name inside the assertion name, e.g., this one is in group 10: (assert (! (>= (* 1 x1310) 1) :named gr10_c5))

…

-- Ofer From: Nikolaj Bjorner ***@***.***> Sent: Sunday, September 11, 2022 10:45 PM To: Z3Prover/z3 ***@***.***> Cc: Ofer Strichman ***@***.***>; Author ***@***.***> Subject: Re: [Z3Prover/z3] understanding expressions within z3 (hacking mus.cpp) (Discussion #6339) If you need soft constraints that are not in the core, you need to change the call site and add a feature to add them. A relevant call site (for testing) should be in smt/smt_solver.cpp. m_solver.check_sat( inconsistent-formulas ) should be unsat. Maybe you are using some code path that wasn't exercised in other use cases. You can double check by adding inconsistent-formulas as assertions. If the version with the assumptions is sat but the version with assertions is unsat the issue should be below your layer. for (auto* e : mus) verbose_stream() << mk_pp(e, m) << "\n"; - Reply to this email directly, view it on GitHub<https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2FZ3Prover%2Fz3%2Fdiscussions%2F6339%23discussioncomment-3620810&data=05%7C01%7Cofers%40ie.technion.ac.il%7Cfe2b731077494847a34f08da942e147b%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637985222887949080%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=gY8vOzDC9dlIIc4dGBXZrY%2BT6ydBgzoKin0cMbB7JGg%3D&reserved=0>, or unsubscribe<https://eur01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fgithub.com%2Fnotifications%2Funsubscribe-auth%2FACLFDDFK46GDOQDXDWP3TGDV5YZCZANCNFSM6AAAAAAQJ2TPXE&data=05%7C01%7Cofers%40ie.technion.ac.il%7Cfe2b731077494847a34f08da942e147b%7Cf1502c4cee2e411c9715c855f6753b84%7C1%7C0%7C637985222887949080%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000%7C%7C%7C&sdata=B%2FtyjJrwPPMzKk%2BvVk2eLsC31c%2BHjn5Q7SMYBAnCfHE%3D&reserved=0>. You are receiving this because you authored the thread.Message ID: ***@***.******@***.***>> External e-mail, be judicious when opening attachments or links