Simulation Analysis on Influence of Congestion Propagation on Operation of Carsharing Systems
-
摘要:
随着共享汽车渗透率的不断增加，站点、路段层面的车辆溢出和拥挤传播现象日趋严重. 为刻画拥挤传播对汽车共享系统运行的影响机理，首先，搭建具有时变性和状态相关性的汽车共享系统排队网络；其次，基于C# 语言和O2DES离散事件仿真框架，提出并设计考虑车路交互影响和拥挤传播现象的汽车共享系统仿真模型，分析动态随机环境下站点与路段层面的拥挤传播现象对汽车共享系统运行的影响；最后，以成都市三站点的小规模汽车共享系统为例，在不同转运比例、需求和道路拥堵场景下，将该模型与引入虚拟空间的无穷排队模型进行对比分析. 研究结果表明：站点和路段层面的拥挤传播现象会导致系统服务率下降9.3%～16.9%，相比无穷排队模型，考虑拥挤传播现象的排队模型更能反映汽车共享系统的实际运营过程；当路网的道路占用率为70% （路网处于中度拥堵）时，考虑拥挤传播现象的汽车共享系统可实现最大收益；汽车共享系统的引入会为道路资源的动态分配带来新变化，当公共交通转向汽车共享系统的用户占比超过70%时，路网拥堵加剧，不利于汽车共享系统的有效运营和可持续发展.
Abstract:With the increasing penetration of carsharing, vehicle overflow and congestion propagation at the level of station and path tend to be serious. In order to describe the influence mechanism of congestion propagation on the operation of carsharing systems, firstly, a queuing network of the carsharing system is built with time-varying and state-dependence properties. Secondly, based on C# language and O2DES framework of discrete event simulation, a simulation model of the carsharing system under dynamic stochastic environment is proposed, which allows for the influence of vehicle–road interaction and congestion propagation. The influence of congestion propagation on the operation of the carsharing system is analyzed in terms of the station and path levels. Finally, a small-scale carsharing system, i.e., three stations in Chengdu, is exemplified. The proposed model and the infinite queuing model in virtual space are compared and analyzed under different transfer ratios, demands and road congestion scenarios. The results show that congestion propagation at the stations and paths will decline the system service rate by 9.3%–16.9%. Compared with the infinite queuing model, the proposed model can better reflect the actual operation of the carsharing system because of considering congestion propagation. When the occupancy rate of the road network reaches 70% (the road network is in moderate congestion), the proposed carsharing system can achieve maximum benefits. The introduction of the carsharing system will bring new changes to the dynamic allocation of road resources. When the proportion of users from public transportation to the carsharing system exceeds 70%, it will intensify the congestion of the road network, which is not conducive to the effective operation and sustainable development of the carsharing system.
-
自动定理证明是人工智能的核心部分之一，致力于生成高效的计算机程序，从而使计算机能够完全或几乎完全自动地进行推理. 即，将形式化为一阶逻辑公式的前提和结论作为计算机程序的输入，并试图利用程序自动从前提中推导出结论. 这样的程序通常被称为自动定理证明器（automated theorem prover，ATP）.
随着形式化技术的发展，ATP的应用范围从理论上的数学定理逐渐拓展到知识编译[1]、软（硬）件模型检验[2-5]、管理规划[6-7]、集成电路设计[8-10]及软件测试[11]等实际问题上. 因此，旨在推理小规模数学问题的ATP越来越多面对从一些大型知识库（CYC[12]、SUMO[13]以及Mizar[14]等）和实际应用中转换而成的大规模的问题. 这些大规模问题通常被称为大理论（large theory），通常包含成千上万个前提，但是仅有非常少的一部分前提才对问题结论的证明有用. 大规模的冗余前提集会使得ATP在证明问题时搜索空间呈指数型增长，甚至可能立即超出计算机的运行能力，这大大地限制ATP自动推理能力. 假设可以直接使用在证明中出现的前提，ATP则能够轻松快速地证明问题的结论. 因此，从问题中去除不必要的前提，可以减少搜索空间，并降低搜索难度. 在ATP开始证明之前选择出对问题结论证明有用的前提的过程被称为前提选择（premise selection）. 前提选择是ATP预处理中非常关键的一环，对解决大理论的自动推理至关重要.
早期的前提选择方法[15-16]通过不断对当前选择的前提和结论否定的模型进行语义分析来指导前提的选择. 然而，基于语义的前提选择方法非常耗时，且严重依赖模型检查器的能力. 随后，一些基于符号相关性的前提选择方法[17-19]不断被提出. 此类方法主要通过计算和比较出现在公式（前提和结论）符号中，分析公式间的相关性. 当前，一些机器学习[20-22]和深度学习[23-27]技术也开始应用在前提选择中. 基于学习的前提选择方法强烈地依赖于大规模成功证明的领域经验，需要从形式化证明构造不同领域（如集合论、代数以及管理等）问题的语料库. 然而，在形式化时不同领域问题使用的符号是随机制定的，使得对应的语料库无法在学习训练中跨领域通用. 因此，当ATP面临一个新领域中的大规模问题时，由于缺乏新领域中的形式化证明，将导致当此类学习方法在前提选择任务中失效.
因此，从效率和可行性出发，当前ATP主要使用基于符号相关性的方法作为主要前提选择方法. 然而，当前方法终止前提选择过程的条件是，无法再选择任何的前提作为相关前提. 在此情况下，现有方法缺少在选择过程中对所选择前提的充分性进行判断，因此，可能在已经充分选择了相关前提的情况下，仍不会停止选择过程. 这直接导致当前选择过程将大量与结论证明无关的前提标记为相关的. 此外，当前的方法在选择前提时仍需人工设置相关度边界，这导致相关度边界值不具有普遍性和广泛适用性.
针对以上问题，本文提出了一种新的基于符号权重的一阶逻辑前提选择方法SymbolWeight. 新方法通过考虑问题中符号出现的频率，为每个符号赋予不同的权重. 在新的权重定义下，若符号是通用符号（高频符号），其权重就越小；若符号是稀有符号（低频符号），其权重就越大. 新定义符号的权重能够削弱通用符号造成的负面影响，以及体现稀有符号的重要性，从而保证基于新权重的相关度计算更加稳定. 同时，为减少手工参数的数量，提高前提选择的精确度，新方法提出一种自适应相关度边界，用于判断前提是否与结论相关. 此外，为了在充分选择相关前提的情况下及时停止前提选择过程，新方法交互结合了前提选择过程和结论自动推理过程. 实验结果表明，和自动定理证明器中广泛使用的通用前提选择方法相比，新方法能够帮助自动定理证明器E在MPTP2078基准测试集上提高10%以上的证明率.
1. 预备工作
在一阶逻辑[28]中，给定一个变元符号集
$ \mathcal{V} $ 、一个函数符号集$\mathcal{{{F}}}$ 、一个谓词集$ \mathcal{P} $ . 一阶逻辑项是一个变量项$v\;（v\in \mathcal{V} ）$ 或者形如$f\left({t}_{\mathrm{u}1},{t}_{\mathrm{u}2},\cdots ,{t}_{\mathrm{u}{{g}}}\right)$ 的函数项. 其中：$ f({\text{•}})\in \mathcal{F} $ ，是$ g $ （$ g\geqslant 0 $ ）元函数符；$ {t}_{\mathrm{u}1} $ ,$ {t}_{\mathrm{u}2} $ ,…,${t}_{\mathrm{u}{{g}}}$ 是项. 一阶逻辑原子（atom）形如${p}_{\mathrm{r}\mathrm{e}\mathrm{d}}\left({t}_{\mathrm{r}1},{t}_{\mathrm{r}2},\cdots ,{t}_{\mathrm{r}{{o}}}\right)$ ，其中：$ {p}_{\mathrm{r}\mathrm{e}\mathrm{d}}({\text{•}})\in \mathcal{P} $ ，是$ o $ （$ o\geqslant 0 $ ）元谓词符；$ {t}_{\mathrm{r}1} $ ，$ {t}_{\mathrm{r}2} $ ，…，$ {t}_{\mathrm{r}{\rm{o}}} $ 是项. 一阶逻辑公式是由一阶逻辑联结词$\mathcal{C}= \{ ～ ,\wedge ,\vee ,\to , \leftrightarrow \}$ 、量词$ {Q}=\{\forall ,\exists \} $ 和原子联结而成. 其中：$～$ 表示否定；$ \wedge $ 表示且；$ \vee $ 表示或；$ \to $ 表示蕴含；$\leftrightarrow$ 表示等价；$ \forall $ 表示全称量词；$ \exists $ 表示存在量词.在自动定理证明中，问题的前提和结论均被形式化为一阶逻辑公式. 因此，符号是前提和结论最直观的特征. 若要为大理论问题的结论选择最相关的前提，最自然的方法是使用基于符号的前提选择方法.
2. 前提选择方法
基于符号相关性的前提选择方法意味着需要根据出现在前提中符号计算前提与当前结论证明的相关性，并据对应的相关度对前提进行选择.
2.1 基本思想
令c和P分别为一个大理论问题中的结论和前提集，基于符号相关性的前提选择方法的基本框架为：
1） 若符号s出现在c中，则s与c是1度相关的；
2） 若前提
$ p\in P $ 中的符号（或符号集）与c是k度相关的，则p是$ k + 1 $ 度相关的；3） 若p与c是k度相关的，则p中的所有符号与c是k度相关的.
在此过程中，首先需要定义两个相关集，即相关前提集
$ {R}_{\mathrm{p}} $ 和相关符号集$ {R}_{\mathrm{s}} $ .$ {R}_{\mathrm{p}} $ 包含结论及与结论证明相关的前提.$ {R}_{\mathrm{s}} $ 包含$ {R}_{\mathrm{p}} $ 中所有公式的所有符号，即Rs=⋃func∈RpF(func), (1) 式中：
$ {f}_{\mathrm{u}\mathrm{n}\mathrm{c}} $ 为结论c或与结论证明相关的任意前提p；$ F\left({f}_{\mathrm{u}\mathrm{n}\mathrm{c}}\right) $ 为$ {f}_{\mathrm{u}\mathrm{n}\mathrm{c}} $ 中所有符号组成的集合.开始时，
$ {R}_{\mathrm{p}} $ 仅包含结论c，$ {R}_{\mathrm{s}} $ 仅包含c中所有的符号. 即初始时，$ {R}_{\mathrm{p}}=\left\{c\right\} $ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ . 前提选择方法基于每个前提p的符号集$ F\left(p\right) $ 和当前$ {R}_{\mathrm{s}} $ , 计算p与c的相关度，不断地选择新的p加入$ {R}_{\mathrm{p}} $ 中，同时更新$ {R}_{\mathrm{s}} $ ，直到无法再将任何前提加入$ {R}_{\mathrm{p}} $ 中. 在完成前提选择后，由相关前提集$ {R}_{\mathrm{p}} $ 中的所有前提和结论组成的缩减问题将作为自动定理证明器新的输入，用于自动地证明问题的结论. 现有基于符号相关性的前提选择方法的通用流程如算法1所示.算法1 现有的基于符号相关性的前提选择方法
输入：结论c、前提P、相关前提集
$ {R}_{\mathrm{p}} $ 、相关符号集
$ {R}_{\mathrm{s}} $ 、无关前提集$ {I}_{\mathrm{p}} $ 、选择前提集SP、相关度阈值h、循环标记
$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}} $ 输出：
$ {R}_{\mathrm{p}} $ ${R}_{\mathrm{p}}=c$ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ ，$ {I}_{\mathrm{p}}=P $ ，$ {S}_{\mathrm{p}}=\varnothing $ ，${F}_{\mathrm{l}\mathrm{a}\mathrm{g}}=\mathrm{T}\mathrm{r}\mathrm{u}\mathrm{e}$ while
$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}} $ dofor
$ p\in {I}_{\mathrm{p}} $ do根据当前的
$ {R}_{\mathrm{s}} $ ，计算$ p $ 的相关度if
$ p $ 的相关度$ \geqslant h $ then$ {S}_{\mathrm{p}}:={S}_{\mathrm{p}}\cup \left\{p\right\} $ end if
end for
if
$ {S}_{\mathrm{p}}=\varnothing $ then$ {F}_{\mathrm{l}\mathrm{a}\mathrm{g}}=\mathrm{F}\mathrm{a}\mathrm{l}\mathrm{s}\mathrm{e} $ else
${R}_{\mathrm{p}}:={R}_{\mathrm{p}}\cup {S}_{\mathrm{p}}$ ，${R}_{\mathrm{s}}:=({\bigcup }_{p\in {S}_{\mathrm{p}}}F(p))\cup {R}_{\mathrm{s}}$ ，${I}_{\mathrm{p}}:={I}_{\mathrm{p}}|{S}_{\mathrm{p}}$ $ {S}_{\mathrm{p}}=\varnothing $ end if
end while
完整的前提选择方法必须包含两个部分：前提选择和结论证明. 给定一个大理论，前提选择方法首先需要对大理论中的前提进行选择，随后利用自动定理证明器在选定的前提集上对问题的结论进行自动推理. 现有基于符号相关性的前提选择方法均将这两个部分分离开来，即，必须在结束前提选择过程之后，再利用自动定理证明器证明缩减后的问题. 尽管通过调整和添加实验参数对选择前提的数量进行限制，现有方法最后选择的前提仍有大量是与结论证明无关的.
2.2 基于符号权重的前提选择方法
由算法1可知，如何计算前提和相关符号集相关度是基于符号相关性的前提选择方法的重点. 简单地，可通过前提中的符号是否出现在相关符号集中，从而确定前提的相关性. 如果前提至少包含相关符号集中的一个符号，则可认为该前提是相关的. 在此情况下，若前提包含相关符号集中的一个符号，则该前提中的所有符号都会变为相关符号（加入相关符号集中）. 这种做法的弊端在于，几次迭代后，问题中几乎所有的前提都将被选择加入相关前提集中. 其中，最主要的原因是大理论问题中某些符号（通常被称为通用符号）频繁地出现在不同的前提中. 若通用符号被标记为相关符号，则所有包含此类符号的前提都将被认为是与结论证明相关的. 因此，前提的选择方法的重心应该放在解决通用符号的问题上.
与通过符号对应的是稀有符号，即在问题中出现的频率较低，基于此类符号的选择方法能够避免选择过多的前提. 因此，符号的权重定义应该遵循两个原则：削弱通用符号造成的负面影响，以及体现稀有符号的重要性. 给定一个前提集
$ P $ ，任意符号$s\in \bigcup\limits_{p \in P}F\left(p\right)$ 的权重$ w\left(s\right) $ 定义为w(s)=1−occ(s)|P|+1， (2) 式中：
$ {o}_{\mathrm{c}\mathrm{c}}\left(s\right) $ 为包含符号s的所有前提数量；$ \left|P\right| $ 为P中的前提总数.显而易见，对任意符号
$ s $ ，$ 0 < w\left(s\right) < 1 $ .$ w\left(s\right) $ 满足符号权重定义的两个原则. 若符号s是通用符号，则s的权重就越小；若符号s是稀有符号，则s的权重就越大. 式（2）定义的符号权重均在区间$ \left(\mathrm{0,1}\right) $ ，这能够保证基于该符号权重的相关度更加稳定.给定相关符号集
$ {R}_{\mathrm{s}} $ ，前提$ p $ 在$ {R}_{\mathrm{s}} $ 下与结论证明的相关度为r(p)=∑si∈Rs∩F(p)w(si)∑sj∈F(p)w(sj), (3) 式中：
$ {s}_{\mathrm{i}} $ 为$ {R}_{\mathrm{s}} $ 与$ F\left(p\right) $ 的交集中的任意符号；$ {s}_{\mathrm{j}} $ 为$ F\left(p\right) $ 中的任意符号.前提p与结论证明的相关度
$ r\left(p\right) $ 是在区间$ \left[\mathrm{0,1}\right] $ 内的实数. 如果p中的符号均不在相关符号集$ {R}_{\mathrm{s}} $ 中，则p与结论证明的相关度为0. 这说明p与当前的相关前提集$ {R}_{\mathrm{p}} $ 毫无符号上的关联. 如果p中的符号均在$ {R}_{\mathrm{s}} $ 中，则p与结论证明的相关度为1. 这说明p与当前的相关前提集$ {R}_{\mathrm{p}} $ 在符号上非常相关. 值得注意的是，随着相关前提集$ {R}_{\mathrm{p}} $ 和相关符号集$ {R}_{\mathrm{s}} $ 的变化，前提p的相关度也会发生变化.由式（3）可知，每个前提都存在一个基于当前相关符号集的相关度. 给定任意两个前提，通过比较其与结论证明的相关度大小，可以形式化两个前提间“更相关”的关系. 根据相关度的高低能够将对应的前提进行排序，但不能直接形式化“最相关前提”这一概念. 最相关前提的相关度大于最不相关前提的相关度, 因此，最直观的做法是设定一个相关度边界，用于区分最相关前提和最不相关前提.
定义1 给定一个相关度边界h（
$0\leqslant h\leqslant 1$ ），前提p被标记为最相关前提, 当且仅当$r\left(p\right)\leqslant h$ .由定义1可知，如果将h设置为0，所有的前提均为最相关前提. 如果将h设置为1，仅有非常少（甚至为0）的前提被标记为最相关的. 显然，相关度边界值过大或过小都会直接影响选择的结果，甚至问题结论的证明. 通过人工设置的相关度边界不具有普遍性和广泛适用性.
为解决以上问题，本文提出了一种自适应相关度边界. 该边界仅由当前选择过程中前提的相关度而决定，从而不再需要提前进行人工设置.
假定问题中包含n个前提
$ {p}_{1} $ ,$ {p}_{2} $ ,…,${p}_{{{{{n}}}}}$ ，$n \in {{{\bf{N}}}}, n \geqslant 1$ ，其对应的相关度分别为$ r\left({p}_{1}\right) $ ,$ r\left({p}_{2}\right) $ ,…,$ r\left({p}_{{n}}\right) $ . 在n个相关度中，部分相关度的值相同. 因此，合并相同的相关度值，能够从$ r\left({p}_{1}\right) $ ,$ r\left({p}_{2}\right) $ ,…,$ r\left({p}_{{n}}\right) $ 中获取M个不同的数值,$M \in {\bf{N}},1 \leqslant M \leqslant n$ . 这里将M个数值从高到低进行排序，序号为m的数值即为第m级自适应相关度边界$ {h}_{m} $ ，$m \in {\bf{N}},1 \leqslant m \leqslant M$ .显然，自适应相关度边界因问题而异，且会随着选择过程的变化而变化. 在选择过程中，所有相关度小于
$ {h}_{m} $ 的前提均不会被选择.前提选择方法的主旨在于选择尽可能少但充分与问题结论证明相关的前提. 一种可能的方法是选择一级自适应相关度边界
$ {h}_{1} $ 作为选择前提的条件. 实验发现，在大部分情况下，$ {h}_{1}=1 $ . 由式（3）可知，若一个前提的相关度为1，则该前提的所有符号均在相关符号集中. 若在相关前提集中加入相关度为1的前提，并不会使对应的相关符号集$ {R}_{s} $ 发生任何变化（加入新的符号）. 因此，仅选择相关度为1的前提作为最相关前提，会导致选择的前提不够充分. 因此，本文进一步细化地定义了自适应相关度边界$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ .定义2 给定一个前提集和前提对应的相关度，
1） 若第1级自适应相关度边界
$ {h}_{1}=1 $ ，则自适应相关度边界为第2级自适应相关度边界，即$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}={h}_{2} $ ；2） 此外，自适应相关度边界为第1级自适应相关度边界，即
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}={h}_{1} $ .由定义2可知，利用自适应相关度边界
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ ，新提出的基于符号权重的前提选择方法不再依赖任何人工设置的相关度边界.给定一个前提集
$ P $ ，现在可以根据前提$ p\in P $ 的相关度和自适应相关度边界，从$ P $ 中选择最相关前提. 然而，当前仍无法直观地判断所选择的前提对问题的结论证明是否足够充分. 因此，本文将前提选择过程和ATP的证明过程进行交互地结合. 在新的框架下，每一次选择的结果均将作为ATP的输入，开始尝试证明问题的结论. 若结论能够被自动地证明，则说明当前选择的前提是充分的，且整个过程可以停止.新提出的基于符号权重的前提选择算法流程如算法2所示. 最初的相关前提集仅包含问题的结论，对应的相关符号集仅包含结论中的符号，且无关前提集为问题的整个前提集. 在每次选择结束后，当前相关前提集中的前提和结论组成了新的缩减问题，ATP开始尝试在给定的CPU （central processing unit）运行时间内对该缩减问题进行证明. 若ATP能够证明该问题的结论，则不需要再继续选择前提，整个选择和证明过程立即停止. 否则，开始基于当前的相关符号集计算前提的相关度，并依据相关度边界, 将符合条件的前提标记为选择前提. 在旋转过程中，若没有满足条件的前提，则整个过程立即停止；否则, 利用当前新选择的前提更新相关前提集和相对应的关符号集，并从无关前提集中移除新选择的前提. 因此，整个过程将在K次循环后停止，
$k \in {\bf{N}}, k \geqslant 1$ .算法2 基于符号权重的前提选择算法
输入： 结论c、前提P、相关前提集
$ {R}_{\mathrm{p}} $ 、相关符 号集$ {R}_{\mathrm{s}} $ 、无关前提集IP、选择前提集SP、 相关度集R、自动定理证明器${{A}}_{\mathrm{T}\mathrm{P}}$ 、迭代 次数K、 CPU运行时间T输出：
$ {R}_{\mathrm{p}} $ $ {R}_{\mathrm{p}}=c $ ，$ {R}_{\mathrm{s}}=F\left(c\right) $ ，$ {I}_{\mathrm{p}}=P $ ，$ {S}_{\mathrm{p}}=\varnothing，R=\varnothing $ for
$ k\in [\mathrm{1,2},\dots ,K] $ do利用
$ {{A}}_{\mathrm{T}\mathrm{P}} $ 尝试在时间T内证明由$ {R}_{\mathrm{p}} $ 中的前提（和结论）组成的缩减问题
if 问题被
${{A}}_{\mathrm{T}\mathrm{P}}$ 证明 then停止
else
for
$ p\in {I}_{\mathrm{p}} $ do根据当前的
$ {R}_{\mathrm{s}} $ ，计算$ p $ 的相关度$ r\left(p\right) $ $ R:=R\cup \left\{r\left(p\right)\right\} $ end for
根据R决定自适应相关度
$ {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}} $ for
$ p\in {I}_{\mathrm{p}} $ doif
$r\left(p\right)\geqslant {h}_{\mathrm{a}\mathrm{d}\mathrm{a}\mathrm{p}\mathrm{t}\mathrm{i}\mathrm{v}\mathrm{e}}$ then$ {S}_{\mathrm{p}}:={S}_{\mathrm{p}}\cup \left\{p\right\} $ end if
end for
if
$ {S}_{\mathrm{p}}=\varnothing $ then停止
else
$ {R}_{\mathrm{p}}:={R}_{\mathrm{p}}\cup {S}_{\mathrm{p}} $ ，${R}_{\mathrm{s}}:=(\bigcup\limits_{p \in {S_{\rm{p}}}} {F(p)} )\cup {R}_{\mathrm{s}}$ ，$ {I}_{\mathrm{p}}:={I}_{\mathrm{p}}|{S}_{\mathrm{p}} $ $ {S}_{\mathrm{p}}=\varnothing $ ，$ R=\varnothing $ end if
end if
end for
3. 实验和分析
本节使用MPTP2078问题库作为实验的基准测试集. MPTP2078问题库一共包含2078个问题，均来自Mizar问题库与Bolzano-Weierstrass定理相关的问题. 问题库中, 所有问题的前提和结论均被形式化为一阶逻辑公式，且公式按照其在Mizar数学库中出现的顺序线性排序. 即出现在每一个结论之前的公式（前提和其他结论）均可作为证明该结论的前提. 问题的前提数量在区间
$ \left[\mathrm{10,4\;563}\right] $ 内，且前提的平均数量为1876个. 有关问题库前提数量和符号的具体分析见表1.表 1 MPTP2078问题库描述Table 1. Description of MPTP2078 benchmark个 项目 公式 结论 最小前提 最大前提 平均前提 符号 数量 4564 2078 10 4563 1876 784 在本文的实验中，使用的操作系统为CentOS Linux 7.4.1708；CPU为octa-core Intel（R） Xeon（R） E5-2667 3.20 GHz；内存128 G. 使用自动定理证明器E作为实验默认ATP. 除证明结论的数量外，还使用选择精准度
${S} _{\mathrm{p}\mathrm{r}\mathrm{e}}$ （selected precision）和选择度${S} _{\mathrm{e}\mathrm{l}}$ （selectivity）[29]作为评估各种选择方法性能的指标, 如式（4）、（5）所示.${S} _{\mathrm{p}\mathrm{r}\mathrm{e}}$ 的值越高越好，而${S} _{\mathrm{e}\mathrm{l}}$ 的值越低越好.Spre=1|Proved|∑prob∈ProvedNUiP(prob)NSel(prob)， (4) Sel=1|Proved|∑prob∈ProvedNSel(prob)NAxP(prob)， (5) 式中：
$ {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ 为被证明的问题集；$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\in {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ ，是$ {P}_{\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{e}\mathrm{d}} $ 中的一个被证明的问题；$ {N}_{\mathrm{U}\mathrm{i}\mathrm{P}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right) $ 为出现在$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}} $ 证明中的有用前提的数量；${N}_{{\rm{S}}\mathrm{e}\mathrm{l}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right)$ 为选择的前提的数量；$ {N}_{\mathrm{A}\mathrm{x}\mathrm{P}}\left({p}_{\mathrm{r}\mathrm{o}\mathrm{b}}\right) $ 为$ {p}_{\mathrm{r}\mathrm{o}\mathrm{b}} $ 包含的原始前提的数量.表2列出了实验所涉及的基于符号的前提选择方法. 为了保证实验的公平性，本文将每个问题在自动定理证明器E上运行的CPU时间设定为60 s. 若一个问题的选择过程迭代K次，则每次迭代后生成的缩减问题仅在自动定理证明器E上运行
$ 60/K $ s. 显然地，需要权衡每次自动定理证明器运行的CPU时间和选择的迭代次数.表 2 参与实验的基于符号的前提选择方法的说明Table 2. Description of symbol-based premise selection methods in experiments提出的SymbolWeight能够根据前提的相当度自动地决定合适的相关度边界. 因此，SymbolWeight的性能仅与选择的迭代次数K有关. 表3评估了其在不同迭代次数K下对自动定理证明器E的性能影响. 由于每个问题运行CPU的时间最多为60 s，继续增加迭代次数会使得每次迭代中证明问题的CPU时间过小. 因此，SymbolWeight在实验中的最大迭代次数设置为30次. 随着K的不断增加，证明问题的数量在不断增加. 当
$ K= 30 $ 时，自动定理证明器E能够证明1077个问题. 值得注意的是，增加迭代次数并不会限制SymbolWeight的选择能力. 实验发现，SymbolWeight能够大大地减少选择前提的数量. 即使当K增加到30时，SymbolWeight平均选择前提数仅约为174个. 这表明，提出的自适应相关度边界在不损害自动定理证明器E证明能力的前提下，能够有效解决相关度边界的阈值设定问题. 随着K的增加，自动定理证明器CPU时间在逐渐减少（${{K}}=30$ 时，CPU时间仅为2 s）. 然而，证明问题的数量在不断增加. 这说明如果能够正确地选择出证明大理论问题结论所需要的全部前提，自动定理证明器E能够轻易地搜索到结论的证明. 因此，有效的前提选择方法能够大大地帮助证明器提高证明问题的能力.表 3 自动定理证明器E在SymbolWeight下的证明性能Table 3. Performance of automated theorem prover E with SymbolWeight$ K $ 证明数
量/个平均选择前提数量/个 选择精
确度选择度 2 288 13.0 0.358 0.054 4 599 22.6 0.336 0.060 6 818 33.3 0.322 0.054 8 862 44.5 0.309 0.053 10 920 55.9 0.302 0.055 12 932 68.4 0.295 0.057 14 967 81.1 0.288 0.059 16 980 94.0 0.285 0.060 18 1003 106.3 0.280 0.061 20 1014 117.3 0.278 0.061 22 1028 128.7 0.275 0.064 24 1045 140.7 0.271 0.068 26 1057 151.5 0.268 0.070 28 1071 162.4 0.265 0.074 30 1077 174.2 0.264 0.076 表4比较了自动定理证明器E在不同基于符号的前提选择方法下的证明性能. E-SInE和Vampire-SInE分别表示在证明器E和Vampire中的SInE[19]方法. 自动定理证明器E在使用SymbolWeight作为前提选择方法时能够证明MPTP2078问题库中超过半数的问题. 与E-SInE和Vampire-SInE相比，SymbolWeight能够帮助自动定理证明器E在MPTP2078基准测试集上分别提高19.49%和10.49%的证明率.
表 4 自动定理证明器E在不同的基于符号的前提选择方法下的证明性能Table 4. Performance of automated theorem prover E with different symbol-based premise selection methods前提选择方法 证明数量/个 证明率/% no-selection 663 30.90 E-SInE 672 32.34 Vampire-SInE 859 41.34 SymbolWeight 1077 51.83 4. 结 论
1） 提出了新的符号权重和相关度计算方法，并基于此设计并实现了用于解决大理论问题的前提选择的方法；
2） 提出了自适应相关度边界，解决了在基于符号的前提选择方法中需要人工地设置相关度边界的问题；
3） 新提出的前提选择方法能够大大地提高自动定理证明器E在MPTP2078问题库上的证明能力.
-
图 8 不同拥堵场景下的性能指标
Figure 8. Performance indicators under different congestion scenarios
表 1 速度模型标准点取值
Table 1. Representative point values of velocity model
相对密度 平均行驶速度/（km•min−1） ${\text{ } }{f_{m,{\text{p} } } }(t){\text{ = } }0$ ${v_{m,0,{\text{p} } } } = 1.00$ ${f_{m,{\text{p} } } }(t) = {b_{m,1,{\text{p} } } }(t){\text{ = } }0.1$ ${v_{m,1,{\text{p} } } } = 0.55$ ${f_{m,{\text{p} } } }(t) = {b_{m,2,{\text{p} } } }(t){\text{ = } }0.2$ ${v_{m,2,{\text{p} } } } = 0.40$ 
下载: 导出CSV
表 2 两种排队模型的性能指标求解结果
Table 2. Solved performance indicators of two queuing models
模型 系统服务率/% 车辆利用率/% 虚拟空间
存储车辆
占比率/%订单流失率/% 利润/
（元•d−1）拥挤传播
排队模型78.50 23.78 0 21.50 4081.50 无穷排队模型 91.33 31.09 34.28 8.67 5139.60
下载: 导出CSV
-
[1] YE J H, WANG D G, LI X, et al. Assessing one-way carsharing’s impacts on vehicle ownership: evidence from Shanghai with an international comparison[J]. Transportation Research Part A: Policy and Practice, 2021, 150: 16-32. doi: 10.1016/j.tra.2021.05.012 [2] 张淼,惠英,汪鸣泉. 汽车共享对城市温室气体排放的影响[J]. 中国人口 · 资源与环境,2012,22(9): 48-53. doi: 10.3969/j.issn.1002-2104.2012.09.008ZHANG Miao, HUI Ying, WANG Mingquan. Urban greenhouse gas emission of car sharing[J]. China Population, Resources and Environment, 2012, 22(9): 48-53. doi: 10.3969/j.issn.1002-2104.2012.09.008 [3] XU M, MENG Q, LIU ZY. Electric vehicle fleet size and trip pricing for one-way carsharing services considering vehicle relocation and personnel assignment[J]. Transportation Research Part B:Methodological, 2018, 111: 60-82. doi: 10.1016/j.trb.2018.03.001 [4] BAPTISTA P, MELO S, ROLIM C. Car sharing systems as a sustainable transport policy: a case Study from Lisbon, Portugal[M]//ATTARD M, SHIFTAN Y. Transport and Sustainability. [S.l.]: Emerald Group Publishing Limited, 2015: 205-227. [5] NANSUBUGA B, KOWALKOWSKI C. Carsharing: a systematic literature review and research agenda[J]. Journal of Service Management, 2021, 32(6): 55-91. doi: 10.1108/JOSM-10-2020-0344 [6] 曹可心,邓羽. 城市共享汽车分布的时空演变及影响因素研究:以北京市主城区为例[J]. 地理科学,2021,41(10): 1792-1801.CAO Kexin, DENG Yu. Spatial-temporal characteristics and impacting factors of carsharing in Beijing[J]. Scientia Geographica Sinica, 2021, 41(10): 1792-1801. [7] 伊二妮. 基于排队论的汽车共享服务系统车辆配置优化研究[D]. 青岛: 山东科技大学, 2018. [8] EFTHYMIOU D, ANTONIOU C, WADDELL P. Factors affecting the adoption of vehicle sharing systems by young drivers[J]. Transport Policy, 2013, 29: 64-73. doi: 10.1016/j.tranpol.2013.04.009 [9] 刘向,洪林,王宁,等. 基于时空消耗的共享汽车拥堵治理效用研究[J]. 汽车工程学报,2020,10(5): 335-341. doi: 10.3969/j.issn.2095-1469.2020.05.04LIU Xiang, HONG Lin, WANG Ning, et al. Research on the effect of car-sharing on traffic congestion management based on spatiotemporal consumption[J]. Chinese Journal of Automotive Engineering, 2020, 10(5): 335-341. doi: 10.3969/j.issn.2095-1469.2020.05.04 [10] 高永,安健,全宇翔. 网络约租车对出行方式选择及交通运行的影响[J]. 城市交通,2016,14(5): 1-8. doi: 10.13813/j.cn11-5141/u.2016.0501GAO Yong, AN Jian, QUAN Yuxiang. The impact of APP-based car sharing on travel mode shift and transportation operation performance[J]. Urban Transport of China, 2016, 14(5): 1-8. doi: 10.13813/j.cn11-5141/u.2016.0501 [11] 张三省,苏倩,张俊青. 基于系统动力学的网约车政策对城市交通的影响研究[J]. 天津大学学报(社会科学版),2019,21(6): 494-502.ZHANG Sanxing, SU Qian, ZHANG Junqing. Analysis of the influence of ride-hailing policy on urban traffic based on system dynamics[J]. Journal of Tianjin University (Social Sciences), 2019, 21(6): 494-502. [12] ZHAO M, LI X, YIN J, et al. An integrated framework for electric vehicle rebalancing and staff relocation in one-way carsharing systems: model formulation and Lagrangian relaxation-based solution approach[J]. Transportation Research Part B: Methodological, 2018, 117: 542-572. doi: 10.1016/j.trb.2018.09.014 [13] HU L, LIU Y. Joint design of parking capacities and fleet size for one-way station-based carsharing systems with road congestion constraints[J]. Transportation Research Part B: Methodological, 2016, 93: 268-299. doi: 10.1016/j.trb.2016.07.021 [14] DENG Y H, CARDIN M A. Integrating operational decisions into the planning of one-way vehicle-sharing systems under uncertainty[J]. Transportation Research Part C: Emerging Technologies, 2018, 86: 407-424. doi: 10.1016/j.trc.2017.11.018 [15] KASPI M, RAVIV T, TZUR M. Parking reservation policies in one-way vehicle sharing systems[J]. Transportation Research Part B: Methodological, 2014, 62: 35-50. doi: 10.1016/j.trb.2014.01.006 [16] 马舒予,胡路,吴佳媛,等. 共享电动汽车系统车队规模与停车泊位数优化[J]. 交通运输工程与信息学报,2022,20(3): 31-42.MA Shuyu, HU Lu, WU Jiayuan, et al. Fleet size and parking capacity optimization of electric carsharing system[J]. Journal of Transportation Engineering and Information, 2022, 20(3): 31-42. [17] 蒋阳升,李衍,李皓,等. 基于模块化仿真的共享汽车联合调度优化[J]. 西南交通大学学报,2023,58(1): 74-82. doi: 10.3969/j.issn.0258-2724.20210083JIANG Yangsheng, LI Yan, LI Hao, et al. Optimization for joint relocation of carsharing based on modular simulation[J]. Journal of Southwest Jiaotong University, 2023, 58(1): 74-82. doi: 10.3969/j.issn.0258-2724.20210083 [18] PARK S, YU W. Analysis of system parameters for one-way carsharing systems[J]. Transportation Letters: the International Journal of Transportation Research, 2021,14(3): 1-11. [19] LI H B, ZHU Y C, CHEN Y X, et al. The object-oriented discrete event simulation modeling: a case study on aircraft spare part management[C]//2015 Winter Simulation Conference (WSC). Huntington Beach: IEEE, 2015: 3514-3525. [20] LI H B, ZHOU C H, LEE B K, et al. Capacity planning for mega container terminals with multi-objective and multi-fidelity simulation optimization[J]. IISE Transactions, 2017, 49(9): 849-862. doi: 10.1080/24725854.2017.1318229 [21] 张维戈,陈连福,黄彧,等. M/G/K排队模型在电动出租汽车充电站排队系统中的应用[J]. 电网技术,2015,39(3): 724-729. doi: 10.13335/j.1000-3673.pst.2015.03.021ZHANG Weige, CHEN Lianfu, HUANG Yu, et al. Application of M/G/K queuing model in queuing system of electric taxi charging station[J]. Power System Technology, 2015, 39(3): 724-729. doi: 10.13335/j.1000-3673.pst.2015.03.021 [22] 李仕鹏. 基于排队论的汽车共享优化设计[D]. 杭州: 杭州电子科技大学, 2013. [23] KENDALL D G. Stochastic processes occurring in the theory of queues and their analysis by the method of the imbedded Markov chain[J]. The Annals of Mathematical Statistics, 1953, 24(3): 338-354 [24] ZEIGLER B P, PRAEHOFER H, KIM T G. Theory of modeling and simulation: integrating discrete event and continuous complex dynamic systems[M]. 2nd edition. Pittsburgh: Academic Press, 2000: 4-5. [25] HU L, ZHAO B, ZHU J X, et al. Two time-varying and state-dependent fluid queuing models for traffic circulation systems[J]. European Journal of Operational Research, 2019, 275(3): 997-1019. doi: 10.1016/j.ejor.2019.01.020 -
下载:
下载:
点击查看大图
计量
- 文章访问数: 513
- HTML全文浏览量: 189
- PDF下载量: 82
- 被引次数: 0