Theory decision by decomposition

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulæ. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based first-order theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis–Putnam–Logemann–Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories.     

Design and Results of the First Satisfiability Modulo Theories Competition (SMT-COMP 2005)

The Satisfiability Modulo Theories Competition (SMT-COMP) is intended to spark further advances in the decision procedures field, especially for applications in hardware and software verification. Public competitions are a well-known means of stimulating advancement in automated reasoning. Evaluation of SMT solvers entered in SMT-COMP took place while CAV 2005 was meeting. Twelve solvers were entered; 1,352 benchmarks were collected in seven different divisions.     

基于一阶逻辑的可满足求解方法研究进展

基于命题逻辑的布尔可满足SAT存在描述能力弱、抽象层次低、求解复杂度高等问题,而基于一阶逻辑的可满足性模理论SMT采用高层建模语言,表达能力更强,更接近于字级设计,避免将问题转化到位级求解,在硬件RTL级验证、程序验证与实时系统验证等领域得到了广泛应用。针对近年来涌现的众多SMT求解方法,依据方法的求解方式进行了分类与对比。而后,对3种主流的求解方法Eager方法、Lazy方法和DPLL(T)方法的实现进行了概要介绍。最后,讨论了SMT求解方法当前所面临的主要挑战以及在SMT求解方面的一些研究成果,并对今后的研究进行了展望。     

Combination of convex theories: Modularity,deduction completeness,and explanation

Decision procedures are key components of theorem provers and constraint satisfaction systems. Their modular combination is of prime interest for building efficient systems, but their effective use is often limited by poor interface capabilities, when such procedures only provide a simple “sat/unsat” answer. In this paper, we develop a framework to design cooperation schemas between such procedures while maintaining modularity of their interfaces. First, we use the framework to specify and prove the correctness of classic combination schemas by Nelson–Oppen and Shostak. Second, we introduce the concept of deduction complete satisfiability procedures, we show how to build them for large classes of theories, then we provide a schema to modularly combine them. Third, we consider the problem of modularly constructing explanations for combinations by re-using available proof-producing procedures for the component theories.     

Decision procedures for elementary sublanguages of set theory: X. Multilevel syllogistic extended by the singleton and powerset operators

The class of unquantified formulae of set theory involving Boolean operators, the powerset and singleton operators, and the equality and membership predicates is shown to have a solvable satisfiability problem.It is shown that whenever a formula in the above class is satisfiable there exists a hereditarily finite model of , whose rank is bounded by a doubly exponential expression in the number of variables occurring in .This paper was written while the author was a Visiting Professor at Courant Institute of Mathematical Sciences, New York University, U.S.A.     

A decision procedure for combinations of propositional temporal logic and other specialized theories

We present a decision procedure for formulae of discrete linear time propositional temporal logic whose propositional part may include assertions in a specialized theory. The combined decision procedure may be viewed as an extension of known decision procedures for quantifier-free theories to theories including temporal logic connectives. A combined decision procedure given by Pratt restricted to linear time temporal logic, runs in polynomial space relative to an oracle for the underlying theory. Our procedure differs from this one in that it can handle assertions containing arbitrary mixtures of global variables, whose values cannot change with time, and state variables, whose values can change with time. This new procedure can also handle assertions containing functions and predicates whose interpretations do not change with time. However, it requires the computation of least and greatest fixed points and has a worse asymptotic running time than that of Pratt. This new procedure has been implemented and seems efficient enough to be practical on simple formulae, although an upper bound derived for the worst case running time is triple exponential in the length of the formula. The techniques used appear to apply to logics other than temporal logic which have decision procedures based on tableaux. Most of this work was done while the author was at SRI International, Menlo Park, California, and at the University of Illinois, Urbana, Illinois, U.S.A. This work was partially supported by the National Science Foundation under grants MCS 81-09831 and MCS 83-07755.     

An integral theorem prover and the role of proof planning

An investigation is made into the ways proof planning can enhance the capability of a rule based prover for the theory of integration. The integrals are of the Riemann type and are defined in a way to maximize the theorem proving methods of predicate calculus. Approximately fifty theorems have been proved and several examples are discussed. A major shortcoming was found to be the inability of the system to work with or produce a proof plan. As a result, a planning scheme based on the idea of subgoals or milestones was considered. With user defined plans, there was a substantial increase in performance and capability of the system and, in some cases, proofs which were previously unsuccessful were completed.     

Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts

We illustrate a methodology for formalizing and reasoning about Abadi and Cardelli’s object-based calculi, in (co)inductive type theory, such as the Calculus of (Co)Inductive Constructions, by taking advantage of natural deduction semantics and coinduction in combination with weak higher-order abstract syntax and the Theory of Contexts. Our methodology allows us to implement smoothly the calculi in the target metalanguage; moreover, it suggests novel presentations of the calculi themselves. In detail, we present a compact formalization of the syntax and semantics for the functional and the imperative variants of the ς-calculus. Our approach simplifies the proof of subject deduction theorems, which are proved formally in the proof assistant Coq with a relatively small overhead. Supported by UE project IST-CA-510996 Types and French grant CNRS ACI Modulogic.     

Reconstructing (h,v)-convex 2-dimensional patterns of objects from approximate horizontal and vertical projections

The problem of reconstructing a pattern of an object from its approximate discrete orthogonal projections in a 2-dimensional grid, may have no solution because the inaccuracy in the measurements of the projections may generate an inconsistent problem. To attempt to overcome this difficulty, one seeks to reconstruct a pattern with projection values having possibly some bounded differences with the given projection values and minimizing the sum of the absolute differences.

This paper addresses the problem of reconstructing a pattern with a difference at most equal to +1 or −1 between each of its projection values and the corresponding given projection value. We deal with the case of patterns which have to be horizontally and vertically convex and the case of patterns which have to be moreover connected, the so-called convex polyominoes. We show that in both cases, the problem of reconstructing a pattern can be transformed into a Satisfiability (SAT) Problem. This is done in order to take advantage of the recent advances in the design of solvers for the SAT Problem. We show, experimentally, that by adding two important features to CSAT (an efficient SAT solver), optimal patterns can be found if there exist feasible ones. These two features are: first, a method that extracts in linear time an optimal pattern from a set of feasible patterns grouped in a generic pattern (obtaining a generic pattern may be exponential in the worst case) and second, a method that computes actively a lower bound of the sum of absolute differences that can be obtained from a partially defined pattern. This allows to prune the search tree if this lower bound exceeds the best sum of absolute differences found so far.     

Properties of the satisfiability threshold of the strictly d-regular random (3, 2s)-SAT problem

A k-CNF (conjunctive normal form) formula is a regular (k, s)-CNF one if every variable occurs s times in the formula, where k≥2 and s>0 are integers. Regular (3, s)- CNF formulas have some good structural properties, so carrying out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysis for random 3-CNF formulas. Some subclasses of the regular (3, s)-CNF formula have also characteristics of intractability that differ from random 3-CNF formulas. For this purpose, we propose strictly d-regular (k, 2s)-CNF formula, which is a regular (k, 2s)-CNF formula for which d≥0 is an even number and each literal occurs s-\frac{d}{2} or s+\frac{d}{2} times (the literals from a variable x are x and \neg x, where x is positive and \neg x is negative). In this paper, we present a new model to generate strictly d-regular random (k, 2s)-CNF formulas, and focus on the strictly d-regular random (3, 2s)-CNF formulas. Let F be a strictly d-regular random (3, 2s)-CNF formula such that 2s>d. We show that there exists a real number s₀ such that the formula F is unsatisfiable with high probability when s>s₀, and present a numerical solution for the real number s₀. The result is supported by simulated experiments, and is consistent with the existing conclusion for the case of d= 0. Furthermore, we have a conjecture: for a given d, the strictly d-regular random (3, 2s)-SAT problem has an SAT-UNSAT (satisfiable-unsatisfiable) phase transition. Our experiments support this conjecture. Finally, our experiments also show that the parameter d is correlated with the intractability of the 3-SAT problem. Therefore, our research maybe helpful for generating random hard instances of the 3-CNF formula.     

An Ant Colony Algorithm (ACA) for solving the new integrated model of job shop scheduling and conflict-free routing of AGVs

This paper concerns with the Job Shop Scheduling Problem (JSSP) considering the transportation times of the jobs from one machine to another. The goal of a basic JSSP is to determine starting and ending times for each job in which the objective function can be optimized. In here, several Automated Guided Vehicles (AGVs) have been employed to transfer the jobs between machines and warehouse located at the production environment. Unlike the advantages of implemented automatic transportation system, if they are not controlled along the routes, it is possible that the production system encounters breakdown. Therefore, the Conflict-Free Routing Problem (CFRP) for AGVs is considered as well as the basic JSSP. Hence, we proposed a mathematical model which is composed of JSSP and CFRP, simultaneously and since the problem under study is NP-hard, a two stage Ant Colony Algorithm (ACA) is also proposed. The objective function is to minimize the total completion time (make-span). Eventually, in order to show the model and algorithm’s efficiency, the computational results of 13 test problems and sensitivity analysis are exhibited. The obtained results show that ACA is an efficient meta-heuristic for this problem, especially for the large-sized problems. In addition, the optimal number of both AGVs and rail-ways in the production environment is determined by economic analysis.     

GF(2m)域上通用可配置乘法器的设计与实现

提出了一种应用于椭圆曲线密码体制中的有限域乘法器结构,基于已有的digit-serial结构乘法器,利用局部并行的bit-parallel结构,有效地省去了模约简电路,使得乘法器适用于任意不可约多项式;通过使用数据接口控制输入数据的格式并内嵌大尺寸乘法器,可以配置有限域乘法器的结构,用以实现基于多项式基的有限域乘法运算。该结构可以有效满足椭圆曲线密码体制的不同安全需求。     

GF(2n)域上基于ONB的ECC运算单元设计与实现

分析了GF(2n)域上基于优化正规基(ONB)的椭圆曲线的运算法则，讨论了域划分对芯片实现速度和硬件资源占用二者的影响，设计了一种串-并行结构的基于ONB的高速有限域运算单元，用于完成GF(2191)域上基于ONB的ECC芯片实现，在50MHz时钟下，GF(2191)域上的点乘运算速度平均为981次/s。     

二元域大型稀疏矩阵向量乘的FPGA设计与实现

作为Wiedemannn算法的核心部分,稀疏矩阵向量乘是求解二元域上大型稀疏线性方程组的主要步骤。提出了一种基于FPGA的二元域大型稀疏矩阵向量乘的环网硬件系统架构,为解决Wiedemannn算法重复计算稀疏矩阵向量乘,提出了新的并行计算结构。实验分析表明,提出的架构提高了Wiedemannn算法中稀疏矩阵向量乘的并行性,同时充分利用了FPGA的片内存储器和吉比特收发器,与目前性能最好的部分可重构计算PR模型相比,实现了2.65倍的加速性能。     

Prelaunch calibration and primary results from in-orbit calibration of the atmospheric correction microwave radiometer (ACMR) on the HY-2A satellite of China

The atmospheric correction microwave radiometer (ACMR) is one of the main payloads for correcting atmospheric path delay in the radar altimeter on the Haiyang-2A (HY-2A) satellite. The ACMR is a three-band microwave radiometer operating at 18.7, 23.8, and 37.0 GHz. Calibration of the ACMR is important for applying its measurements to correct for atmospheric effects on the HY-2A altimeter signal transmission in the air. Therefore, a detailed introduction to the principles and specifications of the ACMR system is given first. The thermal vacuum calibration method of the ACMR is discussed and analysed, and the microwave transfer functions and related coefficients are given, especially the nonlinear coefficients derived from a test for correcting nonlinear responses between the input of antenna temperature and the output of voltage at each channel of the ACMR. Furthermore, antenna pattern correction algorithms for removing the effects of side lobe and cross-polarization are derived and their coefficients are used for in-orbit data processing. Primary calibration results are given by comparing with the similar spaceborne Jason microwave radiometer (JMR) on the Jason-1 satellite and with the advanced microwave radiometer (AMR) on Jason-2. The results of this comparison show that the data from the ACMR match well to those from the JMR and AMR.     

Developing an research and development (R&D) process improvement system to simulate the performance of R&D activities

Because of a shorter R&D cycle time and the increasing complexity of technology development, efficient decision support systems for R&D activities are necessary to facilitate R&D processes. In particular, small and medium enterprises (SMEs) require efficiency of R&D projects due to a lack of R&D budgets and resources. Therefore, this paper aims to develop a system which can assess current levels of R&D processes of companies and improve problematic processes. To this end, the proposed system applies a standard R&D process to evaluate the R&D level of companies, including four types of database and three modules: performance level analysis, comparison analysis, and performance simulation analysis. First, the module of performance level analysis aims to draw strong and weak R&D processes of companies, using three factors: importance, performance goal and current performance on each process. The second module provides the function of comparison analysis that compares the performance level of a company with that of others. Finally, the performance simulation analysis investigates influences of critical processes on R&D outcomes and predicts how much the processes can enhance technical, economic and process outcomes. In particular, a case study is presented to illustrate the application of the proposed system to an IT company. This system can help managers enhance their R&D performance by presenting necessary improvements on critical processes.     

数据挖掘工具DMTools的设计与实现

介绍了一个通用的数据工具ＤＭＴｏｏｌｓ。它实现了基于数据库的知识发现的主要过程,可视分析,数据预处理,数据库的知识发现,数据挖掘,模型解释及模型评估算。主要介绍了这个系统的体系结构和各愉的功能。使用本工具。可从各行业的历史业务数据库中挖掘出隐含的有价值的知识,用于决策支持。     

攀钢2#连铸机切割优化模型的设计与实现

切割优化模型是连铸过程控制计算机系统的一个重要模型,它在生产过程中根据实际的生产计划形成切割计划,并对产生的废坯进行优化,以满足生产要求,提高产品质量及收得率。切割优化模型必须遵循一定的规则或搜索策略才能达到优化的目的。介绍了一种基于手段 目的分析法的连铸机切割优化模型,对模型的设计、功能模块、优化规则及算法实现做了描述。模型已在攀钢2#板坯连铸机上成功运行,对国内同行具有一定的参考价值。