# MUS/MSS Enumeration on SAT small

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

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

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

Evaluation of model performance on the small subset of the SAT dataset, focusing on the enumeration of Minimal Unsatisfiable Sets (MUS) and Minimal Satisfiability Sets (MSS), measured by the normalized count.

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) | SAT small |
| Metric | Normalized Count |
| Unit | SCALAR |
| Direction | Higher is better |
| Results loaded | 8 of 8 |
| 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

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

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

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

## Recorded results

| Method | Normalized Count | Result date | Report paper |
| --- | --- | --- | --- |
| ReMUS | 3.29 | Not recorded | 69dc78607d0172140ec78908 |
| ReMUS | 2.16 | Not recorded | 69dc78607d0172140ec78908 |
| MARCO | 1.79 | Not recorded | 69dc78607d0172140ec78908 |
| TOME | 1.69 | Not recorded | 69dc78607d0172140ec78908 |
| TOME | 1.52 | Not recorded | 69dc78607d0172140ec78908 |
| MARCO | 1 | Not recorded | 69dc78607d0172140ec78908 |

### ReMUS

Normalized Count: 3.29. Result ID: 69dcaa0b47f34ce924c39ef3.

[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 Integration":"w/o Agent"}. This record does not assert independent reproduction.

### ReMUS

Normalized Count: 2.16. Result ID: 69dcaa0b47f34ce924c39ef6.

[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 Integration":"w/ Agent"}. This record does not assert independent reproduction.

### MARCO

Normalized Count: 1.79. Result ID: 69dcaa0b47f34ce924c39ef4.

[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 Integration":"w/ Agent"}. This record does not assert independent reproduction.

### TOME

Normalized Count: 1.69. Result ID: 69dcaa0b47f34ce924c39ef5.

[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 Integration":"w/ Agent"}. This record does not assert independent reproduction.

### TOME

Normalized Count: 1.52. Result ID: 69dcaa0b47f34ce924c39ef2.

[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 Integration":"w/o Agent"}. This record does not assert independent reproduction.

### MARCO

Normalized Count: 1. Result ID: 69dcaa0b47f34ce924c39ef1.

[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 Integration":"w/o Agent"}. This record does not assert independent reproduction.

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