Semantics of Division for Polynomial Solvers

TL;DR

This paper introduces a new semantics for division in polynomial systems involving logical formulas, addressing issues with existing methods by defining fair-satisfiability and providing a translation algorithm.

Contribution

It proposes the concept of fair-satisfiability, offering a new way to handle division in polynomial constraints with a translation method ensuring well-defined division.

Findings

Defines fair-satisfiability for formulas with division

Provides a translation algorithm to eliminate divisions

Establishes properties of the new division semantics

Abstract

How to handle division in systems that compute with logical formulas involving what would otherwise be polynomial constraints over the real numbers is a surprisingly difficult question. This paper argues that existing approaches from both the computer algebra and computational logic communities are unsatisfactory for systems that consider the satisfiability of formulas with quantifiers or that perform quantifier elimination. To address this, we propose the notion of the fair-satisfiability of a formula, use it to characterize formulas with divisions that are well-defined, meaning that they adequately guard divisions against division by zero, and provide a translation algorithm that converts a formula with divisions into a purely polynomial formula that is satisfiable if and only if the original formula is fair-satisfiable. This provides a semantics for division with some nice properties, which we describe and prove in the paper.