Chc Comp21 Lia Lin Eval

---
name: chc-comp21-lia-lin-eval
description: Evaluates the effectiveness of bottom-up versus top-down transformations for solving linear constrained Horn clauses (CHCs) using software verification workflows. It measures how many verification tasks a solver can successfully resolve within a strict time limit. Use when the user wants to benchmark on CHC-COMP21 LIA-Lin track, or asks about evaluating this task. Reports solved_tasks.
metadata:
  skill_kind: dataset_eval
  source_arxiv: 2404.15215
  bibtex_key: [REDACTED]
  confidence: high
---

# chc-comp21-lia-lin-eval

> Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification — Somorjai et al. (2024) (arXiv:2404.15215, 2024)

## What this evaluates

Evaluates the effectiveness of bottom-up versus top-down transformations for solving linear constrained Horn clauses (CHCs) using software verification workflows. It measures how many verification tasks a solver can successfully resolve within a strict time limit.

## Datasets

- **CHC-COMP21 LIA-Lin track** — total 585; splits: benchmark (585)

## Metrics

- `solved_tasks` **(primary)** — range: [0, 585]
  - Count of benchmark tasks successfully solved (SAT/UNSAT proven) within the 300-second timeout. Tasks exceeding the timeout are counted as unsolved.

## Input / output format

**Input**: Linear Constrained Horn Clauses (CHCs) over the background theory of linear integer arithmetic.

**Output**: Satisfiability verdict (SAT/UNSAT) or timeout status.

## Scoring recipe

```python
solved_count = 0
for task in dataset:
    result = solver.run(task, timeout=300)
    if result == "solved":
        solved_count += 1
return solved_count
```

## Common pitfalls

- Timeouts are strictly capped at 300 seconds; partial progress or slow convergence does not count as solved.
- Baseline solvers (Z3, UNIHORN, ELDARICA) were run with their default configurations, which may not be optimized for this specific track.
- The evaluation only reports task counts; it does not measure proof/refutation generation or runtime distribution beyond a quantile plot.

## Evidence (verbatim from paper)

> The implementation was evaluated on 585 linear CHCs over the background theory of linear integer arithmetic from the LIA-Lin track of the CHC-COMP21 benchmark repository. The benchmarks were run on machines with 8 logical CPU cores and 16 GB of memory, with a timeout of 300 seconds. The results of the tool were either correct or timeout for all of the tasks.

## Citation

```bibtex
@misc{somorjai2024bottoms,
  title={Bottoms Up for CHCs: Novel Transformation of Linear Constrained Horn Clauses to Software Verification},
  author={Somorjai et al. (2024)},
  year={2024},
  note={arXiv:2404.15215}
}
```

- arXiv: 2404.15215