基于Yices对时间自动机的有界模型检测

为了避免在有界模型检测过程中对变量进行布尔编码以及对时间自动机模型中的时钟进行预处理,给出一个利用SMT(satisfiability modulo theories)工具进行的对时间自动机进行有界模型检测的方法.该方法将时间自动机模型直接转换成SMT工具可识别的逻辑公式,利用SMT工具可求解包含有整数型和实数型变量逻辑公式的能力来进行模型检测.实验结果表明,对于某些可达性性质的验证,该方法的效率有一定的优势.     

模糊计算树逻辑的符号模型检测

对含有模糊不确定性信息的系统进行模型检测时,状态空间爆炸问题成为了亟待解决的主要问题.将形式化的系统模型用拟布尔公式表示,用多终端二叉决策图来对拟布尔公式进行存储.对模糊计算树逻辑的不动点语义给出了解释和证明,然后给出模糊计算树逻辑的符号化模型检测算法,最后通过一个实例验证算法的正确性.该算法可有效缓解对模糊模型检测验证时的状态空间爆炸问题,并扩展了模型检测的应用范围.     

Sunday算法效率分析

针对Sunday算法的过程比较复杂,难以构建马尔可夫链的问题,提出一种新的根据算法的匹配次数差求平均效率的方法。首先选定初等算法作为效率分析的基准算法,使用马尔可夫链得出初等算法比较精确的平均效率估计公式;然后根据相应的概率公式计算出初等算法和Sunday算法匹配过程的差值;将两者结合,得出Sunday算法平均效率估计公式。实验结果表明,由此公式计算的估计值可以代表实际匹配次数的平均值。     

求解#SMT问题的局部搜索算法

#SMT问题是SMT问题的扩展,它需要计算一阶逻辑公式F所有可满足解的个数.目前,该问题已被广泛应用于编译器优化、硬件设计、软件验证和自动化推理等领域.随着#SMT问题的广泛应用,设计可以求解较大规模#SMT实例的求解器亟待解决.基于以上原因,设计了一种求解较大规模#SMT实例的近似求解器——VolComputeWithLocalSearch.它在现有的#SMT精确求解算法的基础上加入差分进化算法,通过调用体积计算工具qhull,进而给出#SMT问题的近似解.算法采用群体规则减少体积计算的次数,差分进化方法快速地枚举各个有解的区域.另外,从理论上证明了VolComputeWithLocalSearch求解器可以得到精确解的下界,使其可以应用在软件测试等只需要知道问题下界的领域.实验结果表明：VolComputeWithLocalSearch求解器是稳定的、具有快速的求解能力,并在高维问题上具有很好的表现.     

改进的基于布尔模型的网页查重算法*

提出一种基于布尔模型的网页查重算法,利用布尔模型寻找适当的特征,建立索引以减少网页文档之间的比较次数.实验验证了这种算法的性能,并取得了较好的效果.     

代数次数的求解算法及其在SIMON-like算法中的应用

代数次数作为布尔函数重要的密码学指标,在密码算法的设计与分析中有着重要的应用.主要研究布尔函数代数次数的求解及其在分组密码SIMON-like算法中的应用.首先,在利用真值表求解代数正规型算法的基础上建立了基于CUDA的并行求解架构,协同利用CPU和GPU的计算资源,极大地缩短了求解代数次数的时间,在较短的时间内求解了SIMON32算法和SIMECK32算法任意轮数的代数正规型和代数次数;其次,在Cube攻击理论的基础上,根据代数次数和超多项式取值之间的关系,设计了估计代数次数的概率算法,估计了一般SIMON-like算法布尔函数的代数次数;最后,从布尔函数代数次数的角度出发,给出了SIMON-like算法在选择不同循环移位参数表现的差异性,进而给出循环移位参数的选取依据.实验结果表明,SIMON算法在原始参数下,达到最大代数次数所需的轮数最短,原始参数具有更高的安全性.     

全局与局部模型交替辅助的差分进化算法

为求解实际复杂工程应用中的高维计算费时优化问题,提出一种全局与局部代理模型交替辅助的差分进化算法。利用历史样本训练全局和局部代理模型,通过交替搜索全局和局部代理模型得到模型最优解并对其进行真实目标函数评价,实现探索和开采的平衡以减少真实目标函数的计算次数,同时通过针对性地选择个体进行真实目标函数计算,辅助算法快速找到目标函数的较优解。在15个低维测试问题和14个高维测试问题上的实验结果表明,在有限的计算资源情况下,该算法在12个低维测试问题上相较于最优重启策略代理辅助的社会学习粒子群优化算法、基于主动学习的代理模型辅助的粒子群优化算法等表现更好,在7个高维测试问题上相较于高斯过程辅助的进化算法、代理模型辅助的分层粒子群优化算法、求解高维费时问题的代理辅助的多种群优化算法等能找到目标函数的更优解。     

基于数值计算的布尔表达式约简工具

运用数论理论中素数的性质和特点,将符号计算问题转化为数值计算问题,设计了一个布尔表达式化简工具。在理论上根据素数的性质重新定义了布尔函数的合取、析取以及非运算,并提供了相应的推理规则;提出基于素数性质的布尔函数约简算法。用VC++实现了布尔表达式约简工具,并为该工具在底层构建了大数据计算模块,以确保对变量个数没有局限性。该工具既可独立使用,也可以提供DLL作为其它软件、工具、算法的一部分。在移动通信用户流失分析中应用了该工具,取得较好的效果。     

路径和下界公式及其在调度问题中的应用

主要是研究以makespan为目标的多机器置换flow shop调度问题.由于它NP-困难,无法用多项式时间算法求解.而路径和关键路径是研究该问题的一个有力工具,对其进行深入分析可以帮助进一步理解问题最基本的特?挖掘其在更多优化算法中的应用,增加该算法的效率.在研究了原有的关键路径基础上,借助于有向栅格图和重新定义的路径及关键路径公式,直观地给出了对工件排列进行插入移动后的新排列的下界公式.另外,在遗传算法和禁忌搜索之外,还给出了下界公式在NEH启发式算法中的应用,并通过实验验证了它在排除没有希望的排列、减少有效搜索空间的强大能力.     

人工鱼群算法在基因调控网络中的应用研究

在分析基因调控网络现状及优缺点的基础上,提出利用人工鱼群算法对阈值布尔网络模型构建下的基因调控网络进行研究。将阈值布尔网络模型应用于花发育形态模型,构建基于预定义吸引子和极限环的综合网络。比较人工鱼群算法与模拟退火算法在基因调控网络中的应用情况,分析网络节点更新机制变化时布尔网络保留吸引子的能力,发现在极限环长度为2和特定网络拓扑下网络才具有鲁棒性。实验结果表明,与模拟退火算法相比,人工鱼群算法在网络发现、鲁棒性方面具有更好的性能,因此利用人工鱼群算法学习布尔网络结构是有效可行的。     

Theory revision with queries: Horn, read-once, and parity formulas

A theory, in this context, is a Boolean formula; it is used to classify instances, or truth assignments. Theories can model real-world phenomena, and can do so more or less correctly. The theory revision, or concept revision, problem is to correct a given, roughly correct concept. This problem is considered here in the model of learning with equivalence and membership queries. A revision algorithm is considered efficient if the number of queries it makes is polynomial in the revision distance between the initial theory and the target theory, and polylogarithmic in the number of variables and the size of the initial theory. The revision distance is the minimal number of syntactic revision operations, such as the deletion or addition of literals, needed to obtain the target theory from the initial theory. Efficient revision algorithms are given for Horn formulas and read-once formulas, where revision operators are restricted to deletions of variables or clauses, and for parity formulas, where revision operators include both deletions and additions of variables. We also show that the query complexity of the read-once revision algorithm is near-optimal.     

Learning Conjunctions of Horn Clauses

An algorithm is presented for learning the class of Boolean formulas that are expressible as conjunctions of Horn clauses. (A Horn clause is a disjunction of literals, all but at most one of which is a negated variable.) The algorithm uses equivalence queries and membership queries to produce a formula that is logically equivalent to the unknown formula to be learned. The amount of time used by the algorithm is polynomial in the number of variables and the number of clauses in the unknown formula.     

Learning via finitely many queries

This work introduces a new query inference model that can access data and communicate with the teacher by asking finitely many Boolean queries in a language L. In this model the parameters of interest are the number of queries used and the expressive power of L. We study how the learning power varies with these parameters. Results suggest that this model may help studying query inference in a resource bounded environment.AMS subject classification 68Q05, 68Q32, 68T05, 03D10, 03D80     

An intelligent query processing for distributed ontologies

In this paper, we propose an intelligent distributed query processing method considering the characteristics of a distributed ontology environment. We suggest more general models of the distributed ontology query and the semantic mapping among distributed ontologies compared with the previous works. Our approach rewrites a distributed ontology query into multiple distributed ontology queries using the semantic mapping, and we can obtain the integrated answer through the execution of these queries. Furthermore, we propose a distributed ontology query processing algorithm with several query optimization techniques: pruning rules to remove unnecessary queries, a cost model considering site load balancing and caching, and a heuristic strategy for scheduling plans to be executed at a local site. Finally, experimental results show that our optimization techniques are effective to reduce the response time.     

SMT-based query tracking for differentially private data analytics systems

Differential privacy enables sensitive data to be analyzed in a privacy-preserving manner. In this paper, we focus on the online setting where each analyst is assigned a privacy budget and queries the data interactively. However, existing differentially private data analytics systems such as PINQ process each query independently, which may cause an unnecessary waste of the privacy budget. Motivated by this, we present a satisfiability modulo theories (SMT)-based query tracking approach to reduce the privacy budget usage. In brief, our approach automatically locates past queries that access disjoint parts of the dataset with respect to the current query to save the privacy cost using the SMT solving techniques. To improve efficiency, we further propose an optimization based on explicitly specified column ranges to facilitate the search process. We have implemented a prototype of our approach with Z3, and conducted several sets of experiments. The results show our approach can save a considerable amount of the privacy budget and each query can be tracked efficiently within milliseconds.     

自适应的P2P网络路由方法研究

在分析一系列P2P网络资源发现方法的基础上,提出了一种基于查询的P2P网络路由方法（Query-based Routing Method in P2P network,QRM方法）。在该方法中,节点会记录收到的查询以及满足该查询的节点,在这些节点中,优先存储那些距离较远的节点。仿真实验表明,随着查询的增多,该方法能有效地提高查询效率。     

Approximate counting in SMT and value estimation for probabilistic programs

#SMT, or model counting for logical theories, is a well-known hard problem that generalizes such tasks as counting the number of satisfying assignments to a Boolean formula and computing the volume of a polytope. In the realm of satisfiability modulo theories (SMT) there is a growing need for model counting solvers, coming from several application domains (quantitative information flow, static analysis of probabilistic programs). In this paper, we show a reduction from an approximate version of #SMT  to SMT. We focus on the theories of integer arithmetic and linear real arithmetic. We propose model counting algorithms that provide approximate solutions with formal bounds on the approximation error. They run in polynomial time and make a polynomial number of queries to the SMT solver for the underlying theory, exploiting “for free” the sophisticated heuristics implemented within modern SMT solvers. We have implemented the algorithms and used them to solve the value problem for a model of loop-free probabilistic programs with nondeterminism.

     

大数据环境中非交互式查询差分隐私保护模型

针对大数据环境下,非交互式差分隐私无法准确提供及处理大量范围查询的问题,提出一种基于最大信息系数与机器学习的隐私保护数据查询模型。对原始数据集采用最大信息系数选出相关性低的数据作为训练样本集,然后结合差分隐私的并行组合性质对其进行分块划分得到隐私保护的训练样本集,最后应用线性回归算法训练样本集得到差分隐私保护预测模型,该模型隐私保护的方式回答当前提交和大量未知的查询。实验结果表明,所提出的模型在提升发布数据效用性的同时,也提高了查询处理的效率。     

Learning intersections and thresholds of halfspaces

We give the first polynomial time algorithm to learn any function of a constant number of halfspaces under the uniform distribution on the Boolean hypercube to within any constant error parameter. We also give the first quasipolynomial time algorithm for learning any Boolean function of a polylog number of polynomial-weight halfspaces under any distribution on the Boolean hypercube. As special cases of these results we obtain algorithms for learning intersections and thresholds of halfspaces. Our uniform distribution learning algorithms involve a novel non-geometric approach to learning halfspaces; we use Fourier techniques together with a careful analysis of the noise sensitivity of functions of halfspaces. Our algorithms for learning under any distribution use techniques from real approximation theory to construct low-degree polynomial threshold functions. Finally, we also observe that any function of a constant number of polynomial-weight halfspaces can be learned in polynomial time in the model of exact learning from membership and equivalence queries.