-
Exploiting Strict Constraints in the Cylindrical Algebraic Covering
Authors:
Philipp Bär,
Jasper Nalbach,
Erika Ábrahám,
Christopher W. Brown
Abstract:
One of the few available complete methods for checking the satisfiability of sets of polynomial constraints over the reals is the cylindrical algebraic covering (CAlC) method. In this paper, we propose an extension for this method to exploit the strictness of input constraints for reducing the computational effort. We illustrate the concepts on a multidimensional example and provide experimental r…
▽ More
One of the few available complete methods for checking the satisfiability of sets of polynomial constraints over the reals is the cylindrical algebraic covering (CAlC) method. In this paper, we propose an extension for this method to exploit the strictness of input constraints for reducing the computational effort. We illustrate the concepts on a multidimensional example and provide experimental results to evaluate the usefulness of our proposed extension.
△ Less
Submitted 29 June, 2023;
originally announced June 2023.
-
Levelwise construction of a single cylindrical algebraic cell
Authors:
Jasper Nalbach,
Erika Ábrahám,
Philippe Specht,
Christopher W. Brown,
James H. Davenport,
Matthew England
Abstract:
Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a commonly used tool is the Cylindrical Algebraic Decomposition (CAD) to decompose real space into cells where the constraints are truth-invariant through…
▽ More
Satisfiability Modulo Theories (SMT) solvers check the satisfiability of quantifier-free first-order logic formulas. We consider the theory of non-linear real arithmetic where the formulae are logical combinations of polynomial constraints. Here a commonly used tool is the Cylindrical Algebraic Decomposition (CAD) to decompose real space into cells where the constraints are truth-invariant through the use of projection polynomials.
An improved approach is to repackage the CAD theory into a search-based algorithm: one that guesses sample points to satisfy the formula, and generalizes guesses that conflict constraints to cylindrical cells around samples which are avoided in the continuing search. Such an approach can lead to a satisfying assignment more quickly, or conclude unsatisfiability with fewer cells. A notable example of this approach is Jovanović and de Moura's NLSAT algorithm. Since these cells are produced locally to a sample we might need fewer projection polynomials than the traditional CAD projection. The original NLSAT algorithm reduced the set a little; while Brown's single cell construction reduced it much further still. However, the shape and size of the cell produced depends on the order in which the polynomials are considered.
This paper proposes a method to construct such cells levelwise, i.e. built level-by-level according to a variable ordering. We still use a reduced number of projection polynomials, but can now consider a variety of different reductions and use heuristics to select the projection polynomials in order to optimise the shape of the cell under construction. We formulate all the necessary theory as a proof system: while not a common presentation for work in this field, it allows an elegant decoupling of heuristics from the algorithm and its proof of correctness.
△ Less
Submitted 20 July, 2023; v1 submitted 19 December, 2022;
originally announced December 2022.
-
Supporting Proving and Discovering Geometric Inequalities in GeoGebra by using Tarski
Authors:
Christopher W. Brown,
Zoltán Kovács,
Róbert Vajda
Abstract:
We introduce a system of software tools that can automatically prove or discover geometric inequalities. The system, called GeoGebra Discovery, consisting of an extended version of GeoGebra, a controller web service realgeom, and the computational tool Tarski (with the extensive help of the QEPCAD B system) successfully solves several non-trivial problems in Euclidean planar geometry related to in…
▽ More
We introduce a system of software tools that can automatically prove or discover geometric inequalities. The system, called GeoGebra Discovery, consisting of an extended version of GeoGebra, a controller web service realgeom, and the computational tool Tarski (with the extensive help of the QEPCAD B system) successfully solves several non-trivial problems in Euclidean planar geometry related to inequalities.
△ Less
Submitted 3 January, 2022;
originally announced January 2022.
-
Model-based construction of Open Non-uniform Cylindrical Algebraic Decompositions
Authors:
Christopher W. Brown
Abstract:
In this paper we introduce the notion of an Open Non-uniform Cylindrical Algebraic Decomposition (NuCAD), and present an efficient model-based algorithm for constructing an Open NuCAD from an input formula. A NuCAD is a generalization of Cylindrical Algebraic Decomposition (CAD) as defined by Collins in his seminal work from the early 1970s, and as extended in concepts like Hong's partial CAD. A N…
▽ More
In this paper we introduce the notion of an Open Non-uniform Cylindrical Algebraic Decomposition (NuCAD), and present an efficient model-based algorithm for constructing an Open NuCAD from an input formula. A NuCAD is a generalization of Cylindrical Algebraic Decomposition (CAD) as defined by Collins in his seminal work from the early 1970s, and as extended in concepts like Hong's partial CAD. A NuCAD, like a CAD, is a decomposition of n-dimensional real space into cylindrical cells. But unlike a CAD, the cells in a NuCAD need not be arranged cylindrically. It is in this sense that NuCADs are not uniformly cylindrical. However, NuCADs--- like CADs --- carry a tree-like structure that relates different cells. It is a very different tree but, as with the CAD tree structure, it allows some operations to be performed efficiently, for example locating the containing cell for an arbitrary input point.
△ Less
Submitted 23 March, 2014;
originally announced March 2014.
