Research On Redundant Clauses And Redundant Literals In Propositional Logic

The satisfiability of logic formulas has a wide range of applications in engineering,transportation,military and natural sciences.As the capacity of computer solving problems increases gradually and the problem of solving becomes more complicated,the redundancy of logic formulas in propositional logic is more,which wastes a lot of storage space and computing time.Detecting and eliminating redundancy in logic formulas can effectively improve computer storage space utilization efficiency and reduce computation time.This paper studies the redundancy properties of logic formulas and their judgments,in order to provide a certain theoretical basis for the elimination of redundancy.The main research work is as follows:1.Study the nature of redundant clauses and propose methods for judging redundant clauses.Firstly,the concept of redundant clauses in logical formulas is proposed by referring to the hidden literals defined by the binary clauses and the hidden literals’ related properties.Then,some methods for determining whether a unit clause exists in a clause set are obtained,separately.Based on the concept of redundant clauses,the problem of clause redundancy in logical formulas is discussed,and the equivalence conditions for the satisfiability of redundant clauses and their corresponding clause sets are derived.Finally,using the equivalence property between the clause sets,the corresponding judgment conditions of the redundant clauses are obtained.2.Study the nature of redundant literals and propose methods for judging redundant literals.Firstly,the concept of redundant literals in the clause sets is proposed according to the rules of adding hidden literals in the binary clauses,and the relationship between the redundant literals and the satisfiability of their corresponding clause set is obtained.Then,according to the related properties of redundant clauses,the relationship between redundant clauses and redundant literals is derived.Finally,according to the equivalence between clause sets,a method for judging redundant clauses and redundant literals is proposed.