变元的赋值顺序及赋值优化算法、布尔可满足性验证算法

摘要

本发明公开了一种变元的赋值顺序及赋值优化算法、布尔可满足性验证算法。其中分支启发的变元的赋值顺序优化算法，至少一个变元采用以下步骤确定赋值顺序：将当前待赋值的变元作为当前变元；搜索与当前变元同时出现在同一子句中的关联变元；累计所述关联变元与当前变元同时出现在同一子句中的次数；选择次数最少的关联变元作为继当前变元之后的待赋值的变元。本发明可以加快分支启发算法的计算时间。

说明书

技术领域

本发明涉及等价性验证工具中的布尔可满足性验证技术领域，尤其涉及分支启发的变元的赋值顺序优化算法、分支启发的变元的赋值优化算法，以及采用了该赋值优化算法的布尔可满足性验证算法。

背景技术

布尔可满足性验证算法通常包含三个主要部分：分支启发算法、演绎机制和BCP(即BCP传播)、以及冲突分析和学习。

在布尔可满足性验证过程中，BCP传播占用大部分的时间，一个好的分支启发策略可以快速找到决策变元，减少冲突次数，加速BCP过程，因此，好的分支启发策略对提高整个布尔可满足性验证工具的运行效率意义重大。现有使用最多的是VSIDS分支启发策略，相比早期的分支启发(出现次数最多优先、最短字句出现频率最大优先、最短正子句优先、DLIS、DLCS)，VSIDS分支启发策略可以更好的结合冲突分析过程，大大缩减BCP时间。以下为VSIDS算法的主要过程：

1、每一个变元的正、负文字都分配一个计数器s，并且初始值为0；

2、当学习子句加入到子句集时，该子句中所有的文字活性加1；

3、所有文字的活性分数定期除以一个大于1的常数；

4、每次分支决策时选择计数器分值最高未赋值的文字进行赋值，在有多个相等计数器的情况下，随机选择一个文字进行赋值。

在搜索的初始阶段，由于冲突次数较少，VSIDS的活性分数是不准确的，因此通过活性所选择的分支决策具有一定的随机性。简单的说：如果把蕴含图根据连接关系分解为社区结构，我们不确定所选择的自由变元在社区内部还是联接各个社区结构之间的桥接变量。只有随着时间的推移，才能使VSIDS所选择的变元具备一定的质量水平，此时所习得的学习子句质量也更高。

另一方面，初始变元的选择，直接影响整个搜索过程，选择不好的初始变元，在求解过程中虽然会产生大量冲突，但所习得的学习子句通常质量较低，会在子句库删减操作中删除。对于大多数求解器，都是采用随机赋值的方式选择初始变元，这就会使求解过程的开始阶段具备一定的局部性，即求解器此时主要关心初始变元所在的社区结构，也通常从最近的社区结构中挑选变元做分支决策，发生冲突并产生学习子句，然后才逐步扩散至桥接变量和其他社区结构。然而，桥接变量与其他社区结构的所产生的学习子句更能反应SAT问题实例的组织关系。所有造成了时间和空间的浪费。

发明内容

为了解决现有技术中随机选择变元进行赋值导致计算效率较低的技术问题，本发明提出一种变元的赋值顺序及赋值优化算法、布尔可满足性验证算法。

其中分支启发的变元的赋值顺序优化算法，至少一个变元采用以下步骤确定赋值顺序：

步骤1，将当前待赋值的变元作为当前变元；

步骤2，搜索与当前变元同时出现在同一子句中的关联变元；

步骤3，累计所述关联变元与当前变元同时出现在同一子句中的次数；

步骤4，选择次数最少的关联变元作为继当前变元之后的待赋值的变元。

进一步，所述步骤4执行完毕后返回步骤1，直至同一字句的所有的变元的赋值顺序确定。

进一步，所述当前待赋值的变元为分支启发的第一个待赋值的变元或者为子句的第一个待赋值的变元。

进一步，所述分支启发的第一个待赋值的变元通过对CNF文件每个变元的权重进行计算，选择所述权重最高的变元作为SAT求解器的第一个待赋值的变元。

进一步，所述对CNF文件中每个变元的权重进行计算，包括：

将CNF文件中的所有文字以子句为单位读入一个二维容器之中；

对所述存放子句的二维容器进行遍历分别计算CNF文件中每个待赋值的变元的权重。

进一步，计算每个待赋值的变元的权重具体包括：

在遍历子句的过程中，当某个待赋值的变元出现在某个子句中，则根据公式

直至所有子句遍历完成，得到所有待赋值的变元的权重。

本发明提出的分支启发的变元的赋值优化算法，采用上述技术方案所述的变元的赋值顺序优化算法确定变元的赋值顺序，当任意一个变元的赋值顺序被确定时，包括如下赋值步骤：

对待赋值的变元进行第一次赋值；

计算赋值以后所述待赋值的变元在分支启发中发生n次冲突的第一时间；

将第一次赋值的值进行取反并以取反后的值对待赋值的变元进行第二次赋值；

计算赋值以后所述待赋值的变元在分支启发中发生n次冲突的第二时间；

比较第一时间和第二时间，选择时间短的那次赋值的值对待赋值的变元进行赋值。

进一步，所述待赋值的变元的第一次赋值的值为1。

本发明提出的布尔可满足性验证算法，在对CNF文件进行布尔可满足性验证时，采用上述技术方案所述的分支启发的变元的赋值优化算法对各个变元进行赋值。

本发明针对现有技术中VSIDS分支启发策略存在的不足，根据权重确定第一个待赋值的变元，并提出变元关联度的概念，即子句中同时出现两个变元的次数，并通过变元之间关联度的大小进行分支启发的决策。关联度越大的变元，赋值其中一个变元后，那么下一个变元的赋值就可以选取与这个变元相关度大的变元，就可以尽快的产生更多的冲突，从而产生学习子句，有益于后续的计算，即降低计算时间。将本发明的算法基于Glucose3.0进行测试，测试数据如表1所示，新提出的算法最多可以节省95％的处理时间，另外本发明在确定变元的赋值结果时，计算发生n次冲突的时间t1,再将该变元的赋值取反，计算发生n次冲突的时间t2,取时间短的赋值进行下一次分支启发赋值，或者取相同时间内发生冲突最多的变元赋值对当前待赋值的变元进行赋值，还可以采用相同的方式进行下一次分支启发赋值。通过本发明可以尽快找到符合变元的赋值，加快计算时间，具体测试时间的优化如表2所示，最好的例子中计算时间减少97％，平均时间减少50％以上。

本发明涉及到的技术术语如下：

·变元：在命题逻辑中，bool变元x

·文字：变元x

·子句：一些文字的析取，例如

·CNF公式：一些子句的合取，例如

·SAT问题：布尔可满足性问题Boolean Satisfiability Problem。即，判断能否找出一组赋值，使得给定的CNF公式中的所有子句满足。

·自由变元：未被赋值的变元。在所有的最开始，所有的变元都是自由变元。

·分支决策：在所有自由变元中选择某个变元并赋予某个值，称为分支决策。

·单子句：只包含一个文字的子句。在SAT问题中，应该给其文字赋相应的值使得单子句满足。给单子句中的文字赋值后，会导致其他的文字被赋值，此过程即为单子句传播。·BCP传播：给单子句中的文字赋值后，会导致其他的文字被赋值，此过程即为单子句传播，也成为BCP传播。

·产生冲突：单子句传播过程中，不同的单子句传播要求同一变元取相反的值，则出现冲突。

·分支启发策略：更快的找到下一次传播的变元，加速BCP过程，减少回溯次数，最著名的分支策略为VSIDS。

学习子句、子句学习：在搜索的过程中，每次产生冲突，就对产生当前冲突的子句集进行消解，得到一个新的子句，称为学习子句，并添加到子句库中，用来避免未来产生同样的冲突。这一过程称为子句学习。

附图说明

下面结合实施例和附图对本发明进行详细说明，其中：

图1是本发明的流程图。

具体实施方式

为了使本发明所要解决的技术问题、技术方案及有益效果更加清楚明白，以下结合附图及实施例，对本发明进行进一步详细说明。应当理解，此处所描述的具体实施例仅用以解释本发明，并不用于限定本发明。

由此，本说明书中所指出的一个特征将用于说明本发明的一个实施方式的其中一个特征，而不是暗示本发明的每个实施方式必须具有所说明的特征。此外，应当注意的是本说明书描述了许多特征。尽管某些特征可以组合在一起以示出可能的系统设计，但是这些特征也可用于其他的未明确说明的组合。由此，除非另有说明，所说明的组合并非旨在限制。

下面结合附图以及实施例对本发明的原理进行详细说明。

本发明的赋值顺序优化算法，指的是分支启发的所有变元当中至少有一个变元采用了以下步骤来确定赋值顺序。

将当前待赋值的变元作为当前变元，接着搜索与当前变元同时出现在同一子句中的关联变元，累计该关联变元与当前变元同时出现在同一子句中的次数，然后选择次数最多的关联变元作为继当前变元之后的待赋值的变元。本发明提出了变元关联度的概念，即子句中同时出现两个变元的次数，并通过变元之间关联度的大小进行分支启发的决策，赋值其中一个变元后，那么下一个变元的赋值就可以选取与这个变元相关度大的变元。

图1示出了本发明的赋值顺序优化算法的一个较优实施例，将当前待赋值的变元设定为分支启发的第一个待赋值的变元(即整个CNF文件的第一个待赋值的变元)，那么第一个待赋值的变元所在的子句的第二个待赋值的变元就可以通过上述技术方案来获得，进而该变元所在子句的所有变元的赋值顺序均可以通过上述技术方案来确定赋值顺序。当第二个待赋值的变元采用本发明的技术方案来确定时，其优化效果如下表所示，基于VSIDS算法的特性，越早采用本发明的上述技术方案来确定变元的赋值顺序，其优化效果也将越明显。

表1测试数据

分支启发的第一个待赋值的变元是通过对CNF文件每个变元的权重进行计算，选择权重最高的变元作为SAT求解器的第一个待赋值的变元。因为在搜索的初始阶段，由于冲突次数较少，VSIDS的活性分数是不准确的，因此通过活性所选择的分支决策具有一定的随机性。初始变元的选择，直接影响整个搜索过程，选择不好的初始变元，在求解过程中虽然会产生大量冲突，但所习得的学习子句通常质量较低，会在子句库删减操作中删除。因此，本发明的分支启发的第一个待赋值的变元是通过对CNF文件每个变元的权重进行计算，然后选择权重最高的变元作为SAT求解器的第一个待赋值的变元。

下面详细介绍分支启发的第一个待赋值的变元的确认过程。

将CNF文件中的所有文字以子句为单位读入一个二维容器之中；

对存放子句的二维容器进行遍历以分别计算CNF文件中每个待赋值的变元的权重。

在遍历子句的过程中，当某个待赋值的变元出现在某个子句中，则根据公式

当一个变元出现在越多的子句中，则分数越大，越优先被赋值。当所有子句被遍历完毕时，可以得到所有变元的权重的结果，从中找到最大权重的变元作为分支启发的第一个待赋值的变元。本发明以权重为基础进行的第一个分支变元的选择可以消除随机选择的不确定性，将可能蕴含更多冲突的变元优先赋值。一个优秀的初次分支变元的选择将会减少解算过程中冲突的产生，加快解算速度。

当分支启发的第一个待赋值的变元确定以后，随之该第一个待赋值的变元所在的子句的所有变元的赋值顺序可以根据上述技术方案来确定，在这个子句的变元的赋值顺序确定完毕且赋值完毕之后，其他子句的变元的赋值顺序的确定，可以根据VSIDS算法来确定赋值的顺序并赋值，也可以根据VSIDS算法确定到某一个子句(至少是第二个被赋值的子句，如第二、第三个被赋值的子句，直至最后一个被赋值的子句)的第一个待赋值的变元以后，采用上述技术方案中寻找与当前变元关联度最大的策略来依次确定该子句的所有变元的赋值顺序，直到所有子句的所有变元的赋值顺序被确定。

确定完任意一个待赋值的变元的顺序，就可以根据现有的VSIDS算法来对该待赋值的变元进行赋值。

在一个进一步的较优实施例中，确定完任意一个待赋值的变元的顺序，可以采用以下的技术方案来对待赋值的变元进行赋值，或者说可以采用以下的步骤来确定至少一个变元的赋值的值。

对待赋值的变元进行赋值的步骤主要过程如下：

对待赋值的变元进行第一次赋值，在本实施例中，第一次赋值的值默认取1；

计算赋值以后该待赋值的变元在分支启发中发生n次冲突的第一时间；

将第一次赋值的值进行取反，并以取反后的值对待赋值的变元进行第二次赋值，即第二次赋值的值为0；

计算赋值以后该待赋值的变元在分支启发中发生n次冲突的第二时间，n的具体取值由本领域内技术人员根据实际情况所取的经验值，例如当冲突有1000次以上时，此时n可以取1000；

比较第一时间和第二时间，选择时间短的那次赋值的值对待赋值的变元进行赋值，例如赋值为0时，产生1000次冲突所花的第二时间更短，则第一个待赋值的变元赋值为0，如果赋值为1时，产生1000次冲突所花的第一时间更短，则第一个待赋值的变元赋值为1。

之后其他待赋值的变元以及到最后一个待赋值的变元可以依旧按照VSIDS算法的常规赋值方式进行赋值，也可以依照上述技术方案进行赋值，直到所有的待赋值的变元赋值完毕，。

当分支启发的第一个待赋值的变元(即权重最高的变元)采用上述实施例的技术方案进行赋值，其他变元擦采用传统的VSIDS算法进行赋值的话，经过测试，可以得到以下的测试数据：

表2

从上述测试数据可以看出，在最好的例子中分支启发算法的计算时间减少97％，而平均时间可以减少50％以上。

如果分支启发的变元中第一个待赋值的变元至最后一个待赋值的变元均采用上述赋值步骤进行赋值，将会大大减少分支启发算法的计算时间，提高分支启发算法的计算效率，进而提高布尔可满足性验证算法的效率。

本发明同时还保护布尔可满足性验证算法，在对CNF文件进行布尔可满足性验证时，采用上述任一一项技术方案所述的分支启发的变元的赋值优化算法对各个变元进行赋值。

以上所述仅为本发明的较佳实施例而已，并不用以限制本发明，凡在本发明的精神和原则之内所作的任何修改、等同替换和改进等，均应包含在本发明的保护范围之内。