Jump to: navigation, search
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.

Franc Ivankovic is working on this project as part of his Summer Scholarship at ANU in 2010/11.