From Total Assignment Enumeration to Modern SAT Solver

Details From Total Assignment Enumeration to Modern SAT Solver From Total Assignment Enumeration to Modern SAT Solver

2011-10-26

arxiv.org/abs/1110.5867v1

Computer Science

Logic in Computer Science

Scientific paper

A new framework for presenting and analyzing the functionality of a modern DLL-based SAT solver is proposed. Our approach exploits the inherent relation between backtracking and resolution. We show how to derive the algorithm of a modern SAT solver from DLL step-by-step. We analyze the inference power of Boolean Constraint Propagation, Non-Chronological Backtracking and 1UIP-based Conflict-Directed Backjumping. Our work can serve as an introduction to a modern SAT solver functionality and as a basis for future work on the inference power of a modern SAT solver and on practical SAT solver design.

Affiliated with

Also associated with

No associations

Rating

From Total Assignment Enumeration to Modern SAT Solver 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 From Total Assignment Enumeration to Modern SAT Solver, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and From Total Assignment Enumeration to Modern SAT Solver will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFWR-SCP-O-717986