基于OpenMP的并行遗传算法求解SAT问题

为了提高SAT （boolean satisfiability） 问题求解效率,在OpenMP （open multi-processing） 编程框架下,将遗传算法与局部搜索算法结合,改进了混合遗传算法中的选择算法,将原有选择操作的时间复杂度降低到O(N)级别. 算法采用OpenMP中的编译制导语句#pragma omp parallel粗粒度并行化驱动混合遗传算法,采用#pragma omp single语句块实现了子种群间个体的同步迁移操作. 与同类算法HCGA （hybrid cloud genetic algorithm）比较分析表明:改进算法HGA （hybrid genetic algorithm）以及并行后的混合遗传算法CGPHGA （coarse-grained parallel hybrid genetic algorithm）在求解成功率和求解效率上都有显著提高,部分问题求解成功率提高达5倍.      

多元协同演绎在一阶逻辑ATP中的应用

一阶逻辑是数理逻辑中重要的分支,对其逻辑公式的自动推理是人工智能领域重要的研究热点之一. 目前一阶逻辑自动定理证明大多采用二元归结方法，每次只有2个子句进行归结，只消去1组互补对，导致演绎归结式文字数较多，影响了演绎效率. 为此，基于矛盾体分离规则提出了一种多元协同演绎算法，该算法每次允许多个子句进行协同演绎，消去多组互补对，从而演绎分离式文字数较少且可控，能有效提高推理能力；并且，该算法通过有效演绎权重和无效演绎权重调整子句演绎顺序，利用回溯机制搜索较优路径，有效规划演绎路径. 将该算法应用于国际顶尖证明器Eprover 2.1，以CADE2017竞赛例（FOF组）为测试对象，对加入多元协同演绎算法的Eprover 2.1证明器进行试验. 试验结果表明其能力超过了Eprover 2.1:多证明定理8个；能证明Eprover 2.1未证明定理31个，占未证明总数的28.2%.