基于因子图求解(3,4=)-CNF公式类下可满足问题

Based on the Factor Graph for Solving Satisfiability Problem of (3,4=)-CNF Formula Class

合取范式(CNF)公式F是(3,4=)-CNF公式,如果F中每个子句的长度是3,每个变元出现的次数恰好为4次。与(3,4=)-CNF公式所关联的因子图是一类规则的二部图,即每个子句结点的度为3,每个变元结点的度为4,此类规则图被称为(3,4)-双向正则二部图。对于一个(3,4=)-CNF公式F,如果它关联的因子图GF有P7-路径因子,则F可满足。

A CNF formula F is a（3,4=）-CNF formula if each clause contains exactly three literals and each variable appears exactly four times in the formula.The factor graph of a（3,4=）-CNF formula has a regular structure,in which the degree of clause node is exactly three,the degree of variable node is exactly four.Such regular graph is called（3,4）-biregular bigraph.For a（3,4=）-CNF formula F,if the associated factor graph GF has a P7-factor,then F is satisfiable.