Research On Clause Simplification In Model Counting

Model counting(#SAT)is a basic problem in the field of artificial intelligence,aiming to solve the number of satisfiable assignments for a given propositional formula,and the complexity is #P complete.Modern CDCL framework-based model counters are already capable of handling large CNF formulas with millions of clauses.However,in complex practical applications such as Bayesian networks,planning,bounded model detection,probabilistic inference,etc.,there are still many huge CNF formulas that are too difficult to solve using the current state-of-the-art model counters.For large-scale problems,simplifying the clauses in the CNF formula is an effective method to improve the efficiency of model counting.The preprocessing of model counting can simplify the propositional formulas by removing redundant clauses and variables using propositional formula inference rules.A variety of advanced preprocessing techniques including subsumption elimination(SE),tautology elimination(TE),vivification(VIV),and B+E algorithm can greatly reduce the number of clauses in propositional formulas.However,simplified formulas do not always perform better in model counting.The total model counting time of some abnormal formulas which are preprocessed increase significantly.This paper proposes a criterion to measure the difficulty of model counting,and implements a method to filter abnormal formulas by judging whether the propositional formula is more difficult to solve after preprocessing.This paper proposes a preprocessing filtering algorithm FILTER.By calling two mature preprocessors: PMC and B+E,and comparing the solving difficulty of the original formula and the two preprocessed formulas,the formula with the lowest solving difficulty is selected for model counting.The algorithm FILTER is tested on the latest model counter Exact MC,and the experimental results show that the preprocessing filtering strategy proposed in this paper combines the benefits of PMC and B+E,and improves the efficiency of model counter.In many large-scale practical problems,the appearance of multi-valued variables is very common.Multi-valued variables are represented as exactly-one constraints in the propositional logic knowledge base.When using model counters to solve practical problems involving multi-valued variables,it is often necessary to convert exactly-one constraints into CNF formulas.This method expands the scale of proposition formula and easily leads to time overflow.To solve such problems better,this paper proposes an algorithm ECR to identify exactly-one constraints from CNF formulas.C2 D is the only solver that can directly handle exactly-one constraints currently.The experimental results show that the algorithm ECR significantly improves the solving efficiency of C2 D.For other model counters that cannot handle exactly-one constraints directly,this paper proposes an algorithm ECP that handles exactly-one constraints separately.The algorithm ECR and algorithm ECP are applied to the model counter Exact MC,and the improved model counter ECMC has better performance than Exact MC.In summary,the main research content of this paper is to improve the solving efficiency of model counting by simplifying the clauses of propositional formulas.This paper proposes two strategies: one is a preprocessing screening strategy to filter out abnormal formulas in the preprocessing stage,and the other is to identify and individually process exactly-one constraints in propositional formulas in the solving stage.The experimental results tested on Exact MC and C2 D show that the two strategies proposed in this paper have simplified the scale of the propositional formulas and improved the solving efficiency of the model counters.