# Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning

## TL;DR

This paper improves variable ordering for Cylindrical Algebraic Decomposition in formal verification by creating a more balanced dataset and evaluating machine learning models' generalizability.

## Contribution

It introduces a new, less biased dataset for training ML models on variable ordering and assesses their performance and generalizability.

## Key findings

- New dataset with over 41K challenges reduces bias.
- Machine learning models show improved generalization on the new dataset.
- Addressing dataset bias enhances the effectiveness of variable ordering strategies.

## Abstract

Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-exponential complexity. Selecting an optimal variable ordering is paramount to efficient use of CAD. Prior work has demonstrated that machine learning can be useful in determining efficient variable orderings. Much of this work has been driven by CAD problems extracted from applications of the MetiTarski theorem prover. In this paper, we revisit this prior work and consider issues of bias in existing training and test data. We observe that the classical MetiTarski benchmarks are heavily biased towards particular variable orderings. To address this, we apply symmetries to create a new dataset containing more than 41K MetiTarski challenges designed to remove bias. Furthermore, we evaluate issues of information leakage, and test the generalizability of our models on the new dataset.