Smtlib Qf Bv Eval

---
name: smtlib-qf-bv-eval
description: Evaluates the effectiveness of different MCSAT-based bitvector solving strategies and conflict explainers against a standard SMT benchmark suite. It measures how well each solver variant handles fixed-size bitvector formulas under a strict time limit. Use when the user wants to benchmark on SMT-LIB QF_BV, or asks about evaluating this task. Reports solved_instances.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2004.07940
  bibtex_key: [REDACTED]
  confidence: high
---

# smtlib-qf-bv-eval

> Solving bitvectors with MCSAT: explanations from bits and pieces (long version) — Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre (arXiv:2004.07940, 2020)

## What this evaluates

Evaluates the effectiveness of different MCSAT-based bitvector solving strategies and conflict explainers against a standard SMT benchmark suite. It measures how well each solver variant handles fixed-size bitvector formulas under a strict time limit.

## Datasets

- **SMT-LIB QF_BV** — total 41547; splits: test (41547)

## Metrics

- `solved_instances` **(primary)** — range: count
  - Count of benchmark instances solved by the solver before the 3-minute timeout expires. Reported as a cumulative count over time (solving curve) and as a final total.

## Input / output format

**Input**: A quantified bitvector (QF_BV) formula from the SMT-LIB benchmark suite.

**Output**: SATISFIABLE, UNSATISFIABLE, or TIMEOUT (if the 3-minute limit is reached).

## Scoring recipe

```python
def score_solved_instances(predictions, gold):
    solved_count = 0
    for pred in predictions:
        if pred in ('SATISFIABLE', 'UNSATISFIABLE'):
            solved_count += 1
    return solved_count
```

## Common pitfalls

- The timeout is fixed at 3 minutes per instance, which heavily influences the solving curve and final counts.
- Results are reported as cumulative solved instances over time, not as a single scalar metric, making direct point-in-time comparisons difficult without the full curve.
- The dataset is a static collection from SMT-LIB; splits are not explicitly defined, so all 41,547 instances are treated as a single evaluation set.

## Evidence (verbatim from paper)

> To evaluate its effectiveness, and the impact of the different modules, we ran the MCSAT solver with different settings on the 41,547 QF_BV benchmarks available in the SMT-LIB library [BST10]. We used a three-minute timeout per instance. Each curve in Figure 4 shows the number of solved instances for each solver variant; all: the procedures of Sections 3 and 4, with the bitblasting baseline when these do not apply; bb: only the bitblasting baseline; bb+eq: procedure of Section 3 plus the baseline; bb+arith: procedure of Section 4 plus the baseline; all-prop is the same as all but with no propagation of bitvector assignments during search.

## Citation

```bibtex
@misc{grahamlengrand2020solving,
  title={Solving bitvectors with MCSAT: explanations from bits and pieces (long version)},
  author={Stéphane Graham-Lengrand, Dejan Jovanović, Bruno Dutertre},
  year={2020},
  note={arXiv:2004.07940}
}
```

- arXiv: 2004.07940