ABsolver

From ASCEND

Jump to: navigation, search
This article is about planned development or proposed functionality. Comments welcome.

ABsolver is a 'satisfiability modulo theories' solver that can efficiently solve systems of nonlinear equations subject to boolean constraints.

Problems capable of being solved by ABsolver contain:

  • boolean variables
  • real variables
  • real constraints, acting on real variables, each with a corresponding boolean 'truth state'
  • boolean constraints, acting on various subsets of the boolean variables and truth states

ABsolver has been shown to work well with a few test problems. We propose to connect it with ASCEND and see how it goes with a borader set of problems.

See also Category:Solvers and CMSlv and conditional modelling and student projects.

Retrieved from "http://ascendwiki.cheme.cmu.edu/ABsolver"