Phase Selection Heuristics for Satisfiability Solvers

Computer Science – Logic in Computer Science

Scientific paper

Rate now

  [ 0.00 ] – not rated yet Voters 0   Comments 0

Details

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

Say what you really think

Search LandOfFree.com for scientists and scientific papers. Rate them and share your experience with other people.

Rating

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.

Rate now

     

Profile ID: LFWR-SCP-O-26807

  Search
All data on this website is collected from public sources. Our data reflects the most accurate information available at the time of publication.