Benchmark Sets for Variable Elimination in Conjunctions of Linear Real Arithmetic Constraints

Three benchmark sets for testing tools on the task of existential quantifier elimination from conjunctions of linear real arithmetic constraints (a.k.a. polyhedron projection).

All sets are given in three formats:

ine: .ine files as used by the CDD library and some other polyhedra libraries.

redlog: .red files as used by the CAS Reduce and its package Redlog

smtlib: .smt2 files as used by SMT related tools like SMT-RAT or z3.

The Random set contains random satisfiable conjunctions of 3-60 constraints with 3-30 variables and different coefficient densities, from which half of the variables are to be eliminated. The NN-Verif set contains conjunctions obtained in neural network verification tasks. The SMT-lib-deriv set contains conjunctions derived during SMT-solving of the QF_LRA satisfiability checking benchmarks from SMT-lib.