# MUS/MSS Enumeration on SMT

Source: [MUS/MSS Enumeration on SMT](<https://www.sota2.com/research/sota/mus-mss-enumeration-on-smt>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2026-04-13T08:32:26.360Z

Evaluation of model performance on the SMT dataset, focusing on the enumeration of Minimal Unsatisfiable Sets (MUS) and Minimal Satisfiability Sets (MSS).

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

| Scope | Recorded value |
| --- | --- |
| Task | MUS/MSS Enumeration |
| Dataset (including any stated split) | SMT |
| Metric | Count of MUSes/MSSes |
| Unit | SCALAR |
| Direction | Higher is better |
| Results loaded | 2 of 2 |
| Coverage | All results currently returned for this benchmark |

Evaluation settings may differ between results. The original papers and recorded configurations are needed to establish comparability. A shared metric name alone does not establish an identical protocol.

## Metrics

- [Count of MUSes/MSSes](<https://www.sota2.com/research/sota/mus-mss-enumeration-on-smt.md?metric=Count%20of%20MUSes%2FMSSes>): Higher is better; unit: SCALAR.

- [Improvement Ratio](<https://www.sota2.com/research/sota/mus-mss-enumeration-on-smt.md?metric=Improvement%20Ratio>): Higher is better; unit: SCALAR.

## Recorded results

| Method | Count of MUSes/MSSes | Result date | Report paper |
| --- | --- | --- | --- |
| HyMUSE | 58 | Not recorded | 69dc78607d0172140ec78908 |
| Baseline (MARCO) | 43.3 | Not recorded | 69dc78607d0172140ec78908 |

### HyMUSE

Count of MUSes/MSSes: 58. Result ID: 69dcaa0b47f34ce924c39efe.

[Reporting paper](<https://www.sota2.com/research/paper/69dc78607d0172140ec78908.md>)

[Method origin paper](<https://www.sota2.com/research/paper/69dc78607d0172140ec78908.md>)

Recorded evaluation configuration: {"Agent":"w/ Agent","Checks":"10k"}. This record does not assert independent reproduction.

### Baseline (MARCO)

Count of MUSes/MSSes: 43.3. Result ID: 69dcaa0b47f34ce924c39efd.

[Reporting paper](<https://www.sota2.com/research/paper/69dc78607d0172140ec78908.md>)

Recorded evaluation configuration: {"Agent":"w/o Agent","Checks":"10k"}. This record does not assert independent reproduction.

Page 1 of 1. This is an index page, not the full collection.