ABsolver

This article is about planned development or proposed functionality. Comments welcome.

ABSolver is a 'SMT' or 'SAT modulo theories' solver written by Andreas Bauer that augments a conventional boolean satisfiability solver with a solver able to calculate non-linear equation systems. The result is a solver that can optimise difficult decision-making problems coupled with non-linear constraints.

It appears that ABsolver, or a solver based on the same approach, might be an interesting, and possibly powerful, alternative to ASCEND's current CMSlv solver for conditional modelling.