Implement subset minimal unsat core #765

Tomaqa · 2024-09-08T23:45:25Z

No description provided.

Tomaqa · 2024-09-10T14:57:56Z

The solution currently uses MainSolver as an auxiliary SMT solver. However, I believe it would be more efficient to use just SimpSMTSolver, but it seems that it is not as straightforward to do as it may seem.

I decided to make a separate derived class for minimal unsat cores because it requires the other SMT solver to be used, unlike other unsat cores. I think it would be inconvenient to require the user to provide an SMT solver although it might not have been used.

blishko · 2024-09-12T11:27:25Z

src/api/Interpret.cc

+    if (not config.print_cores_full()) {
+        for (PTRef fla : unsatCore->getNamedTerms()) {
+            assert(termNames.contains(fla));
            auto const & name = termNames.nameForTerm(fla);
            std::cout << name << ' ';
        }
+    } else {
+        for (PTRef fla : unsatCore->getTerms()) {
+            if (termNames.contains(fla)) {
+                std::cout << termNames.nameForTerm(fla);
+            }
+            else {
+                std::cout << logic->printTerm(fla);
+            }
+            std::cout << ' ';
+        }


Why is this needed?

In the first branch, we use named terms so all of them must be in termNames. In second branch, we iterate over all terms so not all of them are necessarily in termNames. If it is not, we just print out string representation of the term, because we do not have any name for it.

I still don't get it.
I don't see why you need to change the existing functionality.
What does the new option mean?

We should be printing only names, not the terms themselves, no?

This commit implements option :print-cores-full from https://cvc5.github.io/blog/2024/04/15/interfaces-for-understanding-cvc5.html

I see, can you please document the meaning of this option? And maybe also the minimal-unsat-cores, to make it clear that these are subset minimal, and not global minimum.

Moved to #771

test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.out

blishko · 2024-09-17T08:40:55Z

test/regression/base/QF_UF/php_3_3_40_min_unsat_core.smt2

Do we need these large files? I would prefer to minimize as much as possible the regression tests that we add.

I removed them from this PR. However, I think some of them will be needed to track the minimization process more thoroughly. They could be simplified, though.

blishko

Looks good!
But it seems the two options that you are introducing does not work together correctly.
Maybe the full cores should be introduced in a separate PR? Since it is orthogonal functionality.

Another note is that we should investigate using the Quickxplain algorithm to compute minimal unsat cores.

blishko · 2024-09-17T14:18:37Z

src/api/MainSolver.cc

+    auto unsatCoreBuilder = [&]() -> std::variant<UnsatCoreBuilder, MinUnsatCoreBuilder> {
+        if (not config.minimal_unsat_cores()) { return UnsatCoreBuilder{config, proof, pmanager, termNames}; }
+
+        auto auxSMTSolver = std::make_unique<MainSolver>(logic, config, "unsat core solver");


It might be more efficient to give this new solver a fresh config. Specifically, the new solver does not need to compute unsat cores anymore.

That is a good point.

Based on this, I actually reconsidered the design and I think both builder classes can be merged. Since we use MainSolver and not SimpSMTSolver, it is sufficient to extend UnsatCoreBuilder constructor of just Logic & parameter, which is fine. The internal SMT solver can be constructed inside only if minimization is desired. Do you agree?

That would be very good, I think!

blishko · 2024-09-17T14:26:49Z

src/unsatcores/MinUnsatCoreBuilder.cc

+    assert(size_t(namedTerms.size()) == namedTermsIdxs.size());
+}
+
+void MinUnsatCoreBuilder::minimizeAlgNaive() {


This algorithm only minimizes the named terms, no?
Thus this does not compute minimal explanation if used together with the option print-cores-full, no?

It computes the same minimal explanation of named terms, but the response includes also unnamed terms. I am not sure how CVC5 implements this combination of options, but strictly following their definition would mean ignoring named terms completely, including the minimization process.

My intuition is that if print-cores-full is set then the names should be ignored and, if minimal cores are required then the minimization algorithm should operate on all terms, not only the named ones.

blishko

LGTM!
I would make the solver and config local to the method where they are needed. Feels like the class would simpler that way.
But I am also fine with how it is now.

src/api/MainSolver.cc

blishko · 2024-09-19T07:45:13Z

src/unsatcores/UnsatCoreBuilder.cc

+    setSmtSolver();
+}
+
+void UnsatCoreBuilder::minimizeAlgNaive() {


To me it seems like it would be better if the new config and new solver were local to this method. Then, there would be no need for the set methods.

But then it would not be usable in functions other than minimizeAlgNaive, and I plan to add more functions and select one of them based on the configuration.

Then each method can have its own local solver.
The solver is not supposed to be shared between different methods, no?

Probably not among distinct algorithms, but more sophisticated minimization algorithms may be divided into more functions or even use subclasses and it would require to always pass the local variable as a parameter. I would do that only if it would turn out to be reasonably more efficient than using the current member variable. Or are your concerns other than performance?

My concerns are readability and simplicity.
And local reasoning.

Another thought: minimization stuff can be enclosed in a nested class (e.g. Minimize) where common functionalities among various strategies can be shared using inheritance, and member variables within the class can be "local" in a sense - within the scope of minimization. Also minimizeInit may be replaced by constructor, minimizeFinish by destructor, etc. It would still not use the variables as local variables within a function, but the scope of the variables would still be limited.

How about we merge this now and you can rethink the design when you want to add another minimization strategy?

I got a similar idea. I will make it local for now and we will see what to do next.

blishko

LGTM!

Tomaqa linked an issue Sep 8, 2024 that may be closed by this pull request

Implement subset-minimal unsat core #753

Closed

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch 10 times, most recently from 80f52c4 to 15b1687 Compare September 10, 2024 14:54

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from 15b1687 to 42b9678 Compare September 11, 2024 20:53

Tomaqa marked this pull request as ready for review September 12, 2024 08:49

Tomaqa changed the base branch from master to term-names September 12, 2024 08:49

blishko reviewed Sep 12, 2024

View reviewed changes

Tomaqa force-pushed the term-names branch from 5237ee3 to b8d08c0 Compare September 13, 2024 12:57

Tomaqa added 2 commits September 13, 2024 14:59

Included named terms in unsat cores

99a00fd

Changed ptrs to refs in UnsatCoreBuilder since they are not necess.

17526c2

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch 2 times, most recently from 64ca27f to cea4259 Compare September 13, 2024 13:09

Tomaqa deleted the branch master September 13, 2024 13:19

Tomaqa closed this Sep 13, 2024

Tomaqa reopened this Sep 13, 2024

Tomaqa changed the base branch from term-names to master September 13, 2024 13:22

blishko requested changes Sep 17, 2024

View reviewed changes

test/regression/base/generic/trivial_unsat_core2_full.smt2.expected.out Outdated Show resolved Hide resolved

blishko reviewed Sep 17, 2024

View reviewed changes

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from cea4259 to 9a840f7 Compare September 17, 2024 10:28

blishko reviewed Sep 17, 2024

View reviewed changes

Few regression tests on unsat cores with more possibilities

55ae278

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from 9a840f7 to 7cfe97f Compare September 17, 2024 15:39

Tomaqa mentioned this pull request Sep 17, 2024

Implemented smt2 option ":print-cores-full" (from CVC5) #771

Draft

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from 7cfe97f to 1f9ef14 Compare September 18, 2024 10:59

blishko previously approved these changes Sep 19, 2024

View reviewed changes

Tomaqa dismissed blishko’s stale review via b7352f4 September 19, 2024 10:10

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from 1f9ef14 to b7352f4 Compare September 19, 2024 10:10

Naive implementation of subset-minimal unsat core

effdd77

Tomaqa force-pushed the 753-implement-subset-minimal-unsat-core branch from b7352f4 to effdd77 Compare September 19, 2024 10:14

blishko approved these changes Sep 19, 2024

View reviewed changes

Tomaqa closed this Sep 19, 2024

Tomaqa deleted the 753-implement-subset-minimal-unsat-core branch September 19, 2024 13:36

Tomaqa restored the 753-implement-subset-minimal-unsat-core branch September 19, 2024 13:37

Tomaqa reopened this Sep 19, 2024

Tomaqa merged commit effdd77 into master Sep 19, 2024
9 checks passed

Tomaqa deleted the 753-implement-subset-minimal-unsat-core branch September 19, 2024 13:38

Tomaqa restored the 753-implement-subset-minimal-unsat-core branch September 19, 2024 13:38

Tomaqa temporarily deployed to github-pages September 19, 2024 13:38 — with GitHub Pages Inactive

Tomaqa deleted the 753-implement-subset-minimal-unsat-core branch September 19, 2024 13:41

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Implement subset minimal unsat core #765

Implement subset minimal unsat core #765

Tomaqa commented Sep 8, 2024

Tomaqa commented Sep 10, 2024

blishko Sep 12, 2024

Tomaqa Sep 13, 2024 •

edited

Loading

blishko Sep 16, 2024

Tomaqa Sep 16, 2024

blishko Sep 17, 2024

Tomaqa Sep 17, 2024

blishko Sep 17, 2024

Tomaqa Sep 17, 2024

Tomaqa Sep 17, 2024

blishko left a comment

blishko Sep 17, 2024

Tomaqa Sep 17, 2024

Tomaqa Sep 17, 2024

blishko Sep 17, 2024

Tomaqa Sep 18, 2024

blishko Sep 17, 2024

Tomaqa Sep 17, 2024 •

edited

Loading

blishko Sep 17, 2024

Tomaqa Sep 19, 2024 •

edited

Loading

blishko left a comment

blishko Sep 19, 2024

Tomaqa Sep 19, 2024

blishko Sep 19, 2024

Tomaqa Sep 19, 2024

blishko Sep 19, 2024 •

edited

Loading

Tomaqa Sep 19, 2024

blishko Sep 19, 2024

Tomaqa Sep 19, 2024

blishko left a comment

Implement subset minimal unsat core #765

Implement subset minimal unsat core #765

Conversation

Tomaqa commented Sep 8, 2024

Tomaqa commented Sep 10, 2024

Choose a reason for hiding this comment

Tomaqa Sep 13, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Tomaqa Sep 17, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Tomaqa Sep 19, 2024 • edited Loading

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko Sep 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

blishko left a comment

Choose a reason for hiding this comment

Tomaqa Sep 13, 2024 •

edited

Loading

Tomaqa Sep 17, 2024 •

edited

Loading

Tomaqa Sep 19, 2024 •

edited

Loading

blishko Sep 19, 2024 •

edited

Loading