On strategies for solving boolean satisfiability problems

The paper deals with one of the most important problems of modern digital systems verification and design - Boolean satisfiability checking. The work analyzes different strategies for SAT solving evaluations. The approach is based on FUDASAT algorithm that employs commonsense reasoning methodology. Problems of variables selection, conflicts analyses and clauses set extensions are discussed. The presented methodology is exemplified on various benchmarks´ evaluations. Basing on the results of practical experiments a set of navigation rules, controlling Boolean satisfiability checking process, are formulated. Finally, the author summarizes the benefits of the proposed SAT solving technique.