Proposition matrix search algorithm for satisfiability degree computation

Satisfiability degree is used as a new means of representing uncertainty. It is able to express the extent of a system satisfying some property. How to compute the satisfiability degree is a critically problem. Although this paper has proved the computation for the satisfiability degree has the exponential worst case complexity, the proposition matrix is proposed to construct the proposition matrix search algorithm. It always chooses the high frequency proposition to simplify the old formula to obtain two new formulae, and the satisfiability degree of the old formula is equal to the sum of satisfiability degrees of the two new formulae. If the new formulae can be judged as true or false, the algorithm directly computes their satisfiability degree; else their satisfiability degree is recursively computed as the old formula. The proposition matrix search algorithm uses a truth detector to detect the truth value of a proposition so that computation times can be reduced significantly. Experimental results show it is more effective than the basic enumeration algorithm and the backtracking search algorithm.