This page has been moved to

STROPSAT: a library for SubTROPical SATisfiability

Brief description

STROPSAT is a library providing new incomplete but efficient and terminating method to identify positive values for polynomials reals. The method is derived from the subtropical method recently introduced in the context of symbolic computation for computing real zeros of a single very large multivariate polynomial. It takes an abstraction of polynomials as exponent vectors over the natural numbers tagged with the signs of the corresponding coefficients. The library uses two alternatives to decide subtropical satisfiablity.


FroCos 2017 submission files