Computation of Satisfiability Degree Based on CNF

摘要

Satisfiability degree extends the satisfiable property of a formula, represents the satisfiable extent of certain properties in model checking, and exhibits it sex actness and convenience for representing real-world uncertainty and fuzziness. Computation of the satisfiability degree of propositional formulas is concerned in this paper. The computation relies on truth table, avoids the obtaining of membership function in fuzzy logic and probability function in probabilistic logic, and finally obtains much exacter value than fuzzy logic and probabilistic logics. Two computation algorithms respectively based on interpretations of CNF (Conjunctive Normal Form)formulas and explanations of propositional formulas are proposed, and further improvement of the basic interpretation-based algorithm is disclosed.