【Applied Algebra】求解布尔方程(Boolean Equations)的4个高效baseline算法

布尔方程组求解问题和计算机科学里的许多其他 NP-hard 问题都有联系(比如SAT问题,MILP整数规划问题等等);因此求解思路大致分为搜索求解,代数方法求解,问题变换求解三种基本思路,按照这样的划分,本文要介绍以下4种baseline算法:

• BCS算法(Boolean Characteristic Set Algorithm)[1]:基于经典代数消元方法吴消元法的求解算法;
• Groebner基算法[2]:基于多项式理想构造算法Groebner Basis的求解算法(基于SAGE V9.2的Polybori库实现);
• FESLib库(Fast Exhaustive Search Algorithm)[3]:基于分治+解空间搜索的求解算法(复杂度是指数级别 O ( d ⋅ 2 n ) \mathcal{O}(d \cdot 2^n) O(d⋅2n));
• 转SAT算法(Boolean Equations to SAT Algorithm)[4]:将布尔方程组问题转化为等价的SAT问题再使用SAT求解器求解的算法(基于Cryptominisat实现);

在本文中,我们主要侧重实现(所有代码均在Linux下编译实现),理论部分可以详见参考文献(如有需要,我会另外写博客来分别介绍这4篇工作的技术细节部分);

BCS算法 [1] 虽然基于吴消元法计算特征列,但是巧妙利用了布尔多项式的加法特点,克服了原方法里多项式膨胀的问题:

在 R 2 \mathcal{R}_{2} R2​ 中做拟除 Pesudo-division: 利用多项式 P 1 = I 1 x C + R 1 P_{1}=I_{1} x_{C}+R_{1} P1​=I1​xC​+R1​ 去消元 P 2 = I 2 x c + R 2 P_{2}=I_{2} x_{c}+R_{2} P2​=I2​xc​+R2​ 中的 x C x_{C} xC​. 计算:

I 1 ( I 2 x C + R 2 ) + I 2 ( I 1 x c + R 1 ) = I 1 R 2 + I 2 R 1 I_{1}(I_{2} x_{C}+R_{2})+I_{2}(I_{1} x_{c}+R_{1})=I_{1} R_{2}+I_{2} R_{1} I1​(I2​xC​+R2​)+I2​(I1​xc​+R1​)=I1​R2​+I2​R1​

其中 I 1 , I 2 , R 1 , R 2 I_{1},I_{2},R_{1},R_{2} I1​,I2​,R1​,R2​均为多项式,因此这样的运算会导致快速的多项式阶和项数的膨胀(这样的膨胀每次消元都会发生);

本文防止消元的多项式膨胀的方法主要依赖以下两点:

• 零点分解,作情况分支: V ⁡ ( F , I x c + U ) = V ⁡ ( F , x c + U , I + 1 ) ∪ V ⁡ ( F , U , I ) \operatorname{V}(\mathcal{F}, I x_{c}+U)=\operatorname{V}(\mathcal{F}, x_{c}+U, I+1) \cup \operatorname{V}(\mathcal{F},U, I) V(F,Ixc​+U)=V(F,xc​+U,I+1)∪V(F,U,I)

• F 2 \mathbb{F}_{2} F2​ 上加法消元: ( x c + U 1 ) + ( x c + U 2 ) = U 1 + U 2 (x_{c}+U_{1})+(x_{c}+U_{2})=U_{1}+U_{2} (xc​+U1​)+(xc​+U2​)=U1​+U2​.

更具体的算法可以参考原文,下面给出代码实现(源代码:https://github.com/hzy-cas/BCS);算法实现依赖CUDD包,该包主要实现了表示布尔函数的二元决策图数据结构 BDD(Binary Decision Diagram)及其相应算法,在选取初式时会更快;CUDD包的编译(使用cudd-2.4.2):

首先是修改Makefile里的XCFLAGS(对应主机的gcc版本):

XCFLAGS	= -mtune=native -DHAVE_IEEE_754 -DBSD -DSIZEOF_VOID_P=8 -DSIZEOF_LONG=8

尔后就是make,我没有make install,之后的依赖编译都是手动路径;下面是编译BCS算法的代码的Makefile(编译的cudd放在"/download/my_install/cudd-2.4.2"):

CFILES = main.cpp
INSTALL_DIR = /download/my_install/cudd-2.4.2
INCLUDING_PATH = /download/my_install/cudd-2.4.2/include
OBJFILES = main.o binary.o IO.o zddrcs.o zddrp.o zddrps.o zddrpss.o
CFLAGS = -pg
CFLAGS = -g -I$(INCLUDING_PATH) -L$(INSTALL_DIR)/cudd -L$(INSTALL_DIR)/epd -L$(INSTALL_DIR)/mtr -L$(INSTALL_DIR)/st -L$(INSTALL_DIR)/util
CC = g++
LIBS = -lcudd -lmtr -lst -lutil -lepd
DDDEBUG = -DDD_STATS

wu_char: main.o binary.o IO.o zddrcs.o zddrp.o zddrps.o zddrpss.o 
	$(CC) -o wu_char $(CFLAGS) $(OBJFILES) $(LIBS)

binary.o: binary.cpp 
	$(CC) -c $(CFLAGS) binary.cpp

IO.o: IO.cpp 
	$(CC) -c $(CFLAGS) IO.cpp

zddrcs.o: zddrcs.cpp 
	$(CC) -c $(CFLAGS) zddrcs.cpp

zddrp.o: zddrp.cpp 
	$(CC) -c $(CFLAGS) zddrp.cpp

zddrps.o: zddrps.cpp 
	$(CC) -c $(CFLAGS) zddrps.cpp

zddrpss.o: zddrpss.cpp 
	$(CC) -c $(CFLAGS) zddrpss.cpp

main.o: main.cpp 
	$(CC) -c $(CFLAGS) main.cpp

clean: 
	\rm -f $(OBJFILES)

用BCS算法求解一个变元数 n = 16 n=16 n=16的二次型布尔方程组:

[hanss@Mint]$ ./wu_char
--------------BCS algorithm by Zhenyu Huang, Version 1.2----------------
Please choose the RUNNING MODE:
0 for PoSSo mode(obtian all solutions );
1 for SAT mode (obtain one monic triangular set);
2 for Counting mode (Counting zero number);
0
-----------------Solving Mode: Obtain all solutions-------------------
Please input the name of the file containing the input polynomial system:
n16m32.poly
... ...
x1+1,x2+1,x3,x4+1,x5,x6+1,x7,x8,x9+1,x10+1,x11,x12+1,x13,x14,x15,x16

其中"x1+1"代表 x 1 = 1 x_1 = 1 x1​=1,"x3"代表 x 3 = 0 x_3 = 0 x3​=0,以此类推;

定义(Groebner基): 多项式组 G ⊂ K [ x 1 . . . x n ] \mathbb{G} \subset \mathcal{K}[x_1...x_n] G⊂K