Algorithm Research On Satisfiability Problem Parameterized By Formula Length

Abstract:The Satisifiability(SAT) problem is a core NP-complete problem in the field of theoretical computation and computational complexity. Nowadays, SAT problems have widely applications on automated reasoning, computer-aided design, computer-aided manufac-turing, machine vision, database and so on. Traditional methods focus on the discrete, constrained decision SAT problem, and the formal definition is:given a bool Conjecture Normal Form CNF, does there exists an assignment satisfying all the clauses in the CNF? The time complexity in the computing process of SAT can be in terms of3main parameters:the number of the given variables n, the number of the given clauses m and the number of the given literals in the whole L.This paper focuses on the exact algorithm of the general SAT problem in terms of literals L. The existing best result on exact algorithm has a running time O*(1.0652L). This paper first studies the reduction rules of SAT problem in terms of formula length. It gives12reduction rules and the proofs, according to the resolution method and the new measure-the sum of the weighted frequencies of all the variables in the given CNF. Owing to the reduction rules, all clauses containing at least2literals and each two different literals do not contained in2clauses, and they show the relation between the clauses containing2literals and the clauses containing at least3literals.This paper adopts branch-and-bound searching algorithm. The branching procedure first finds3special sub-formulas for branching, then chooses a variable of largest degree for branching. Besides using a more refined branching technique to improve the algorithm for SAT, this paper introduces a new technique in analysis--Measure and Conquer. Based on Measure and Conquer technique and a more refined branching technique, this paper improves the upper bound of the SAT algorithm to O*(1.0651L).