Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning

John Hester, Briland Hitaj, Grant Passmore +3

Cylindrical Algebraic Decomposition (CAD) is a key proof technique for formal verification of cyber-physical systems. CAD is computationally expensive, with worst-case doubly-expon…