English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

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

Revisiting Variable Ordering for Real Quantifier Elimination using Machine Learning