本发明涉及电子设计自动化（electronicdesignautomation，eda）领域，尤其涉及一种布尔可满足性问题求解方法及系统。
背景技术：
可满足性问题（sat问题）是指给出一个以合取范式格式表达的命题逻辑公式，推理判断是否存在一组或多组赋值使得这个合取范式表示的公式可满足。在可满足的情况下，算法会给出一组使得问题满足的解。自2002年至2020年，大批高效的sat求解器和先进的算法被不断提出，其中算法主要分为两种，即cdcl（conflictdrivenclauselearning，冲突驱动子句学习）算法和sls（stochasticlocalsearch，随机局部搜索）算法。cdcl算法是基于dpll算法的改进，对产生的冲突进行分析，引入冲突分析、子句学习策略和非时序性回溯策略，提高了算法求解效率。基于cdcl算法框架进行改进的sat求解器如chaff、minisat、glucose等已经在sat问题上取得了很大的效果，当前sat的研究主要集中在分支启发策略、单子句传播、子句学习、重启、预处理、非时序性回溯和数据结构的设计上。
chaff的作者表明，在求解过程中bcp传播占用了大量的时间，因此提出一种分支启发策略给予持续出现在冲突中的变元较高的活性分数，这样，在下一次决策时可以快速选择变元，现有的变元分支启发策略都是基于这种思路。
但是，在求解的初始阶段仍然存在问题。一方面，在搜索的初始阶段，由于冲突次数太少，分支启发策略的选择是不准确的，因此选择分支变元具有一定的时间局限性。简单的说，在初始阶段，不能确定所选择赋值的自由变元在命题逻辑结构中扮演者怎样的逻辑角色，只有随着时间的推移，才能通过分支启发策略选择具有一定质量水平的变元。另一方面，初始变元的选择，直接影响整个搜索过程，选择不好的初始变元，在求解过程中虽然会产生大量冲突，但所习得的学习子句通常质量较低，会在子句库删减操作中删除。对于大多数求解器，都是采用随机赋值的方式选择初始变元，这就会使求解过程的开始阶段具备一定的空间局限性。
在电子设计自动化领域，sat求解器在搜索初始阶段的时间局限性和空间局限性尤为明显，原因在于：电子设计自动化领域往往通过先设计一些小的功能模块，再用这些小的功能模块来构筑复杂的电路，电路模块内联系紧密但各个电路模块之间的联系较少，联接各个电路模块之间的桥接变元具有划分模块的作用，即：通过分割桥接变元可以或多或少的独立解决考虑电路模块的内部关系。但此类问题转化为sat问题之后，可能会导致一些结构信息的缺失。而且，由于随机选择初始值，不能有效选择在电路模块中扮演桥接作用的变元。造成了时间和空间的浪费。在其他领域，如软件开发等，也存在这种情况。
技术实现要素：
本发明的目的是针对现有技术的sat解算器随机选取第一个分支变元导致解算初始阶段存在时间局限性和空间局限性的技术问题，本发明提出一种布尔可满足性问题求解方法及系统。
本发明实施例中，提供了一种布尔可满足性问题求解方法，其包括：
采用多个并行求解器在设定的阈值条件内对cnf实例进行多线程并行求解，其中，每个并行求解器采用不同的初始变元；
每个并行求解器在触发阈值条件后停止求解，并记录求解过程中各个变元的活性分数；
选择所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解。
本发明实施例中，所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间。
本发明实施例中，所述多个并行求解器通过克隆所述主求解器得到。
本发明实施例中，所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。
本发明实施例中，在采用多个并行求解器对cnf实例进行多线程并行求解之前，还包括：
对所述cnf实例进行预处理，解析所述cnf实例的初始化全局变量和文字及子句的关系，并进行优化。
本发明实施例中，还提供了一种布尔可满足性问题求解系统，其包括：
多个并行求解器，用于采用不同的初始变元在设定的阈值条件内对cnf实例进行多线程并行求解，并在触发阈值条件后停止求解，记录求解过程中各个变元的活性分数；
主求解器，用于采用所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解。
本发明实施例中，所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间。
本发明实施例中，所述多个并行求解器通过克隆所述主求解器得到。
本发明实施例中，所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。
本发明实施例中，所述的布尔可满足性问题求解系统，还包括：
随机赋值模块，用于为每个并行求解器产生一个随机的初始变元；
选择模块，用于选择出所述多个并行求解器中的活性分数最高的变元；
赋予初值模块，用于采用所述随机赋值模块产生的随机的初始变元赋予所述多个并行求解器，还用于将所述活性分数最高的变元作为初始变元赋予所述主求解器；
预处理模块，用于解析所述cnf实例的初始化全局变量和文字与子句的关系，并进行优化。
与现有技术相比较，采用本发明的布尔可满足性问题求解方法及系统，采用多个并行求解器在设定的阈值条件内对cnf实例进行多线程并行求解，其中，每个并行求解器采用不同的初始变元；每个并行求解器在触发阈值条件后停止求解，并记录求解过程中各个变元的活性分数；选择所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解，将更符合桥接变量作用的变元作为sat求解器的初始赋值，减少因错选噪声变元为初值而造成时间、空间浪费的可能性，另外，由于选择的变元本身就具有很高活性分数，由于参与冲突越高，活性分数越大，sat求解器一开始就会发生大量的冲突，并且将隐含冲突的其他变元优先选择出来，产生质量较高的学习子句。
附图说明
图1是本发明实施例的布尔可满足性问题求解方法的流程图。
图2示出了依据本发明提出的布尔可满足性问题求解方法对glucose3.0的求解策略进行改进的求解时间与原版glucose3.0的求解时间的对比。
图3是本发明实施例的布尔可满足性问题求解系统的结构示意图。
具体实施方式
本发明中，提供了一种布尔可满足性问题求解方法，其包括：采用多个并行求解器在设定的阈值条件内对cnf实例进行多线程并行求解，其中，每个并行求解器采用不同的初始变元；每个并行求解器在触发阈值条件后停止求解，并记录求解过程中各个变元的活性分数；选择所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解。
具体的，如图1所示，所述布尔可满足性问题求解方法包括步骤s1-s6。下面分别进行说明。
s1：初始化主求解器。
本发明实施例中，所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。
s2：解析cnf实例，并进行预处理。
需要说明的是，cnf实例由多个cnf子句合取而成，每一个cnf子句都是一个与变元有关的逻辑运算。有些变元可能只在一个cnf子句中存在，有些变元可能在多个cnf子句中存在，因此每一个变元的值都会影响cnf实例的运算结果。在cnf子句中，文字是一个变元或是变元的非。
步骤s2中，将解析所述cnf实例的初始化全局变量和文字及子句的关系后，将解析关系映射到储存赋值、活性、与子句关联关系等容器的过程中，同时进行预处理优化操作。例如删除在一个子句内重复出现的文字、单文字传播以及一些推理消除技术等预处理操作。在读取cnf实例文件结束以后，进行例如删除冗余子句、检测被涵盖的子句等预处理技术。
s3：初始化各线程中的并行求解器，每个线程中为各个并行求解器赋予不同的初始变元。
需要说明的是，本发明实施例中，在用于对所述cnf实例的计算机服务器中采用多个并行的线程来对所述cnf实例进行初步求解，从而来获得所述主求解器的初始变元。所述多个并行求解器可以通过克隆所述主求解器得到，也可以采用具有与所述主求解器具有相同分支启发算法、活性增量统一的不同求解器。各个线程中选择随机生成的初始变元，若选择的初始变元在预处理阶段已经被赋值或消除，则重新选择直到初始变元未被选择。
s4：所述多个并行求解器从所述初始变元开始进行求解，在触发设定的阈值条件后停止求解，并记录求解过程中各个变元的活性分数。
需要说明的是，在所述多个并行求解器开始求解前，设置了求解的阈值条件，在求解的过程中，一旦触发到所述阈值条件，就停止求解。所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间，例如，设定冲突次数1000次、重启3次、运行3s。当触发到其中的一个任意一个触发条件时，所述并行求解器停止运行。值得一提地是，许多现代求解器采用地是动态重启策略，例如glucose采用的重启策略是基于学习子句的平均lbd的，如果最新产生的学习子句的lbd平均值较大，则进行重启，所以重启是非常频繁的，平均几百次冲突就会重启一次。
s5：所述多个并行求解器停止求解后，获取各个并行求解器产生的活性分数，选择活性分数之和最高的变元作为主求求解器的初始变元。
需要说明的是，各个并行求解器停止求解后，都会产生一个对变元活性进行记录的序列，将这些序列中每个变元的活性分数进行相加，选择活性分数之和最高的变元作为主求解器的初始变元。由于选择的变元本身就具有很高活性分数，由于参与冲突越高，活性分数越大，sat求解器一开始就会发生大量的冲突，并且将隐含冲突的其他变元优先选择出来，产生质量较高的学习子句。
s6：主求解器求解并输出结果。
如图2所示，依据本发明提出的布尔可满足性问题求解方法对glucose3.0的求解策略进行改进，比对原版glucose3.0的求解时间。其中，实验环境为在同一台64位服务器，服务器配置为intel(r)core(tm)i5-7400cpu@3.00ghz（4cpus）,8192mbram，安装centos7虚拟机linux版本3.10.0-957，gcc版本4.8.5。从图2中可以看出，依据本发明提出的布尔可满足性问题求解方法的改进版本的求解时间均快于原版，且最快可缩短90%。
如图3所示，相应于上述布尔可满足性问题求解方法，本发明实施例中，还提供了一种布尔可满足性问题求解系统，其包括预处理模块1、多个并行求解器2、主求解器3、随机赋值模块4、选择模块5及赋予初值模块6。下面分别进行说明。
所述预处理模块1，用于解析cnf实例的初始化全局变量和文字与子句的关系，并进行优化。
所述多个并行求解器2，用于采用不同的初始变元在设定的阈值条件内对预处理后的cnf实例进行多线程并行求解，并在触发阈值条件后停止求解，记录求解过程中各个变元的活性分数。
所述主求解器3，用于采用所述多个并行求解器2中的活性分数最高的变元作为初始变元，对所述cnf实例进行求解。
所述随机赋值模块4，用于为每个并行求解器2产生一个随机的初始变元。
所述选择模块5，用于选择出所述多个并行求解器得到的活性分数之和最高的变元。
所述赋予初值模块6，用于采用所述随机赋值模块4产生的随机的初始变元赋予所述多个并行求解器2，还用于将所述选择模块5选择的活性分数最高的变元作为初始变元赋予所述主求解器3。
本发明实施例中，所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间。所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。所述多个并行求解器通过克隆所述主求解器得到。
综上所述，采用本发明的布尔可满足性问题求解方法及系统，采用多个并行求解器在设定的阈值条件内对cnf实例进行多线程并行求解，其中，每个并行求解器采用不同的初始变元；每个并行求解器在触发阈值条件后停止求解，并记录求解过程中各个变元的活性分数；选择所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解，将更符合桥接变量作用的变元作为sat求解器的初始赋值，减少因错选噪声变元为初值而造成时间、空间浪费的可能性，另外，由于选择的变元本身就具有很高活性分数，由于参与冲突越高，活性分数越大，sat求解器一开始就会发生大量的冲突，并且将隐含冲突的其他变元优先选择出来，产生质量较高的学习子句。
以上所述仅为本发明的较佳实施例而已，并不用以限制本发明，凡在本发明的精神和原则之内所作的任何修改、等同替换和改进等，均应包含在本发明的保护范围之内。
1.一种布尔可满足性问题求解方法，其特征在于，包括：
采用多个并行求解器在设定的阈值条件内对cnf实例进行多线程并行求解，其中，每个并行求解器采用不同的初始变元；
每个并行求解器在触发阈值条件后停止求解，并记录求解过程中各个变元的活性分数；
选择所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解。
2.如权利要求1所述的布尔可满足性问题求解方法，其特征在于，所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间。
3.如权利要求1或2所述的布尔可满足性问题求解方法，其特征在于，所述多个并行求解器通过克隆所述主求解器得到。
4.如权利要求3所述的布尔可满足性问题求解方法，其特征在于，所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。
5.如权利要求1所述的布尔可满足性问题求解方法，其特征在于，在采用多个并行求解器对cnf实例进行多线程并行求解之前，还包括：
对所述cnf实例进行预处理，解析所述cnf实例的初始化全局变量和文字及子句的关系，并进行优化。
6.一种布尔可满足性问题求解系统，其特征在于，包括：
多个并行求解器，用于采用不同的初始变元在设定的阈值条件内对cnf实例进行多线程并行求解，并在触发阈值条件后停止求解，记录求解过程中各个变元的活性分数；
主求解器，用于采用所述多个并行求解器得到的活性分数之和最高的变元作为主求解器的初始变元，对所述cnf实例进行求解。
7.如权利要求6所述的布尔可满足性问题求解系统，其特征在于，
所述设定的阈值条件包括求解过程中冲突的次数、求解器重启的次数及求解器运行的时间。
8.如权利要求6或7所述的布尔可满足性问题求解系统，其特征在于，所述多个并行求解器通过克隆所述主求解器得到。
9.如权利要求8所述的布尔可满足性问题求解系统，其特征在于，所述主求解器采用以cdcl为算法框架且具有分支启发测策略、子句学习、非时序性回溯、冲突分析、重启策略的sat求解器。
10.如权利要求6所述的布尔可满足性问题求解系统，其特征在于，还包括：
随机赋值模块，用于为每个并行求解器产生一个随机的初始变元；
选择模块，用于选择出所述多个并行求解器中的活性分数最高的变元；
赋予初值模块，用于采用所述随机赋值模块产生的随机的初始变元赋予所述多个并行求解器，还用于将所述活性分数最高的变元作为初始变元赋予所述主求解器；
预处理模块，用于解析所述cnf实例的初始化全局变量和文字与子句的关系，并进行优化。
技术总结