QBF问题中隐蔽集的求解过程

隐蔽集作为QBF问题的重要结构之一,能使QBF这一难求解问题变得更加简单. QBF问题中隐蔽集的求解相当复杂且难以理解. 为了使读者更好的理解QBF问题中隐蔽集的求解过程,本文对QBF问题中隐蔽集的求解过程进行深入研究,结合实例计算变量的深度、选择符合条件的变量X并计算其对应的三角依赖变量集D_ψ^Δ（x）,根据B=B∪{x}=x和ψ''=ψ-D_ψ^Δ（x）的思想求解出问题的隐蔽集,希望本文能为该领域的相关研究人员提供一定的参考.     

图象处理中边界转换的并行算法及其实现

本文提出了一种把图象中边界转换成区域四分树的并行方法.该方法基于MIMD模型,并在曙光1000上实际运行.整个算法用P个处理器可以在时间O((B×logB)/P)内完成其中B是循环代码长度.该算法可应用于图象处理、计算机图形学、模式识别等领域.     

基于词表示模型的领域文献数据可视分析方法

随着科学技术的发展,科研文献数量越来越大,如何从海量文献信息中找出特定领域的研究主题、有影响力的学者和高水平论文是一个巨大的挑战。为此提出一种基于词表示模型的领域文献数据可视分析方法,首先利用词嵌入模型 word2vec 向量化推荐领域相关的关键词,根据这些词向量之间的近似度筛选出领域相关的论文;然后应用 BERTopic 模型从领域论文摘要中提取主题;基于 PageRank 算法计算论文影响力,应用综合考虑作者署名顺序、发表论文数量和论文影响力的作者影响力评价方法 Author-Rank 计算作者的影响力;最后使用多视图协同和交互的可视化方法帮助研究人员从领域的主题词频、主题演变、文献影响力和引用关系、作者影响力等多个角度对特定领域进行快速理解和分析。将该方法应用于食品安全领域的文献数据分析,应用结果和用户测试说明了其有效性。     

基于类型理论的领域数据建模和验证及案例

数据作为软件系统的主要处理对象,其规范性有助于软件系统的设计开发和软件系统之间的数据交换。本文面向行业数据规范及其验证,提出了一种基于类型理论的领域数据建模语言（DDML）和领域建模方法（DDMM）。DDML语言通过定义类型和项的语法和语义,描述领域数据类型和对象的结构,通过定义类型规则及其类型检查算法判定任意项t：T?。DDMM给出了领域数据建模的方法,即构建K₁（原子类型）、K₂（数据元）、K₃（数据元目录）三层框架,生成表示K3层数据元目录之间关系的类型规则。在此基础上,给出了数据元目录序列的定义及其正确性判定算法。基于上述方法,实现了一种领域数据建模工具原型系统,并通过领域数据建模与自动验证的一个实际案例,完成了一个较大规模行业数据规范的制定与验证。     

高阶类型化可验证应用系统体系结构建模及案例

随着应用软件体系结构风格变化和规模变大,其运行环境变得日趋复杂,对应用系统体系结构的设计及其正确性验证提出了新的挑战.现有的应用系统体系结构设计无法支持需求满足验证,需求满足验证需要其它验证工具的支持.而应用系统体系结构在设计阶段的需求满足验证,有助于客观评价应用系统部署方案和系统如期上线以及主动运维.本文面向应用系统体系结构设计及其验证,在模型驱动的软件工程背景下,提出了一种高阶类型化模型驱动的可验证应用系统体系结构建模语言（V_ASAML）与可验证应用系统体系结构建模方法（V_ASAMM）.V_ASAML语言通过定义类型和项的语法和语义,描述构成应用系统体系结构的类型和对象的结构,通过定义两种类型规则及其类型检查算法,判定Γ⊦t：T和Γ⊦R（T₁,T₂）是否成立,其中,结构类类型规则用于描述应用系统体系结构中的组成部分,关系类类型规则用于描述组成部分之间的关系和配置.V_ASAMM方法给出了应用系统体系结构建模过程,包括构建M_bd（基本数据类型）、M_bti（基本接口类型）、M_dev（设备类型）和M_frwk（应用系统框架）等四层,以及自动生成层内与层间类型之间关系对应的类型规则,同时定义了设备类型服务调用图（G_DSI）用以刻画部署要求,定义了类型序列及其正确性用以刻画需求期望性质,并给出了相应的基于类型检查的验证算法.设计实现了基于该方法的原型工具系统V_ASAMS,其中,建模编辑环境支持应用系统部署方案的设计过程,验证环境支持设计是否满足需求的自动验证.通过一个实际案例完成了某行业较大规模应用系统体系结构的建模和验证.     

基于余归纳的最小Kripke结构的求解

状态空间爆炸问题是模型检测的最大障碍.从余归纳（特别是余代数）的角度研究了这个问题.用余归纳的方法证明：（1） 对于任意给定的一类Kripke结构（记为K）,在互模拟等价意义下K中最小Kripke结构（记为K₀）的存在唯一性.K₀描述了K中所有Kripke结构的行为而且没有冗余的状态;（2） 对于任意的M∈K（M可能包含无穷多个状态）,在互模拟等价意义下的相对于（M且基于K₀）的最小Kripke结构（记为K_M）的存在唯一性.由此提出一种求解K_M的算法,并用Ocaml予以简单实现.其应用之一在于可以用状态空间更小的K_M代替M进行模型检测.该方法可自然地推广到基于其他类型函子的余代数结构.     

具有模态词□φ=□1V□2φ且可靠与完备的公理系统

提出具有模态词□φ=□₁V□₂φ的命题模态逻辑,给出其语言、语法与语义,其公理化系统是可靠与完备的,其中,□₁与□₂是给定的模态词.该逻辑的公理化系统具有与公理系统S5相似的语言,但具有不同的语法与语义.对于任意的公式φ,□φ=□₁V□₂φ;框架定义为三元组W,R₁,R₂,模型定义为四元组W,R₁,R₂,I;在完备性定理证明过程中,需要在由所有极大协调集所构成的集合上构造出两个等价关系,其典型模型的构建方法与经典典型模型的构建方法不同.如果□₁的可达关系R₁等于□₂的可达关系R₂,那么该逻辑的公理化系统变成S5.     

IEEE 802.16竞争解决方案的性能分析

目前,IEEE 802.16标准推荐采用基于截断二进制指数回退算法的竞争解决方案.分析了该方案同IEEE 802.11竞争机制的区别,给出了传送机会利用率u、带宽请求延时d以及带宽请求丢失率p_d等性能指标的计算方法.通过性能模拟,讨论了初始化回退窗口W、用户站数目n以及单位时间帧内传送机会数目N_to等参数对性能指标的影响,进而得出基站调整性能参数的一般策略.这些策略对于基站进行上行带宽资源的分配具有指导意义.     

基于适应性分段估计的数据流相似性搜索

相似性搜索在股票交易行情、网络安全、传感器网络等众多领域应用广泛.由于这些领域中产生的数据具有无限的、连续的、快速的、实时的特性,所以需要适合数据流上的在线相似性搜索算法.首先,在具有或不具有全局约束条件下,分别提出了没有索引结构的DTW(dynamic time warping)下限函数LB_seg_WF_global和LB_seg_WF,它们是一种分段DTW技术,能够处理数据流上的非等长序列间在线相似性匹配问题.然后,为了进一步提高LB_seg_WF_global和LB_seg_WF的近似程度,提出了一系列的改进方法.最后,针对流上使用LB_seg_WF_global或LB_seg_WF可能会出现连续失效的情况,分别提出了DTW的下限函数LB_WF_global(具有全局约束条件)和上限函数UB_WF、下限函数LB_WF(不具有全局约束条件).通过增量方式快速估计DTW,极大地减少了估计DTW的冗余计算量.通过理论分析和统计实验,验证了该方法的有效性.     

独立多处理机任务静态调度问题的近似算法

研究独立多处理机任务静态调度问题P_m|fix|C_max,即在m个处理机系统中调度n个多处理机任务,每个任务指派到所需一组处理机上不可剥夺地执行.该问题应用广泛但早已证明为NP难问题,而且也不存在常数近似算法.分析了问题P_m|fix|C_max和其中所有任务都是单位处理机时间的特殊情形P_m|fix,p=1|C_max的调度,并利用实例划分(split scheduling,简称SS)、首次满足优先(first fit,简称FF)和最大宽度优先(large wide first,简称LWF)等方法,构造了问题P_m|fix,p=1|C_max的√2m +1近似算法和问题P_m|fix|C_max的2√m 近似算法,优于目前已有文献的最好结果.     

M/G/c/K blocking probability models and system performance

An exact solution for the M/G/c/K model is only possible for special cases, such as exponential service, a single server, or no waiting room at all. Instead of basing the approximation on an infinite capacity queue as is often the case, an approximation based on a closed-form expression derivable from the finite capacity exponential queue is presented. Properties of the closed-form expression along with its use in approximating the blocking probability of M/G/c/K systems are discussed. Extensive experiments are provided to test and verify the efficacy of our approximate results.     

设计模式变体的描述与验证*

为解决标准设计模式演化后难以检测的问题,引入设计模式变体思想,以Bridge模式为例,给出了八种常用的变体实现,并以人工形式挖掘了四种开源系统中Bridge模式变体的基准数,接着在Apache Ant1.6.2与JHotDraw5.1开源系统中通过六种主流设计模式检测工具进行了变体检测实验。试验结果表明,FCA-CBR方法简单有效,对2种开源系统中Bridge模式变体检测的精确率达到60%与48.1%,与先前方法相比有了较大的提高。     

(r∞, n12, s12) measurements on the 2-CPU CRAY X-MP

We report performance measurements made on the 2-CPU CRAY X-MP at ECMWF, Reading. Vector (SIMD) performance on one CPU is interpreted by the two parameters ($\text{r}{}_{\mathrm{\infty }}\text{, n}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}$), and we find for dyadic operations using FORTRAN $\text{r}{}_{\mathrm{\infty }}\text{= 70}\text{Mflop/s}\text{, n}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}\text{= 53}\text{flop}$. All vector triadic operations produce $\text{r}{}_{\mathrm{\infty }}\text{= 107}\text{Mflop/s}\text{, n}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}\text{= 45}\text{flop}$; and a triadic operation with two vectors and one scalar gives r_∞ = 148 Mflop/s and $\text{n}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}\text{= 60}\text{flop}$. MIMD performance using both CPUs on one job is interpreted with the two parameters ($\text{r}{}_{\mathrm{\infty }}\text{, s}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}$), where $\text{s}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}$ is the amount of arithmetic that could have been done during the time taken to synchronize the two CPUs. We find, for dyadic operations using the TSKSTART and TSKWAIT synchronization primitives, that r_∞ = 130 Mflop/s and $\text{s}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}\text{= 5700}\text{flop}$. This means that a job must contain more than ～ 6000 floating-point operations if it is to run at more than 50% of the maximum performance when split between both CPUs by this method. Less expensive synchronization methods using LOCKS and EVENTS reduces $\text{s}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}$ to 4000 flop and 2000 flop respectively. A simplified form of LOCK synchronization written in CAL code further reduces $\text{s}{}_{\mathrm{<mtext>1</mtext><mtext>2</mtext>}}$ to 220 flop. This is probably the minimum possible value for synchronization overhead on the CRAY X-MP.     

Complex random sample scheduling and its application to an N/M/F/Fmax problem

“Complex Random Sample Scheduling(CRSS)” was proposed in this paper as an efficient heuristic method for solving any permutation scheduling problems. To show the effectiveness of the proposed CRSS, it was applied to an N-job, M-machine, permutation flowshop scheduling problem to minimize makespan, N/M/F/F_max. Numerical experiments made it clear that the proposed CRSS provides a schedule very close to the near-optimal schedule obtained by the existing promising heuristic methods such as taboo search and simulated annealing, within less computation time than these heuristic methods.     

On the M/Ck/1 queue

We obtain the exact analytic expression of the probability distribution of the number of units in a single server queue with Poisson arrivals and Coxian service time distribution (notated as M/C_k/1). A recursive procedure for calculating this probability distribution is given. The well-known queues M/E_k/1 and M/D/1 are re-derived as special cases of the M/C_k/1 queue. Finally, the cases of M/C₂/1 and M/C₃/1 are fully worked out.     

Geom/G/1/n system with LIFO discipline without interrupts and constrained total amount of customers

Consideration was given to the discrete-time queuing system with inversive servicing without interrupts, second-order geometrical arrivals, arbitrary (discrete) distribution of the customer length, and finite buffer. Each arriving customer has length and random volume. The total volume of the customers sojourning in the system is bounded by some value. Formulas of the stationary state probabilities and stationary distribution of the time of customer sojourn in the system were established.     

Properties and performance modelling of finite buffer M/G/1/K networks

Finite buffer, single-server queueing systems and networks are difficult to analyze since the length of time a customer spends in the system does not follow the Markovian property. A two-moment approximation schema is developed for the probability distribution of M/G/1/K systems and extended to the analysis of M/G/1/K   queueing networks. The general purpose of this paper is to develop a flexible and practical transform-free approach for computing the probability distribution and performance measures of the system as well as identify the underlying properties of these systems. It is shown that for most performance measures, a sigmoid or S-shaped curve with an inflection point at ρ=1$\rho =1$ appears as K→∞$K\to \infty$. This has direct implications for the analysis and optimization of such systems. The performance modelling of the M/G/1/K queueing networks of general topologies along with extensive numerical results accompany the paper along with the linear concave performance measures for these systems.     

Efficient implementation of Johnson''s rule for the n/2/F/Fmax scheduling problem

Several efficient algorithms of O(n log n) computational complexity, for the Johnson's rule to schedule a set of simultaneously available jobs on two machines in a flowship to minimize the maximum job flowtime have appeared in the literature. A modified version of one of these algorithms is presented which not only simplifies the programming effort for implementation but is also able to generate all possible optimal sequences obtainable from Johnson's rule.