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.

- Minkowski sum and linear programming:
- SMT solving over linear real arithmetic

**STROPSAT-0.1**(8 May 2017)

**Experimental results**: veriT (with STROPSAT as a theory solver for QF_NRA) vs Z3, the clear winner of SMTCOMP 2016 on QF_NRA**Paper**- SMT2 benchmarks for example 12 of the above paper
**Nonlinear SMT2 Benchmark****Linear SMT2 Benchmark**for searching a solution of the nonlinear benchmark in (R^+)^d (Example 12 runs this example against CVC4)**Linear SMT2 Benchmark**for searching a solution of the nonlinear benchmark in R^d (Section 5)

Vu Xuan Tung at JAIST