Computer Science – Logic in Computer Science
Scientific paper
2011-06-07
Computer Science
Logic in Computer Science
12 pages 2 figures
Scientific paper
In general, a SAT Solver based on conflict-driven DPLL consists of variable selection, phase selection, Boolean Constraint Propagation, conflict analysis, clause learning and its database maintenance. Optimizing any part of these components can enhance the performance of a solver. This paper focuses on optimizing phase selection. Although the ACE (Approximation of the Combined lookahead Evaluation) weight is applied to a lookahead SAT solver such as March, so far, no conflict-driven SAT solver applies successfully the ACE weight, since computing the ACE weight is time-consuming. Here we apply the ACE weight to partial phase selection of conflict-driven SAT solvers. This can be seen as an improvement of the heuristic proposed by Jeroslow-Wang (1990). We incorporate the ACE heuristic and the existing phase selection heuristics in the new solver MPhaseSAT, and select a phase heuristic in a way similar to portfolio methods. Experimental results show that adding the ACE heuristic can improve the conflict-driven solvers. Particularly on application instances, MPhaseSAT with the ACE heuristic is significantly better than MPhaseSAT without the ACE heuristic, and even can solve a few SAT instances that remain unsolvable so far.
No associations
LandOfFree
Phase Selection Heuristics for Satisfiability Solvers does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Phase Selection Heuristics for Satisfiability Solvers, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Phase Selection Heuristics for Satisfiability Solvers will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-26807