fix a bug of unsat-based algorithm when a initial solution is given
improve SAT.TseitinEncoder module a bit