一种布尔公式的代数逻辑约化新方法  

New Algebraic Logic Reduction Method for Boolean Formula

作　　者：刘江[1,2] 周鸿昊 LIU Jiang;ZHOU Hong-hao(High Performance Computing Application Research Center,Chongqing Institute of Green and Intelligent Technology,Chinese Academy of Sciences,Chongqing 400714,China;University of Chinese Academy of Sciences,Beijing 100049,China)

机构地区：[1]中国科学院重庆绿色智能技术研究院高性能计算应用研究中心,重庆400714 [2]中国科学院大学,北京100049

出　　处：《计算机科学》2020年第5期32-37,共6页Computer Science

基　　金：国家自然科学基金(61672488)。

摘　　要：布尔可满足问题是最早被证明的NP完全问题之一,1-in-3-SAT问题是一个NP完全的布尔可满足子类问题。1-in-3-SAT的计算复杂度取决于对应公式的变量以及子句的个数。将1-in-3公式归约为一个变量数或者子句数更少的1-in-3公式,是提高1-in-3-SAT问题求解效率的一个关键。基于一个新的范式形式——XCNF,针对1-in-3-SAT问题提出一种新的代数逻辑约化方法,用于在多项式时间内约减一个1-in-3公式的变量数和子句数。所提算法的主要思想为:首先将1-in-3公式转化为XCNF公式,然后尝试找出XCNF公式中的X-纯文字,并利用X-纯文字法则对1-in-3公式中相应的布尔变量赋值,最后得到一个约减公式,该约减公式与原公式的1-in-3可满足性等价。Boolean satisfiability problem is one of the earliest proven NP complete problem.1-in-3-SAT problem is an NP complete subclass of Boolean satisfiability problem.The computational complexity of 1-in-3-SAT depends on the number of the variables and clauses in the formula.How to reduce the 1-in-3 formula to one with less variables or clauses is the key to improve the efficiency of solving 1-in-3-SAT.Based on a new type of normal form-XCNF,this paper proposes a new algebraic logic reduction method to reduce the number of variables and clauses in polynomial time.The main idea is as follows.First,the method transforms the 1-in-3 formula into a XCNF formula,then tries to find out the X pure literal in the XCNF formula and assign the corresponding Boolean variable in the 1-in-3 formula with X pure literal rule.At last,a reduced formula which has the same 1-in-3 satisfiability with the original one can be obtained.

关 键 词：NP完全问题 布尔可满足性问题 1-in-3-SAT XCNF X-纯文字 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]