基于分组的启发式SAT新算法——DC&DS算法

目前提高求解SAT问题完全算法的计算效率问题已成为挑战性研究问题。提出了一种基于启发式分组的SAT完备算法。启发式分组策略将一个全局搜索问题,转为局部搜索问题。并将该策略引入到结合BDD与SAT算法的形式验证中,与一般的启发式SAT算法相比,该算法在求解速度和求解问题的规模等方面都明显地改进了,实验结果表明了该算法的可行性和有效性。     

基于回跳层数的SAT求解器学习子句删除策略

目前学习子句删除策略广泛采用的是基于LBD的评估方式,LBD评估方式在每次执行删除时都会删除前一半LBD值大的学习子句,这种方式对LBD值大的学习子句的删除过于激进。针对此问题,提出了一种利用冲突回跳层数（back-jump levels）的评估方式来保留LBD值较大的相关学习子句。以CDCL（conflict driven clause learning）完备算法为框架,在子句删除环节形成了BJL删除算法。通过测试2017年SAT国际竞赛例,对新改进的版本与原版求解器进行了对比实验。实验表明,所提策略可显著提高求解器的求解性能和求解效率。     

最坏情况下Min-2SAT问题的上界

最坏情况下MaxSAT问题上界的研究已成为一个热门的研究领域.与MaxSAT问题相对的是MinSAT问题,在求解某些组合优化问题时,将其转化为MinSAT问题比转化为MaxSAT问题有着更快的速度,因此对MinSAT问题进行研究.针对Min-2SAT问题提出算法MinSATAlg,该算法首先利用化简算法Simplify对公式进行化简,然后通过分支树的方法对不同情况的子句进行分支.从子句数目的角度分析算法的时间复杂度并证明Min-2SAT问题可在O(1.134 3m)时间内求解,对于每个变量至多出现在3个2-子句中的情况,得到最坏情况下的上界为O(1.122 5n),其中n为变量的数目.     

基于子句权重学习的求解SAT问题的遗传算法

该文提出了一种求解SAT问题的改进遗传算法（SAT—WAGA）．SAT-WAGA算法有多个改进性特点：将SAT问题的结构信息量化为子句权重,增加了学习算子和判定早熟参数,学习算子能根据求解过程中的动态信息对子句权重进行调整,以便防止遗传进程的早熟,同时,算法还采用了最优染色体保存策略,防止进化过程的发散．该文最后描述了实现包括SAT—WAGA等多个算法的实验系统,对选择最佳早熟判定参数值给出了一些有效的建议．实验结果表明：与一般遗传算法相比,SAT—WAGA算法在求解速度、成功率和求解问题的规模等方面都有明显的改善．     

基于频次的SAT问题学习子句混合评估算法

为了有效管理学习子句,避免学习子句规模呈几何级增长,减少冗余学习子句对系统内存占用,从而提高布尔可满足性问题SAT求解器的求解效率,需要对学习子句进行评估,然后删减学习子句。传统的评估方式是基于学习子句的长度,保留较短的子句。当前主流的做法一个是变量衰减和VSIDS的子句评估方式,另外一个是基于文字块距离LBD的评估方式,也有将二者结合使用作为子句评估的依据。通过对学习子句参与冲突分析次数与问题求解的关系进行分析,将学习子句使用频率与LBD评估算法混合使用,既反映了学习子句在冲突分析中的作用,也充分利用了文字与决策层之间的信息。以Syrup求解器（GLUCOSE 4.1并行版本）为基准,在评估算法与并行子句共享策略方面做改进测试,通过实验对比发现,混合评估算法比LBD评估算法有优势,求解问题个数明显增多。     

求解多文字可满足SAT问题的置信传播算法

可满足(SAT)问题是指:是否存在一组布尔变元赋值,使得合取范式公式中每个子句至少有一个文字为真.多文字可满足SAT问题是指:是否存在一组布尔变元赋值,使得CNF公式中每个子句至少有两个文字为真.显然,此问题仍然是一个NP难问题.为了研究解决多文字可满足SAT问题的算法,引入随机实例产生模型,设计求解多文字可满足SAT问题的置信传播算法.最后,用实例模型产生了大量数据进行实验验证,结果表明:该算法求解多文字可满足SAT问题的性能优于其他启发式算法.     

一种SAT邻域的快速搜索算法

用局部搜索算法求解SAT问题．通常都需要在较大的邻域中。寻找合适的邻解。如果对邻域中的每个邻解。都通过重新判断每个子句是否为可满足来得到其可满足的子句个数．则时间耗费较多。已经有一些经典的处理方法．例如通过修改邻域结构．来减小搜索空间。从另外一个角度来考虑搜索过程．根据当前解和邻解的内在关系．介绍一种SAT邻域的快速搜索算法。该算法能在不影响解质量的前提下．快速寻找合适的邻解．从而进一步提高局部搜索算法的求解速度。另外．该算法还提供用于提高解质量的信息。有助于研究新的局部搜索算法。     

求解SAT问题的算法的研究进展

SAT问题是研究最广泛的NPC问题之一。由于SAT问题本身的特性,除非P=NP,否则不存在最坏情况下多项式阶时间复杂度的SAT求解算法。因此设计出高效快速的SAT求解算法至今仍是研究热点。首先简要介绍了SAT问题;其次从完备算法、不完备算法和组合算法3个角度总结了新近的研究进展,深入分析了已有算法解决SAT问题的基本流程,并从适用问题类别、算法特点、求解效率等方面对各类先进的求解器进行了对比分析;最后讨论了求解SAT问题的算法面临的挑战,并对下一步研究工作进行了展望。     

基于参与冲突分析次数的动态学习子句评估策略

针对现有学习子句评估策略的单一性,提出一种基于学习子句参与冲突分析次数的评估策略,并将该策略分别与经典的文字块距离评估策略和活跃值评估策略结合,形成两个动态学习子句评估策略。基于2018年SAT国际竞赛部分基准实例,将动态评估策略与原评估策略进行参数适应性对比实验,并通过2018和2017年的基准实例进行评估。结果表明动态评估策略能更好地评估学习子句的质量,由此生成的求解器在求解数量和速度方面表现出较好的求解性能。     

基于趋势强度的SAT问题学习子句评估算法

针对命题逻辑公式求解过程中难以有效评估学习子句是否有利于后续搜索的问题,提出了一种基于学习子句趋势强度的评估算法。该算法首先通过分析学习子句在生存期内参与冲突分析的时间分布特征,将随机、离散的时间分布转换为连续的累积趋势强度;然后在删除周期达到时,通过设定趋势强度阈值删除在后续搜索过程中“不大可能”被使用的子句,保留“可能”被使用的子句;最后采用2015年、2016年SAT问题国际竞赛实例,将该算法与经典的活跃度评估算法和文字块距离(LBD)评估算法进行对比。实验结果表明,趋势强度评估算法在效率上明显优于活跃度评估算法,且求解的实例更多,同时与LBD算法基本持平。     

基于寻找可满足2SAT子问题的SAT算法*

可满足问题（SAT）是一个NP-Hard问题。提出了一种求解SAT的新算法（FFSAT）。该算法将SAT问题转换为寻找一个可满足的2-SAT子问题。SAT问题虽然是NP完全问题,但是当所有子句长度不大于2时,SAT问题可以在线性时间求解。使用2-SAT算法-BinSat求解2-SAT子问题,当它不满足时,根据赋值选择新的2-SAT子问题。实验结果表明,采用本算法的结果优于UnitWalk。     

基于演绎长度的学习子句删除策略

学习子句删除策略是CDCL-SAT求解器中的一个重要内容,可以避免内存爆炸和加速单元传播。评估学习子句有用性的标准不同导致所删除的学习子句是不同的,极大地影响求解效率。基于CDCL算法的求解过程可被形式化为增加管理学习子句策略的归结演绎过程,基于此,提出一种基于演绎长度的学习子句评估方法,并与现有的基于文字块距离的评估方法结合,根据排序子句的基准不同,形成两种不同的结合算法。采用国际SAT竞赛的基准实例,与目前主流的求解器进行了实验对比分析。结果表明,所提的结合算法能更好地评估学习子句的有用性,较基于文字块距离策略的求解个数提高了4.1%,说明所提策略具有一定的优势。     

SAT问题中局部搜索法的改进

局部搜索方法在求解SAT问题的高效率使其成为一研究热点．提出用初始概率的方法对局部搜索算法中变量的初始随机指派进行适当的约束．使在局部搜索的开始阶段,可满足的子句数大大增加,减少了翻转的次数,加快了求解的速度．用该方法对目前的一些重要的SAT问题的局部搜索算法(如WSAT,TSAT,NSAT,SDF等)进行改进,通过对不同规模的随机3-SAT问题的实例和一些不同规模的结构性SAT问题的实例,以及利用相变现象构造的难解SAT实例测试表明,改进后的这些局部搜索算法的求解效率有了很大的提高．该方法对其他局部搜索法的改进具有参考价值。     

基于加权平均值的一种分支启发式方法

在可满足性(Satisfiability,SAT)问题算法中提出有效的分支策略可以提高求解器的效率,文中主要从冲突分析的角度出发,依据变量是否发生冲突和冲突的次数,提出 一种基于加权平均值的分支启发式方法。该方法首先采用一组序列来记录变量是否参与冲突;其次赋予一个加权平均函数,依据变量的序列和决策层求出函数值;最后选择具有最大的函数值变量赋值,执行实例分析比较。由于该方法是对控制编码方法的改进,因此在进行例子分析时,采用了比较法和分析法,同时分析比较了所提方法、 SUM(Sum in experiment)策略和 ACIDS(Average Conflict-index Decision Score)策略。对SATLIB(SAT Little Information Bank)中的实例进行分析,结果表明所提方法能够实现更多子句被满足或最新冲突子句优先满足。     

O（m^2）时间求解SAT问题的随机算法

传统的求解SAT问题的随机算法主要是对满足解进行搜索,在找不到满足解的情况下,则无法正确判断问题的可满足性。该文提出了两个时间复杂度为O（m^2）求解SAT问题的随机算法SatTestl和SatTest2,这里m为CNF公式中的子句数。这两个随机算法是通过对不满足解数的估计来判断SAT问题的可满足性,不同于传统的随机算法。其中第二个算法SatTest2在搜索满足解的同时又可以对不满足解数进行估计,是对传统随机算法的重要改进。试验结果表明,文中提出的算法对相变区域的难SAT实例有较好的求解能力。     

O(m~2)时间求解SAT问题的随机算法

传统的求解 SAT问题的随机算法主要是对满足解进行搜索 ,在找不到满足解的情况下 ,则无法正确判断问题的可满足性 .该文提出了两个时间复杂度为 O( m2 )求解 SAT问题的随机算法 Sat Test1和 Sat Test2 ,这里 m为CNF公式中的子句数 .这两个随机算法是通过对不满足解数的估计来判断 SAT问题的可满足性 ,不同于传统的随机算法 .其中第二个算法 Sat Test2在搜索满足解的同时又可以对不满足解数进行估计 ,是对传统随机算法的重要改进 .试验结果表明 ,文中提出的算法对相变区域的难 SAT实例有较好的求解能力 .     

基于加强概率控制策略的SAT局部搜索算法

局部搜索算法是目前求解SAT问题比较有效的方法,而Sattime算法是在SAT国际大赛中获得大奖的一种典型局部搜索算法。在Sattime算法的求解过程中,记录变元翻转事件流数据库,通过数据分析与模式挖掘,发现Sattime算法的局部搜索行为中会出现相邻搜索步选择同一个变元的现象,即所谓的回环现象,从而降低了求解效率。为解决此问题,提出两种概率控制策略：加强子句选择策略和加强变元选择策略,并将这两种策略应用到Sattime算法中,形成新的局部搜索算法Sattime-P。实验结果表明,与Sattime算法相比,改进后的Sattime-P算法求解效率有显著的提升。该方法也对其他局部搜索算法的改进具有参考价值。     

MAX-SAT问题一种改进的局部搜索算法

局部搜索算法是求解大规模SAT问题的高效算法。经典的局部搜索算法有GSAT、WSAT、TSAT、NSAT等,但这些算法的初始解都是随机产生的。本文提出了用单纯形法产生“初始概率”（每个变量取1的概率）,用“初始概率”对局部搜索算法中变量的初始随机指派进行适当的约束,使在局部搜索的开始阶段,满足的子句数大大增加,加快了收敛的速度。通过对不同规模的随机STA问题实例的实验表明,这些改进有效地提高了局部搜索算法求解SAT问题的效率。     

一个求解结构SAT问题的高效局部搜索算法

逻辑表达式可满足性(SAT)问题是第一个被证明的NP完全问题.它也是解决人工智能和计算理论中许多实际问题的基础.人们发现,对于某些类型的SAT问题,局部搜索算法要比一些传统的算法(例如Davis-Putnam过程)更为有效.在本文中,我们主要讨论如何用局部搜索算法求解结构SAT问题.我们对一个典型的局部搜索算法GSAT+walk做了改进与扩展.首先,我们除去了GSAT+walk中GSAT部分的"平移";其次,我们给每一个子句赋权,并在GSAT+walk的搜索过程中动态地调整子句的权.文中给出的实验结果表明改进后的新算法对于求解结构SAT问题非常有效.     

基于学习子句删除策略的SAT求解器分支策略

对于SAT求解器,目前流行的分支变量决策策略大多是基于冲突的变量活跃度评估算法,选择具有最大活性的未赋值变量作为决策变量,优先解决最近的冲突.但是,它们都忽略了包含决策变量的子句数目对布尔约束传播(BCP)的影响.针对此问题,提出了 一种基于学习子句删除策略的分支变量决策策略(VDALCD),在删除学习子句的同时减小被删除子句中变量的活跃度.基于VDALCD策略分别对Glucose4.1,MapleLCMDistChronoBT-DL-v2.1进行改进,形成了求解器Glucose4.1_VDALCD和Maple-DL_VDALCD.以2018年、2019年SAT国际竞赛题为基准测试例,将改进版本与原版本求解器进行比较.实验结果表明,在2018年的例子测试中,Gluose4.1_VDALCD比Gluose4.1多求出26个例子,增加了 15.5％.在2019年的例子测试中,Maple-DL_VDALCD 比 MapleLCMDistChronoBT-DL-v2.1 多求出 17个例子,增加了 7.6％.