论文部分内容阅读
摘 要：可满足性问题是著名的np难问题，骨干集是可满足性问题的重要结构。随着人工智能的快速发展，也给求解可满足性问题提供了更多的方法。本文通过分析决策树算法划分数据的关键原理，寻求决策树数据集与可满足性赋值之间的关系，探索新的求解命題公式骨干集的方法。
关键词：可满足性问题;决策树算法;骨干集;可满足赋值
约束满足性问题（Constraint Satisfaction Problem，CSP）是人工智能领域的重要问题[1-3]，它不仅给许多理论问题提供了一个框架，在实际生活中也有很多的应用。可满足性问题（SAT问题）是典型的CSP问题[4]，SAT 问题的 NP-完全性表明，在 P ！=NP 的情况下，不存在多项式时间算法求解该问题。在对可满足问题的不断研究中发现，骨干集是SAT问题中一类特殊变元的集合，它的大小构成了SAT问题的求解难度，骨干集越大，可满足性问题越难求解，因此求解可满足问题骨干集也是NP难问题。
一、可满足性问题介绍
可满足问题的判定是指，是否存在一组0与1赋值的组合，能够使得命题公式的值为1（称为True）。当命题公式为True时，则称该命题公式是可满足的，若找不到一组赋值组合能够使命题公式为True，则称其为不可满足的。由于不可满足的命题公式只有一个False标签，因此本文的决策树算法求解命题公式骨干集主要从可满足命题公式来进行探索。
在可满足性问题中，由不同的变元和析取成子句，不同的子句合取组成命题公式F。例如：。变元的取值只有0和1两种情况，那么公式F的一组可满足性赋值为（0，1，0）;不可满足的赋值为（1，1，1）。同时，不难看出，只有X1的取值为0时，第一个子句的值才能为1，才能使整个公式满足，说明第一个子句的可满足性完全依赖于X1，而整个命题公式的可满足性依赖于第一个子句。因此，我们称具有这种性质的变元叫做骨干变元，由这样相同性质的变元组成的集合为骨干集。
二、决策树算法介绍
决策树算法是一种无限逼近函数值的归纳分类算法，多用于机器学习和数据挖掘领域。决策树算法是树状结构，通过对无序的训练集进行学习，提炼出有序的规律，从而达到对目标集进行归纳分类的目的。
一个决策树结构包含根节点、若干内部节点以及若干叶子节点。决策树有且只有一个根节点，并其根节点位于顶层，代表第一个测试条件。内部节点位于根节点和叶子结点的中间，每一个内部节点都代表着一种测试条件，若干个内部节点组成了若干个不同的测试条件。叶子节点则代表测试结果，位于树结构的最下层。
本文所提出的决策树求解命题公式的骨干集算法主要是利用决策树寻找最佳分类点的思想，在命题公式众多可满足与不可满足的赋值数据中，找到决定命题公式的为True的骨干变元。
目前，经典的决策树算法有三种：Quinlan在1986年提出的ID3算法、在1993年提出的C4.5算法，以及Breiman等人在1984年提出的CART（Classification and Regression Tree）算法，本文主要探究的决策树最基础的ID3算法和C4.5算法求解骨干集。
（一）ID3算法
ID3算法是决策树算法的基础算法，决策树算法的本质是对数据进行分类处理，找到一组分类规则，在决策树上以节点—分支—节点的形式表示，算法通过输入训练样本集来进行学习生成决策树。核心原理是计算带有标签T或F数据集的属性的信息增益，属性的信息增益越大，表明该属性对分类结果有最大的影响，因此在分类过程中，ID3算法的每一步都选择具有最大信息增益的属性作为节点对数据进行分类，分类后的数据集再次计算信息增益，选择最大的属性作为节点，循环迭代，直到数据的分类都只有一种情况为止。
（二）C4.5算法
C4.5和CART算法是ID3算法的扩展与延申，由于ID3算法在计算时考虑到不同的分支结点所包含的样本数不同，给分支结点赋予的权重即样本数越多的分支结点影响就越大。
所以ID3算法会倾向于特征选项较多的特征，因此C4.5对目标函数进行了调整，通过计算信息增益率对数据进行分类，并且在树的构造过程中进行剪枝优化，使分类更加准确。
三、决策树算法求解骨干集
决策树算法的数据集一般由属性，属性值和标签组成。一般来说，决策树算法用于分来是十分准确的，但是不是用来分类，是利用决策树求解最佳分类属性的思想来求解命题公式骨干集。我们简单把数据集分成T与F两个类，相当于数据的两类标签。这里也可以解释不可满足的命题公式骨干集是不能用决策树算法求解的，因为不可满足的命题公式只有False的取值，无法根据标签来计算变元的信息增益。由此可知，可满足性命题公式的赋值有T与F的两类标签的数据集，将可满足性公式赋值的集合进行数据处理，变元为属性，0与1为属性的取值。对于ID3算法，用ID3算法的原理求解原始数据集的属性的信息增益，将算得信息增益最大的变元为命题公式的骨干变元，将该变元从原始数据集删除后，继续对剩下得数据集求解骨干变元，迭代计算，直至数据集的标签只有一类为止，此时可知叶节点的数据集都是纯的（不可再分），这样所得节点集合即为命题公式骨干集。
由于C4.5算法是在ID3算法上扩展的算法，改变了目标函数，使ID3算法不倾向于选值较多的特征，但是在应用到命题公式求解骨干集时并不优秀。这是由于求信息增益率是针对变元取值得，由于命题公式变元只会取0和1两个属性值，并不存在属性值选项较多的情况，也就不会由于属性取值过多而倾向于某个属性。因此C4.5算法在原理上对求解命题公式骨干集的效果与ID3是一样的，并不适用于求解骨干集。
四、总结
本文分析了求解可满足性问题骨干集的重要性，并且从决策树的基本原理研究如何将决策树算法应用到求解命题公式骨干集中，这样可以为今后能够设计出高效快速的SAT求解器提出一个新的思考方向。
参考文献：
[1]Dyer M， Frieze A， Molloy M. A probabilistic analysis of randomly generated binary constraint satisfaction[J]. Theoretical Computer Science， 2003， 290（3）：1815-1828.
[2]Creignou N， Daudé H. The SAT–UNSAT transition for random constraint satisfaction problems[J]. Discrete Mathematics， 2009， 309（8）：2085-2099.
[3]Gaspers S， Papadimitriou C， S H， et al. On satisfiability problems with a linear structure[J]. arXiv preprint arXiv：1602.07876， 2016.
[4]Benjamin D， Frank N， Andrew S. Time complexity analysis of evolutionary algorithms on random satisfiable k-CNF formulas[J]. Algorithmica， 2017， 78（2）： 561-586.
基金项目：北方民族大学创新项目《数据分类算法在可满足性判定问题中的应用研究》;项目编号：YCX19076
关键词：可满足性问题;决策树算法;骨干集;可满足赋值
约束满足性问题（Constraint Satisfaction Problem，CSP）是人工智能领域的重要问题[1-3]，它不仅给许多理论问题提供了一个框架，在实际生活中也有很多的应用。可满足性问题（SAT问题）是典型的CSP问题[4]，SAT 问题的 NP-完全性表明，在 P ！=NP 的情况下，不存在多项式时间算法求解该问题。在对可满足问题的不断研究中发现，骨干集是SAT问题中一类特殊变元的集合，它的大小构成了SAT问题的求解难度，骨干集越大，可满足性问题越难求解，因此求解可满足问题骨干集也是NP难问题。
一、可满足性问题介绍
可满足问题的判定是指，是否存在一组0与1赋值的组合，能够使得命题公式的值为1（称为True）。当命题公式为True时，则称该命题公式是可满足的，若找不到一组赋值组合能够使命题公式为True，则称其为不可满足的。由于不可满足的命题公式只有一个False标签，因此本文的决策树算法求解命题公式骨干集主要从可满足命题公式来进行探索。
在可满足性问题中，由不同的变元和析取成子句，不同的子句合取组成命题公式F。例如：。变元的取值只有0和1两种情况，那么公式F的一组可满足性赋值为（0，1，0）;不可满足的赋值为（1，1，1）。同时，不难看出，只有X1的取值为0时，第一个子句的值才能为1，才能使整个公式满足，说明第一个子句的可满足性完全依赖于X1，而整个命题公式的可满足性依赖于第一个子句。因此，我们称具有这种性质的变元叫做骨干变元，由这样相同性质的变元组成的集合为骨干集。
二、决策树算法介绍
决策树算法是一种无限逼近函数值的归纳分类算法，多用于机器学习和数据挖掘领域。决策树算法是树状结构，通过对无序的训练集进行学习，提炼出有序的规律，从而达到对目标集进行归纳分类的目的。
一个决策树结构包含根节点、若干内部节点以及若干叶子节点。决策树有且只有一个根节点，并其根节点位于顶层，代表第一个测试条件。内部节点位于根节点和叶子结点的中间，每一个内部节点都代表着一种测试条件，若干个内部节点组成了若干个不同的测试条件。叶子节点则代表测试结果，位于树结构的最下层。
本文所提出的决策树求解命题公式的骨干集算法主要是利用决策树寻找最佳分类点的思想，在命题公式众多可满足与不可满足的赋值数据中，找到决定命题公式的为True的骨干变元。
目前，经典的决策树算法有三种：Quinlan在1986年提出的ID3算法、在1993年提出的C4.5算法，以及Breiman等人在1984年提出的CART（Classification and Regression Tree）算法，本文主要探究的决策树最基础的ID3算法和C4.5算法求解骨干集。
（一）ID3算法
ID3算法是决策树算法的基础算法，决策树算法的本质是对数据进行分类处理，找到一组分类规则，在决策树上以节点—分支—节点的形式表示，算法通过输入训练样本集来进行学习生成决策树。核心原理是计算带有标签T或F数据集的属性的信息增益，属性的信息增益越大，表明该属性对分类结果有最大的影响，因此在分类过程中，ID3算法的每一步都选择具有最大信息增益的属性作为节点对数据进行分类，分类后的数据集再次计算信息增益，选择最大的属性作为节点，循环迭代，直到数据的分类都只有一种情况为止。
（二）C4.5算法
C4.5和CART算法是ID3算法的扩展与延申，由于ID3算法在计算时考虑到不同的分支结点所包含的样本数不同，给分支结点赋予的权重即样本数越多的分支结点影响就越大。
所以ID3算法会倾向于特征选项较多的特征，因此C4.5对目标函数进行了调整，通过计算信息增益率对数据进行分类，并且在树的构造过程中进行剪枝优化，使分类更加准确。
三、决策树算法求解骨干集
决策树算法的数据集一般由属性，属性值和标签组成。一般来说，决策树算法用于分来是十分准确的，但是不是用来分类，是利用决策树求解最佳分类属性的思想来求解命题公式骨干集。我们简单把数据集分成T与F两个类，相当于数据的两类标签。这里也可以解释不可满足的命题公式骨干集是不能用决策树算法求解的，因为不可满足的命题公式只有False的取值，无法根据标签来计算变元的信息增益。由此可知，可满足性命题公式的赋值有T与F的两类标签的数据集，将可满足性公式赋值的集合进行数据处理，变元为属性，0与1为属性的取值。对于ID3算法，用ID3算法的原理求解原始数据集的属性的信息增益，将算得信息增益最大的变元为命题公式的骨干变元，将该变元从原始数据集删除后，继续对剩下得数据集求解骨干变元，迭代计算，直至数据集的标签只有一类为止，此时可知叶节点的数据集都是纯的（不可再分），这样所得节点集合即为命题公式骨干集。
由于C4.5算法是在ID3算法上扩展的算法，改变了目标函数，使ID3算法不倾向于选值较多的特征，但是在应用到命题公式求解骨干集时并不优秀。这是由于求信息增益率是针对变元取值得，由于命题公式变元只会取0和1两个属性值，并不存在属性值选项较多的情况，也就不会由于属性取值过多而倾向于某个属性。因此C4.5算法在原理上对求解命题公式骨干集的效果与ID3是一样的，并不适用于求解骨干集。
四、总结
本文分析了求解可满足性问题骨干集的重要性，并且从决策树的基本原理研究如何将决策树算法应用到求解命题公式骨干集中，这样可以为今后能够设计出高效快速的SAT求解器提出一个新的思考方向。
参考文献：
[1]Dyer M， Frieze A， Molloy M. A probabilistic analysis of randomly generated binary constraint satisfaction[J]. Theoretical Computer Science， 2003， 290（3）：1815-1828.
[2]Creignou N， Daudé H. The SAT–UNSAT transition for random constraint satisfaction problems[J]. Discrete Mathematics， 2009， 309（8）：2085-2099.
[3]Gaspers S， Papadimitriou C， S H， et al. On satisfiability problems with a linear structure[J]. arXiv preprint arXiv：1602.07876， 2016.
[4]Benjamin D， Frank N， Andrew S. Time complexity analysis of evolutionary algorithms on random satisfiable k-CNF formulas[J]. Algorithmica， 2017， 78（2）： 561-586.
基金项目：北方民族大学创新项目《数据分类算法在可满足性判定问题中的应用研究》;项目编号：YCX19076