SAT(Satisfiability)可满足性问题研究具有很广的应用价值,是计算机和人工智能领域内的一个重要问题,也是第一个被证明为NP完全的问题。随着对SAT问题的深入研究,已经提出了很多高效的算法,其中随机算法(WalkSAT)、进化算法等启发式算...SAT(Satisfiability)可满足性问题研究具有很广的应用价值,是计算机和人工智能领域内的一个重要问题,也是第一个被证明为NP完全的问题。随着对SAT问题的深入研究,已经提出了很多高效的算法,其中随机算法(WalkSAT)、进化算法等启发式算法是今年来研究的热点。进化算法是遗传算法的一种,通过对生物组织进化的学习,形成的一种高效算法。针对CNF(Con-jecture Normal Formula)权重和生物进化算法相结合,提出一种有效求解难SAT问题的不完全算法WOSAT.展开更多
为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一...为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一类有向图——BF(bounded flips)图。研究带翻转控制参数的BF图的若干基础性质,根据BF图的性质研究CNF公式可满足解的概率性质。对于含有n个变元m个子句CNF公式,随着翻转控制参数k的增大,在其BF图上取得可满足解的概率也相应增大。当k靠近n时,概率稳定。对于可满足的CNF公式,在其任意k值下的BF图上进行t次随机游走。当t足够大时,取得可满足解的概率最终会收敛于1。最后,实验仿真支持性质的正确性。展开更多
文摘SAT(Satisfiability)可满足性问题研究具有很广的应用价值,是计算机和人工智能领域内的一个重要问题,也是第一个被证明为NP完全的问题。随着对SAT问题的深入研究,已经提出了很多高效的算法,其中随机算法(WalkSAT)、进化算法等启发式算法是今年来研究的热点。进化算法是遗传算法的一种,通过对生物组织进化的学习,形成的一种高效算法。针对CNF(Con-jecture Normal Formula)权重和生物进化算法相结合,提出一种有效求解难SAT问题的不完全算法WOSAT.
文摘为分析合取范式(conjunctive normal form,CNF)公式的赋值空间在可满足性情况下的结构性质,引入一个变元翻转次数控制的参数k,k不小于1且不大于n,n为公式中出现的变元个数,以赋值作为结点,基于翻转界控制下赋值满足子句数的大小,引入一类有向图——BF(bounded flips)图。研究带翻转控制参数的BF图的若干基础性质,根据BF图的性质研究CNF公式可满足解的概率性质。对于含有n个变元m个子句CNF公式,随着翻转控制参数k的增大,在其BF图上取得可满足解的概率也相应增大。当k靠近n时,概率稳定。对于可满足的CNF公式,在其任意k值下的BF图上进行t次随机游走。当t足够大时,取得可满足解的概率最终会收敛于1。最后,实验仿真支持性质的正确性。