To solve the problem that SAT solvers usually has excessive backtraces during assigning binary values to an unassigned variables, a new SAT solver based on symbolic simulation and variable partition, which lower not only the number of backtrack but the memory blow-up, was presented. The SAT solver partitions a big CNF into two smaller subset A and B, then divides the set of variables into three disjoint set. Through the constraint that the symbolic values are only assigned to the variable in the set which occur in both A and B, the symbolic simulation based SAT solver get both the low backtrack number and memory occupation. Experimental result showed the SAT solver is sound and efficient.
