检索结果-内蒙古大学图书馆

东北大学学报（自然科学版） 2022年第4期43卷 463-469页

作者：韩淑婷赖永刘杰吉林大学计算机科学与技术学院吉林长春130012 吉林大学符号计算与知识工程教育部重点实验室吉林长春130012

模型计数是求给定命题公式的模型数,是人工智能领域的一个基本问题.在贝叶斯网络、有界模型检测、精确集合覆盖等众多实际问题中,存在许多exactly-one约束.常见的处理方法是将exactly-one约束编码为CNF公式,再调用模型计数器求解.这种... 详细信息

模型计数是求给定命题公式的模型数,是人工智能领域的一个基本问题.在贝叶斯网络、有界模型检测、精确集合覆盖等众多实际问题中,存在许多exactly-one约束.常见的处理方法是将exactly-one约束编码为CNF公式,再调用模型计数器求解.这种方法扩大了命题公式的规模,容易导致求解时间过长.本文分别提出从CNF公式中还原exactly-one约束的ECR算法和处理exactly-one约束的ECP算法.ECR算法能明显提高C2D编译器的求解效率.基于最新的模型计数器ExactMC,本文改进了能识别和单独处理exactly-one约束的模型计数器ECMC.实验结果表明,ECMC的时间效率相比ExactMC有显著提高.

关键词： exactly-one约束模型计数二元约束传播合取范式 C2D

来源：评论

学校读者我要写书评

暂无评论

伪布尔约束的一种模型计数方法

引用

计算机科学 2024年第S02期51卷 150-154页

作者：郑苏豪牛秦洲陶小梅桂林理工大学信息科学与工程学院广西桂林541006 广西师范大学计算机科学与工程学院、软件学院广西桂林541006

伪布尔约束问题是一类与布尔约束问题相似的组合优化难题。解决这类问题的核心在于以不同的数学形式对伪布尔约束进行编码,例如线性规划、整数规划以及其他形式的组合优化。当前流行的解决方法是将问题转化为布尔公式,然后运用冲突导向... 详细信息

伪布尔约束问题是一类与布尔约束问题相似的组合优化难题。解决这类问题的核心在于以不同的数学形式对伪布尔约束进行编码,例如线性规划、整数规划以及其他形式的组合优化。当前流行的解决方法是将问题转化为布尔公式,然后运用冲突导向的子句学习(CDCL)类SAT求解器对这些布尔公式进行求解。提出了一种新的方法来解决伪布尔约束问题中的模型计数问题。首先,介绍了知识编译和扩展规则的相关概念,随后详细阐述了如何利用知识编译将伪布尔约束问题转化为二元决策图(BDD),并着重探讨了BDD结构的特性,最后采用基于扩展规则的模型计数方法来处理伪布尔约束问题中的模型计数问题。实验结果表明,该方法在处理互补因子较高的子句集时表现出更为优越的性能。

关键词：伪布尔约束 SAT问题模型计数知识编译子句

来源：评论

学校读者我要写书评

暂无评论

知识编译下的伪布尔公式模型计数研究

知识编译下的伪布尔公式模型计数研究

引用

作者：郑苏豪桂林理工大学

学位级别：硕士

伪布尔(Pseudo-Boolean,PB)约束是一种用于描述离散决策问题的数学形式,通常用于在离散领域中建模和求解各种问题。伪布尔约束具有较高的表达能力和灵活性,能够有效地描述各种问题中的逻辑关系和约束条件。与传统的命题公式相比,伪布尔... 详细信息

伪布尔(Pseudo-Boolean,PB)约束是一种用于描述离散决策问题的数学形式,通常用于在离散领域中建模和求解各种问题。伪布尔约束具有较高的表达能力和灵活性,能够有效地描述各种问题中的逻辑关系和约束条件。与传统的命题公式相比,伪布尔约束表达能力更强,形式更简洁。由于其优秀的表达能力,伪布尔约束在实际应用中常用于描述各种离散决策问题,如电路设计自动化、自动规划和调度、人工智能和模式识别等。伪布尔公式的模型计数是伪布尔约束问题的一类扩展,对于部分伪布尔约束相关问题,仅是判断公式是否可满足是不够的,还需要求解出可满足赋值的个数。概率推理、一致性概率规划等问题都与伪布尔公式的模型计数问题相关联。虽然针对伪布尔约束的编码方法和技术在近年来得到了广泛的研究和应用,不断涌现出新的方法和算法为解决大规模和复杂的伪布尔约束问题提供了更加有效和高效的求解手段。但相比于布尔可满足性计数问题(#SAT),伪布尔公式的模型计数方法却没有得到深入研究,因此本文将从模型计数相关角度对伪布尔公式进行深入研究,提出了求解两类伪布尔约束模型计数相关问题的方法。 1.针对伪布尔公式的模型计数问题,提出了一种基于知识编译技术的求解方法。首先将伪布尔公式转换为二元决策图(Ordered Binary Decision Diagrams,OBDD),这一步骤利用知识编译技术将复杂的逻辑约束转化为更容易处理的形式。OBDD能够表示伪布尔公式,并且可以得到与其等价的子句集。接着利用扩展规则对子句集进行扩展,将其转化为极大项集合。最后根据解空间的性质得到子句集的可满足解个数,进而得到伪布尔公式的模型个数。 2.针对布尔变元在概率分布下的伪布尔公式的可满足概率计算,提出了一种基于知识编译技术和加权模型计数的求解方法。在通过OBDD得到与伪布尔公式等价的子句集后,利用知识编译技术将其编译为具有平滑性和确定性的可分解否定范式(Smooth Decision Diagrams in Decomposable Negation Normal Form,sdDNNF)。根据sd-DNNF的结构性质构造相应的算术回路,算术回路能够同时表示布尔变元之间的逻辑关系和变量的概率分布,保证逻辑推理过程的完整性和准确性。最后利用加权模型计数方法对算术回路计算得到概率分布下的伪布尔公式可满足概率。通过将所提出方法与现有算法在相应的测试集上进行对比实验,验证了其可行性和有效性,为研究伪布尔约束的模型计数相关问题提供了新思路。

关键词：伪布尔约束模型计数知识编译布尔可满足问题算术回路

来源：评论

学校读者我要写书评

暂无评论

基于机器学习的模型计数方法研究

基于机器学习的模型计数方法研究

引用

作者：张一凡吉林大学

学位级别：硕士

作为布尔可满足性问题的重要拓展,模型计数是从人工智能到形式化验证的一项重要推理任务,其在概率推理、神经网络验证、自动规划等领域有着广泛的应用。可满足性问题是对于一个给定的命题逻辑公式φ,判断是否存在满足该公式的赋值,而模... 详细信息

作为布尔可满足性问题的重要拓展,模型计数是从人工智能到形式化验证的一项重要推理任务,其在概率推理、神经网络验证、自动规划等领域有着广泛的应用。可满足性问题是对于一个给定的命题逻辑公式φ,判断是否存在满足该公式的赋值,而模型计数问题是计算满足公式φ的赋值的数量,计算复杂度是#P完全,故模型计数问题相较于可满足性问题更具有挑战性。随着学界对模型计数相关算法研究的不断深入以及模型计数应用需求的持续增长,再加之模型计数竞赛的推广,社区中已经出现了数十种模型计数求解器,这些求解器使用的求解算法主要分为三类:基于搜索、基于编译以及基于变量消除。基于搜索的模型计数方法通过更智能的枚举部分解去扩展DPLL框架;基于编译的技术依赖于高效的知识编译器,编译器将输入语言表示的公式编译为目标语言,编译完成后基于目标语言的表示高效地进行模型计数;基于变量消除的方法主要通过对变量进行一系列求和来执行模型计数。随着模型计数求解器的广泛应用,人们逐渐发现不存在单一求解器在大规模实例集的所有实例上表现都比其他求解器好,即没有单一的主导性求解器。相反,不同求解器在不同实例上表现各不相同,主要原因是不同实例有着不同的特征,而使用不同求解算法的求解器在具有不同特征的实例上会表现出较大差异。如果能根据实例的特征使用机器学习分类器为不同的实例选择不同的求解器,那么将有效地增加求解实例的数量并大幅度降低求解时间。基于这个问题,本文设计并实现了基于求解器选择的模型计数求解器SmartMC,其主要思想是计算实例的特征并使用机器学习分类器根据特征进行求解器选择。SmartMC使用的特征基于9类常用的表现命题逻辑公式特性的特征并在此基础上进行了特征选择,此外本文还加入了与模型计数任务相关的特征。本文还对神经网络求解器进行了研究与探索,提出并实现了基于信念传播的神经网络模型计数求解器BPMC,其能在极短的时间内给出实例的近似模型计数值,并且求解时间基本不受实例规模的影响。本文将SmartMC与神经网络求解器BPMC进行了结合,即当SmartMC无法求解实例时,使用神经网络求解器BPMC在极短时间内获得近似模型计数值,保证SmartMC对于任意实例一定能给出结果,进一步提升SmartMC的完备性。本文设计了两组实验,第一个组实验将神经网络求解器BPMC与目前先进的近似模型计数求解器Approx MC、信念传播神经网络BPNN进行对比,实验结果表明BPMC的准确度接近Approx MC,优于BPNN,但是在求解时间上,BPMC花费的求解时间远少于Approx MC,并且BPMC求解时间几乎不受实例规模的影响。第二组实验将关闭了神经网络求解器BPMC的SmartMC与目前先进的模型计数求解器sharp SAT-TD、Exact MC、Ganak、DPMC进行对比,实验结果表明,在求解实例的数量以及平均求解时间上,SmartMC的表现都优于目前先进的模型计数求解器。

关键词：模型计数机器学习求解器选择神经网络求解器

来源：评论

学校读者我要写书评

暂无评论

模型计数问题中子句简化方法研究

模型计数问题中子句简化方法研究

引用

作者：韩淑婷吉林大学

学位级别：硕士

模型计数(model counting,#SAT)问题是人工智能领域的一个基本问题,旨在求解给定命题公式的可满足赋值个数,求解难度是#P完全的。现代基于CDCL(conflict driven clause learning)框架的模型计数求解器已经能够处理具有百万条子句的大型... 详细信息

模型计数(model counting,#SAT)问题是人工智能领域的一个基本问题,旨在求解给定命题公式的可满足赋值个数,求解难度是#P完全的。现代基于CDCL(conflict driven clause learning)框架的模型计数求解器已经能够处理具有百万条子句的大型合取范式(conjunctive normal form,CNF)。然而,在诸如贝叶斯网络、规划、有界模型检测、概率推理等复杂实际应用中,仍有许多庞大的CNF公式使用目前最先进模型计数求解器也难以求解。对于大规模问题而言,简化CNF公式中的子句,是提升模型计数求解效率的有效方法。模型计数的预处理阶段能够通过使用命题公式推理规则删除冗余子句和变量,实现对命题公式中子句的简化。包含消除(subsumption elimination,SE)、重言式消除(tautology elimination,TE)、活化(vivification,VIV)、B+E算法等多种先进的预处理技术能够大大减少了命题公式的子句数。然而子句简化后的命题公式并非总能在模型计数时表现得更好,存在部分反常公式经预处理后模型计数总时间反而明显增加。本文提出衡量预处理前后命题公式模型计数求解难度的标准,通过判断预处理后命题公式是否更难求解实现对反常公式的过滤。本文提出预处理筛选算法FILTER,通过调用PMC和B+E两种成熟的预处理器,对比原公式以及两种预处理后公式的求解难度,筛选出求解难度最低的公式进行模型计数。在最新的精确模型计数求解器Exact MC上测试算法FILTER,实验结果表明本文提出的预处理筛选策略综合了PMC和B+E的好处,从整体上提高了模型计数求解效率。在许多大规模实际问题中,多值变量的出现十分常见。多值变量在命题逻辑知识库中表示为exactly-one约束,在使用模型计数解决包含多指变量的实际问题时,通常需要将exactly-one约束转换为CNF公式,这将以指数形式扩大CNF公式的子句规模,容易造成模型计数求解时间溢出的问题。为更好地解决这类问题,本文提出了从CNF公式中识别exactly-one约束的算法ECR。C2D是目前唯一能够直接处理exactly-one约束的求解器,实验结果显示算法ECR显著提升了C2D的求解效率。对于其他不能直接处理exactly-one约束的模型计数求解器,本文提出对exactly-one约束进行单独处理的算法ECP。将算法ECR和算法ECP应用于模型计数求解器Exact MC,改进得到的模型计数求解器ECMC性能优于Exact MC。综上,本文的主要研究内容是通过简化命题公式的子句,提升模型计数求解效率。在对模型计数问题中命题公式的子句进行简化时,本文采用了两种策略:一是在预处理阶段过滤反常公式的预处理筛选策略,二是在求解阶段识别和单独处理命题公式中exactly-one约束的策略。在Exact MC和C2D两种模型计数求解器上测试的实验结果表明,本文提出的两种策略都实现了命题公式的简化和模型计数求解效率的提升。

关键词：模型计数预处理 exactly-one约束 ExactMC C2D 可满足性问题

来源：评论

学校读者我要写书评

暂无评论

基于格局检测的并行模型计数方法

引用

吉林大学学报（工学版） 2020年第4期50卷 1443-1448页

作者：李壮刘磊张桐搏吕帅吉林大学计算机科学与技术学院长春130012

在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基... 详细信息

在经典的可满足性问题求解中,针对处理模型数较少的实例,SWcc迭代法和SWcc优化增量法与完备的模型计数方法相比,求解适用性更高,但SWcc迭代法和SWcc优化增量法均为串行求解方法,没有对解空间进行剪枝、化简等处理。本文基于此设计了基于格局检测的并行模型计数算法。该算法以化简解空间和启发式为核心,将原解空间分解成为若干子空间并对原子句集进行化简后,并行处理各个子空间。实验结果表明:对于模型个数较少、公式规模较大的问题,该算法比原算法更具有适用性。

关键词：自动推理局部搜索模型计数格局检测并行框架

来源：评论

学校读者我要写书评

暂无评论

基于格局检测的模型计数方法

引用

软件学报 2020年第2期31卷 395-405页

作者：贺甫霖刘磊吕帅牛当当王强吉林大学计算机科学与技术学院吉林长春130012 符号计算与知识工程教育部重点实验室(吉林大学) 吉林长春130012 西北农林科技大学信息工程学院陕西杨凌712100

模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,很多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharp SAT,它们均采用完备方法且具有高效的求解能... 详细信息

模型计数是指求出给定命题公式的模型数,是SAT问题的泛化.模型计数在人工智能领域取得了广泛应用,很多现实问题都可以规约为模型计数进行求解.目前,常用的模型计数求解器主要有Cachet与sharp SAT,它们均采用完备方法且具有高效的求解能力,但其求解效率对模型数不敏感.有理由猜测:当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数.局部搜索是求解SAT问题的高效不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中,提出了SWcc算法,具有很高的求解效率.对SWcc算法进行扩充,分别得到了迭代法与优化后的增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现.最后给出了大量测试样例的实验结果,以验证当给定合取范式的模型较少时,该迭代法与优化后的增量法的求解效率有所提升.

关键词：模型计数局部搜索格局检测

来源：评论

学校读者我要写书评

暂无评论

基于局部搜索的模型计数方法研究

基于局部搜索的模型计数方法研究

引用

作者：贺甫霖吉林大学

学位级别：硕士

模型计数问题是指求解出给定命题公式的模型数,是自动推理领域的重要难题。模型计数在人工智能领域取得了广泛应用,许多现实问题都可以规约为模型计数问题进行求解。目前常用的完备的模型计数求解器具有高效的求解能力,但其求解效率对... 详细信息

模型计数问题是指求解出给定命题公式的模型数,是自动推理领域的重要难题。模型计数在人工智能领域取得了广泛应用,许多现实问题都可以规约为模型计数问题进行求解。目前常用的完备的模型计数求解器具有高效的求解能力,但其求解效率对模型数不敏感。有理由猜测:当给定问题的模型较少时,不完备算法可能发挥其效率优势而更适合模型计数。本文旨在利用不完备方法的求解优势,设计出新的求解能力更强的模型计数求解方法。其中求解能力以正确求出给定合取范式模型的求解时间长短来衡量。局部搜索是求解SAT问题的高效的不完备方法,Cai等人提出了格局检测策略,并将其应用到局部搜索方法中提出了SWcc算法。格局检测策略定义了邻居变量,很好地解决了变量翻转过程中容易遇到的局部最优问题,具有很高的求解效率。本文对SWcc算法进行扩充分别得到了迭代法与增量法两种效率较高的不完备模型计数方法,给出了两种方法的思路和具体实现。SWcc算法每完成一次局部搜索的迭代计算过程,便可以得到一个可满足的全值指派。迭代法采用添加子句的方法,将刚刚得到的可满足指派的否定形式添加到原合取范式,解决了解的重复性问题,使得算法在每次迭代过程中都可以得到一个不同的可满足指派,并记录下可满足指派数目。增量法同样采用添加子句的方法,与迭代法不同的是,增量法在每次迭代结束后会计算相关变量的邻居信息,下一次翻转操作仍在当前指派上进行,从而减少了许多变量的初始化计算过程。为了进一步提升不完备算法的求解能力,本文提出了两种启发式策略,并将他们分别应用于迭代法与增量法。在迭代法的基础上添加了加速求解策略,给出了该策略的详细描述,理论上该算法适用于求解模型数目较多的合取范式,并且当求解可满足指派中有部分文字正负形式相同的合取范式时,求解效率会进一步提升。在增量法的基础上添加了解的优化策略,尽可能减少添加子句的变量数目,从而发挥了格局检测的优越性。最后,给出了大量测试样例的实验结果,实验结果表明,当给定合取范式的模型较少时,本文提出的迭代法与增量法的求解效率有所提升。本文提出的两种启发式策略在求解部分特定实例时,也会得到较好的求解效果。

关键词：模型计数局部搜索格局检测启发式策略自动推理

来源：评论

学校读者我要写书评

暂无评论

基于扩展规则的模型计数方法研究

基于扩展规则的模型计数方法研究

引用

作者：贾凤雨吉林大学

学位级别：硕士

早在二十世纪五十年代,智能规划一经提出便成为了人工智能领域中的一个前沿研究领域,自此,随着国内外诸多研究学者们不懈努力,在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法,其中一种较为高效的求解方法... 详细信息

早在二十世纪五十年代,智能规划一经提出便成为了人工智能领域中的一个前沿研究领域,自此,随着国内外诸多研究学者们不懈努力,在该领域的研究成果方面取得了突破性的进展。目前求解该问题存在着许多种方法,其中一种较为高效的求解方法则是将规划问题编译为命题可满足性问题(SAT问题),然后利用SAT求解器进行求解。有时此种间接求解的方法会比直接求解的方法更为高效快捷,目前已成为求解智能规划问题的主流方法之一。在1971年,Cook等人证明SAT问题是NP完全的。事实上,许多NP问题都可以转为SAT问题进行求解。然而,在人工智能研究领域还有许多经典问题的计算复杂度是高于NP的,对于这些问题的求解仅仅判断给定命题公式是否可满足是不够的,还需要知道问题模型的个数。由此扩展出了模型计数问题(#SAT问题)。如贝叶斯网络推理,概率规划问题等都可以转化成#SAT问题进行求解。因此,如何高效地求解#SAT问题,对人工智能的很多领域都有重要意义。目前,求解#SAT问题的算法可以分为精确求解和近似求解两种。精确算法可以保证计算出给定命题公式的准确模型个数;而近似算法只能计算出给定公式模型的近似个数。在精确求解的算法中主要有基于DPLL(Davis Putnam Logemann and Loveland)的方法和基于扩展规则的方法。这两种方法是互补的求解方法。一般情况下,当互补因子较高时,基于扩展规则的求解方法要优于基于DPLL求解方法;反之,当互补因子较低时,要差于基于DPLL求解方法。本文在对基于扩展规则的模型计数求解方法CER深入研究的基础上,从不同角度对其进行改进,提出了两种更为高效的求解方法:(1)结合扩展规则重构的#SAT问题增量求解方法:对CER中的重要计算公式进行重构,并证明了重构的正确性;给出了极大项相交集和扩展极大项相交集的定义,并提出结合两者关系复用极大项相交集求解结果的增量计算方法,还删减了所有广义互补子句集对应的扩展极大项相交集,有效避免了许多冗余计算;给出用互补表记录子句间互补关系的方法,提出一种对极大项相交集的基础子句集进行增量判定互补的方法,很好地避免了在判定子句间及基础子句集互补性时的大量冗余计算。实验结果表明:与CER方法相比,RCER方法效率更高,尤其是互补因子较低的情况下。(2)结合互补度的基于扩展规则#SAT问题求解方法:在计算给定子句集的模型个数时,利用SE-Tree(set enumeration tree)形式化地表达计算过程,逐步生成需要计算的子句集合。并在SE-Tree中添加终止结点,避免大部分含互补文字子句集合的生成,且不会因剪枝而导致求解不完备。提出互补度的概念,在扩展SE-Tree结点时按照互补度由大到小的顺序扩展,较早地生成含互补文字且长度较小的子句集合,有效减少枚举树生成的结点个数,进而减少对子句集合判断是否含互补文字的计算次数。实验结果表明,与CER方法相比该方法效率较好,且进一步改进了CER方法在互补因子较低时求解效率低下的不足。以上两种方法从不同角度对CER方法进行了改进,并取得了较好的效果。两种方法分别利用了CER方法中重要公式的计算项间的关系和计算顺序减少了求解过程中的冗余计算,从而达到提高效率的目的。

关键词：智能规划命题可满足性问题模型计数扩展规则增量方法

来源：评论

学校读者我要写书评

暂无评论

工作流可满足性的约简增量模式回溯法

引用

计算机集成制造系统 2023年第11期29卷 3624-3638页

作者：翟治年刘关俊卢亚辉向坚吴茗蔚丰明坤浙江科技学院信息与电子工程学院浙江杭州310023 同济大学计算机科学系上海201804 深圳大学计算机与软件学院广东深圳518060

在大量云/服务化资源造成的性能压力下,增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径,但对“欠约束”实例,其模式枚举性能显著下降,不利于大量可行解的优化选择。针对该问题提... 详细信息

在大量云/服务化资源造成的性能压力下,增量模式回溯法(Incremental Pattern Backtracking, IPB)及其k指派技术是工作流可满足性求解的首选途径,但对“欠约束”实例,其模式枚举性能显著下降,不利于大量可行解的优化选择。针对该问题提出新颖的简指派图概念,证明其可取代k指派图用于模式授权匹配验证,且尽管其块邻域大小耦合了图的整体信息,但仍可以增量方式计算。进而,分析了增量化简指派的实施条件和效果,及其主要影响因素。由此建立了约简增量模式回溯法(Reduced Incremental Pattern Backtracking, RIPB)。在资源配比为2~100的两个仿真实例集上测试,实验结果表明:在其基本子集上,RIPB较IPB有0.96~1.24倍时间性能优势;当资源比例升高或约束密度降低时,RIPB的优势有不同程度扩大;特别地,对资源配比为10而授权比例在1/2左右的两个子集,RIPB的平均优势分别可达1.29和1.61倍。

关键词：可满足性工作流授权约束资源分配模型计数模式

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：