added <Algorithm::SAT::Expression> to use the backtrack solver