SAT solver with static and dynamic ordering decision making

This paper proposes a propositional satisfiability problem (SAT) solver, which inherits the features such as conflict-driven learning and fast Boolean constraint propagation. It improves the decision making strategy by encouraging conflicts, thus pruning the search as early as possible. Variables are ordered according to f(x) × f(∼ x), where f(x) is the number of literal x in all clauses. The unassigned variable with the largest value is chosen to assign. When conflicted, the activities of all literals in the conflict clauses are increased and the order is updated. Experimental results show that the proposed SAT solver obtains much performance improvement in comparison with other solvers.