A self-adaptive multi-engine solver for quantified Boolean formulas

In this paper we study the problem of engineering a robust solver for quantified Boolean formulas (QBFs), i.e., a tool that can efficiently solve formulas across different problem domains without the need for domain-specific tuning. The paper presents two main empirical results along this line of research. Our first result is the development of a multi-engine solver, i.e., a tool that selects among its reasoning engines the one which is more likely to yield optimal results. In particular, we show that syntactic QBF features can be correlated to the performances of existing QBF engines across a variety of domains. We also show how a multi-engine solver can be obtained by carefully picking state-of-the-art QBF solvers as basic engines, and by harnessing inductive reasoning techniques to learn engine-selection policies. Our second result is the improvement of our multi-engine solver with the capability of updating the learned policies when they fail to give good predictions. In this way the solver becomes also self-adaptive, i.e., able to adjust its internal models when the usage scenario changes substantially. The rewarding results obtained in our experiments show that our solver AQME—Adaptive QBF Multi-Engine—can be more robust and efficient than state-of-the-art single-engine solvers, even when it is confronted with previously uncharted formulas and competitors.     

Compressing BMC Encodings with QBF

Symbolic model checking is PSPACE complete. Since QBF is the standard PSPACE complete problem, it is most natural to encode symbolic model checking problems as QBF formulas and then use QBF decision procedures to solve them. We discuss alternative encodings for unbounded and bounded safety checking into SAT and QBF. One contribution is a linear encoding of simple path constraints, which usually are necessary to make k-induction complete. Our experimental results show that indeed a large reduction in the size of the generated formulas can be obtained. However, current QBF solvers seem not to be able to take advantage of these compact formulations. Despite these mostly negative results the availability of these benchmarks will help improve the state of the art of QBF solvers and make QBF based symbolic model checking a viable alternative.     

基于加密二维条码和指纹识别的证件防伪系统

目前证件造假越来越多,因此提出一种新的证件防伪方法。二维条码信息密度高,应用成本低廉,将其用于证件防伪中能有效的验证证件本身的真假;同时将指纹信息存储于二维条码中,利用指纹识别技术可以验证持证人真伪。在进行证件双重验证的同时与加密技术相结合,来保证证件信息的安全携带。实验结果表明对证件的误识率（FAR）为0,拒识率（FRR）为1．38％。基于加密的二维条码和指纹识别技术的证件防伪系统具有深刻的应用价值。     

A solver for QBFs in negation normal form

Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, $\ensuremath{\sf qpro}Various problems in artificial intelligence can be solved by translating them into a quantified boolean formula (QBF) and evaluating the resulting encoding. In this approach, a QBF solver is used as a black box in a rapid implementation of a more general reasoning system. Most of the current solvers for QBFs require formulas in prenex conjunctive normal form as input, which makes a further translation necessary, since the encodings are usually not in a specific normal form. This additional step increases the number of variables in the formula or disrupts the formula’s structure. Moreover, the most important part of this transformation, prenexing, is not deterministic. In this paper, we focus on an alternative way to process QBFs without these drawbacks and describe a solver, , which is able to handle arbitrary formulas. To this end, we extend algorithms for QBFs to the non-normal form case and compare with the leading normal form provers on several problems from the area of artificial intelligence. We prove properties of the algorithms generalized to non-clausal form by using a novel approach based on a sequent-style formulation of the calculus. This paper is based on an extended abstract presented at ECAI 2006 (see [16]). This work was supported by the Austrian Science Fund (FWF) under grant P18019, the Austrian Academic Exchange Service (?AD) under grant Amadée 2/2006, and by the Austrian Federal Ministry of Transport, Innovation and Technology BMVIT and the Austrian Research Promotion Agency FFG under grant FIT-IT-810806.     

Solving quantified constraint satisfaction problems

We make a number of contributions to the study of the Quantified Constraint Satisfaction Problem (QCSP). The QCSP is an extension of the constraint satisfaction problem that can be used to model combinatorial problems containing contingency or uncertainty. It allows for universally quantified variables that can model uncertain actions and events, such as the unknown weather for a future party, or an opponent's next move in a game. In this paper we report significant contributions to two very different methods for solving QCSPs. The first approach is to implement special purpose algorithms for QCSPs; and the second is to encode QCSPs as Quantified Boolean Formulas and then use specialized QBF solvers. The discovery of particularly effective encodings influenced the design of more effective algorithms: by analyzing the properties of these encodings, we identify the features in QBF solvers responsible for their efficiency. This enables us to devise analogues of these features in QCSPs, and implement them in special purpose algorithms, yielding an effective special purpose solver, QCSP-Solve. Experiments show that this solver and a highly optimized QBF encoding are several orders of magnitude more efficient than the initially developed algorithms. A final, but significant, contribution is the identification of flaws in simple methods of generating random QCSP instances, and a means of generating instances which are not known to be flawed.     

一种基于RSA签名的多KAC公钥认证模式

在公开密钥系统中，公钥的认证是非常重要的。本提出了一种新的基于RSA签名的认证模式。在该模式中，多个KAC和用户共同产生公钥证明，但任何KAC均不参与验证过程，验证由用户独立完成。该模式安全性好，能够有效地防止KAC伪造假冒证明。     

SDSI中名字证书链的分布式发现

利用处理基于角色的证书体系的证书图,实现了对SDSI名字证书的处理。基于这种证书图,给出了针对SDSI名字证书的分布式搜索算法,并证明其可靠性和完备性,表明当证书适当存储时,该算法能搜索和找到相关证书并形成证书链。与现有的自下至上的证书搜索算法相比,该算法更好地适应了SDSI名字证书的分布式存储特性。作为有目的的搜索算法, 它具备了自下至上算法所不具有的高效性、灵活性,更适合应用于海量证书分散存储的Internet。     

A Syntactic Approach to Foundational Proof-Carrying Code

Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in the typing rules. In foundational proof-carrying code (FPCC), on the other hand, proofs are constructed and verified by using strictly the foundations of mathematical logic, with no type-specific axioms. FPCC is more flexible and secure because it is not tied to any particular type system and it has a smaller trusted base. Foundational proofs, however, are much harder to construct. Previous efforts on FPCC all required building sophisticated semantic models for types. Furthermore, none of them can be easily extended to support mutable fields and recursive types. In this article, we present a syntactic approach to FPCC that avoids all of these difficulties. Under our new scheme, the foundational proof for a typed machine program simply consists of the typing derivation plus the formalized syntactic soundness proof for the underlying type system. The former can be readily obtained from a type-checker, while the latter is known to be much easier to construct than the semantic soundness proofs. We give a translation from a typed assembly language into FPCC and demonstrate the advantages of our new system through an implementation in the Coq proof assistant.     

SPKI2.0信任模型的改进及应用

本文简要介绍了SPKI证书,同时提出使用SPKI证书进行访问控制时容易出现的问题,即查找证书链失败的问题,并提出了对SPKI授权认证模型改进的方法,使得当授权证书链不存在时客户端建立新的证书链访问资源服务器,并将此模型应用于网上电子商务中。     

Conformant planning as a case study of incremental QBF solving

We consider planning with uncertainty in the initial state as a case study of incremental quantified Boolean formula (QBF) solving. We report on experiments with a workflow to incrementally encode a planning instance into a sequence of QBFs. To solve this sequence of successively constructed QBFs, we use our general-purpose incremental QBF solver DepQBF. Since the generated QBFs have many clauses and variables in common, our approach avoids redundancy both in the encoding phase as well as in the solving phase. We also present experiments with incremental preprocessing techniques that are based on blocked clause elimination (QBCE). QBCE allows to eliminate certain clauses from a QBF in a satisfiability preserving way. We implemented the QBCE-based techniques in DepQBF in three variants: as preprocessing, as inprocessing (which extends preprocessing by taking into account variable assignments that were fixed by the QBF solver), and as a novel dynamic approach where QBCE is tightly integrated in the solving process. For DepQBF, experimental results show that incremental QBF solving with incremental QBCE outperforms incremental QBF solving without QBCE, which in turn outperforms nonincremental QBF solving. For the first time we report on incremental QBF solving with incremental QBCE as inprocessing. Our results are the first empirical study of incremental QBF solving in the context of planning and motivate its use in other application domains.     

基于Clark-Wilson的属性证书授权模型

本文采用Clark-Wilson完整型模型,使用属性证书作为权限传递的载体,结合授权管理基础设施（PMI）实现基于角色的授权模型,并提出一种形式化描述架构,描述权限、证书和相关的授权;基于语义的演算过程对给定的属性证书集和撤销证书集可以验证某种权限是否有效;采用Alloy形式化语言来定义模型,并且给出描述扩展Clark-Wilson的方法。     

Solution Validation and Extraction for QBF Preprocessing

In the context of reasoning on quantified Boolean formulas (QBFs), the extension of propositional logic with existential and universal quantifiers, it is beneficial to use preprocessing for solving QBF encodings of real-world problems. Preprocessing applies rewriting techniques that preserve (satisfiability) equivalence and that do not destroy the formula’s CNF structure. In many cases, preprocessing either solves a formula directly or modifies it such that information helpful to solvers becomes better visible and irrelevant information is hidden. The application of a preprocessor, however, prevented the extraction of proofs for the original formula in the past. Such proofs are required to independently validate the correctness of the preprocessor’s rewritings and the solver’s result as well as for the extraction of solutions in terms of Skolem functions. In particular for the important technique of universal expansion efficient proof checking and solution generation was not possible so far. This article presents a unified proof system with three simple rules based on quantified resolution asymmetric tautology (\(\mathsf {QRAT}\)). In combination with an extended version of universal reduction, we use this proof system to efficiently express current preprocessing techniques including universal expansion. Further, we develop an approach for extracting Skolem functions. We equip the preprocessor bloqqer with \(\mathsf {QRAT}\) proof logging and provide a proof checker for \(\mathsf {QRAT}\) proofs which is also able to extract Skolem functions.     

基于区块链的零知识位置证明系统设计

智能终端设备及定位技术的发展催生了许多基于位置的服务，如定点打卡服务（访问特定地点获取相应的奖励），这导致非法用户为了获取利益对位置服务器进行位置欺骗。因此，需要对用户提供的位置证书进行验证。但现有的位置证明系统在验证用户位置证书的同时对用户隐私保护并不周全，且用户对位置证书的控制并不灵活。基于区块链技术，提出一种分布式位置证明系统架构；进而在此架构基础上，引入零知识证明，提出一种零知识位置证明协议。架构与协议组成的零知识位置证明系统允许用户根据需求，自由选择披露的证书内容及位置精度，实现分级的位置隐私保护。     

多线程程序数据竞争检测与证据生成方法

数据竞争是多线程程序最为常见的问题之一。由于线程交织导致状态空间爆炸,多线程程序数据竞争引起的错误检测难度大、成本高、精度低;此外,即使检测到数据竞争,由于线程调度难以控制、执行过程难以复现,错误难以复现和定位。提出了一种多线程程序数据竞争检测与证据生成方法,基于程序语义分析和执行过程监测,构建程序的执行路径约束模型和数据竞争条件,将多线程程序数据竞争检测问题转化为约束求解问题,降低检测难度,提高检测精度;利用SMT求解器计算可能的数据竞争,并生成触发该数据竞争的程序执行序列,协助程序员定位和验证错误。实验中对10个程序进行了测试,相比现有数据竞争检测工具threadsanitizer和helgrind,本方法检测出的数据竞争多出287.5%和264.7%,且没有误报,而其他方法平均误报率为10.5%和9.8%。     

求解QBF 问题的启发式调查传播算法

提出了一种启发式调查传播算法,并基于该算法设计了一种QBF(quantified Boolean formulae)求解器——HSPQBF(heuristic survey propagation algorithm for solving QBF)系统.它将Survey Propagation信息传递方法应用到QBF求解问题中.利用Survey Propagation作为启发式引导DPLL(Davis,Putnam,Logemann and Loveland)算法,选择合适的变量进行分支,从而可以减小搜索空间,并减少算法回退的次数.在分支处理过程中,HSPQBF系统结合了单元传播、冲突学习和满足蕴涵学习等一些优秀的QBF求解技术,从而能够提高QBF问题的求解效率.实验结果表明,HSPQBF无论在随机问题上还是在QBF标准测试问题上都有很好的表现,验证了调查传播技术在QBF问题求解中的实际价值.     

基于证书的语义Web服务访问控制方法

为了实现语义Web服务环境中的访问控制机制,研究了基于证书授权的访问控制方法.在对语义Web服务的访问控制需求进行分析的基础上,提出了将简单公钥基础设施/简单分布式安全基础设施(SPKI/SDSI)证书与OWL-S本体描述集成的访问控制方法,该方法将访问控制描述与服务功能描述集成在一个统一的框架中,既便于管理又提高了用户访问Web服务的效率.     

平滑学习算法在机器翻译消歧中的应用

机器翻译中,在词性标注和句法语义分析阶段经常会遇到歧义,使用基于统计方法的词汇评分和句法语义评分就是对词性标注和句法语义分析阶段产生的歧义进行消歧,在用统计方法消歧时,经常遇到的一个现象就是数据稀疏问题,本文对词汇评分和句法语义评分遇到数据稀疏现象使用改进的Turing公式来平滑参数,给出平滑算法对词汇评分平滑的处理过程,在实验中给出语料与参数数量,正确率的实验结果。     

基于代理属性证书的分布式RBAC系统

采用属性证书的方式可对分布式RBAC系统中的用户进行有效的管理,并通过证书中的签名确保证书的有效性.但全部工作都由系统管理员完成,管理员的负担重,在大型分布式的应用中存在瓶颈.设计基于可跟踪代理签名的证书及其代理发布,不仅有效的分散了管理员的任务,而且管理员和代理者不能滥用权力,攻击者也不能伪造证书和冒充用户,解决了管理员签发证书的效率问题,提高了RBAC系统的效率和安全性.