Satisfiability checking and symbolic computation