对数空间可构造的无向图遍历序列

研究了为无向连通子图设计环状遍历序列（TSC）的空间复杂性问题。通过定义对数空间的Cook归约,分析了TSC问题与无向图连接性问题及通用遍历序列构造问题的关系,证明了TSC问题以及无向图遍历问题是对数空间可解的,并给出了一个TSC一般性构造方法。最后还提出了一个更有效的针对树状图的TSC构造算法。     

Completeness of a first-order temporal logic with time-gaps

The first-order temporal logics with □ and ○ of time structures isomorphic to ω (discrete linear time) and trees of ω-segments (linear time with branching gaps) and some of its fragments are compared: the first is not recursively axiomatizable. For the second, a cut-free complete sequent calculus is given, and from this, a resolution system is derived by the method of Maslov.     

On institutions for modular coalgebraic specifications

We present an algebraic extension of standard coalgebraic specification techniques for state-based systems which allows us to integrate constants and n-ary operations in a smooth way and which leads to institutions enabling the use of modular specification techniques. A sound and complete proof system for first-order observational properties of modular specifications is given. The framework of (Ω,Ξ)-structures that we present can be considered as the result of a transformation of concepts of observational logic as in Hennicker and Bidoit (in: A. Haeberer (Ed.), Algebraic Methodology and Software Technology (AMAST’98), Lecture Notes in Computer Science, vol. 1548, Springer, Berlin, 1999) into the coalgebraic world. Moreover, it is shown that the features of (Ω,Ξ)-structures that make them suitable models for an observational approach to specifications can be categorically expressed by the fact that the operation mapping an (Ω,Ξ)-structure to its behaviour is a fibred idempotent monad.     

On completeness for NP via projection translations

In this paper we investigate the logics obtained by augmenting first-order logic (with successor) with operators corresponding to some decision problems complete forNP via logspace reductions. We show that our encodings of the Satisfiability Problem and the 3-Colourability Problem, namely SAT and 3COL, respectively (as sets of finite structures over specific vocabularies), are complete forNP via projection translations (very weak reductions between problems): the fact that an encoding of the Satisfiability Problem (resp. the 3-Satisfiability Problem) is (resp. not) complete forNP via interpretative reductions (again, very weak reductions) had been shown previously by Dahlhaus. It is unknown whether our encoding of the 3-Satisfiability Problem, namely 3SAT, is complete forNP via projection translations, although we show that it is for iterated projection translations. However, if we consider an encoding of the version of the 3-Satisfiability Problem where each instance has at most three literals in each clause (as opposed to exactly three literals), namely 3SAT, then we show that 3SAT is complete forNP via projection translations. It appears to matter as to how we encode a decision problem as a set of finite structures over some vocabulary when considering weak reductions such as ours. Our proof that SAT is complete forNP via projection translations differs extremely from the proof of Dahlhaus that SAT is complete forNP via interpretative reductions, as he relies on Fagin's well-known characterization ofNP whereas our results do not: indeed, they give Fagin's result as a corollary. We use the problem 3COL to show the difference between interpretative reductions and projection translations as we show that 3COL is complete forNP via the latter but not via the former. The logics mentioned above are shown to be similar in expressibility but are shown to be much more expressible than that formed by extending first-order logic with an operator corresponding to the Hamiltonian path problem for digraphs (assumingNP co-NP).     

Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances

An analysis of the average-case complexity of solving random 3-Satisfiability (SAT) instances with backtrack algorithms is presented. We first interpret previous rigorous works in a unifying framework based on the statistical physics notions of dynamical trajectories, phase diagram and growth process. It is argued that, under the action of the Davis–Putnam–Loveland–Logemann (DPLL) algorithm, 3-SAT instances are turned into 2+p-SAT instances whose characteristic parameters (ratio of clauses per variable, fraction p of 3-clauses) can be followed during the operation, and define resolution trajectories. Depending on the location of trajectories in the phase diagram of the 2+p-SAT model, easy (polynomial) or hard (exponential) resolutions are generated. Three regimes are identified, depending on the ratio of the 3-SAT instance to be solved. Lower satisfiable (sat) phase: for small ratios, DPLL almost surely finds a solution in a time growing linearly with the number N of variables. Upper sat phase: for intermediate ratios, instances are almost surely satisfiable but finding a solution requires exponential time (2^Nω with ω>0) with high probability. Unsat phase: for large ratios, there is almost always no solution and proofs of refutation are exponential. An analysis of the growth of the search tree in both upper sat and unsat regimes is presented, and allows us to estimate ω as a function of . This analysis is based on an exact relationship between the average size of the search tree and the powers of the evolution operator encoding the elementary steps of the search heuristic.     

Geometric design of motions constrained by a contacting surface pair

We discuss the following problem which arises in robot motion planning, NC machining and computer animation: Given are a fixed surface Ψ and N positions Φ_i of a moving surface Φ such that the Φ_i are in point contact with Ψ. Compute a smooth and fair Euclidean gliding motion Φ(t) of the surface Φ on the surface Ψ which interpolates (or approximates) the given positions Φ_i at time instances t_i. First we generalize interpolatory variational subdivision algorithms for curves to curves on surfaces. Second we study an unconstraint motion design algorithm which we then extend to the main contribution of this paper, an algorithm for the design of a motion constraint by a contacting surface pair. Both motion design algorithms use a feature point representation of the moving surface, subdivision algorithms for curves, instantaneous kinematics, and ideas from line geometry. Geometric methods are used for the numerical solution of the arising optimization problems.     

一阶逻辑中约束求解的局部搜索法*

以一阶谓词逻辑为基础,讨论约束满足问题.着重研究一阶逻辑公式可满足性的局部搜索法,并与命题逻辑中的可满足性过程加以比较.以皇后问题和哈密顿回路问题为例,说明基于一阶逻辑的方法能处理较大的问题实例.     

Interval logics and their decision procedures : Part II: a real-time interval logic

In a companion paper, we presented an interval logic, and showed that it is elementarily decidable. In this paper we extend the logic to allow reasoning about real-time properties of concurrent systems; we call this logic real-time future interval logic (RTFIL). We model time by the real numbers, and allow our syntax to state the bounds on the duration of an interval. RTFIL possesses the “real-time interpolation property,” which appears to be the natural quantitative counterpart of invariance under finite stuttering. As the main result of this paper, we show that RTFIL is decidable; the decision algorithm is slightly more expensive than for the untimed logic. Our decidability proof is based on the reduction of the satisfiability problem for the logic to the emptiness problem for timed Büchi automata. The latter problem was shown decidable by Alur and Dill in a landmark paper, in which this real-time extension of ω-automata was introduced. Finally, we consider an extension of the logic that allows intervals to be constructed by means of “real-time offsets”, and show that even this simple extension renders the logic highly undecidable.     

Object recognition by combining paraperspective images

This paper provides a study on object recognition under paraperspective projection. Discussed is the problem of determining whether or not a given image was obtained from a 3-D object to be recognized. First it is clarified that paraperspective projection is the first-order approximation of perspective projection. Then it is shown that, if we represent an object as a set of its feature points and the object undergoes a rigid transformation or an affine transformation, any paraperspective image can be expressed as a linear combination of several appropriate paraperspective images: we need at least three images for rigid transformations; whereas we need at least two images for affine transformations. Particularly in the case of a rigid transformation, the coefficients of the combination have to satisfy two conditions: orthogonality and norm equality. A simple algorithm to solve the above problem based on these properties is presented: a linear, single-shot algorithm. Some experimental results with synthetic images and real images are also given.This work was done while the author was with ATR Auditory and Visual Perception Research Laboratories.Advanced Research Laboratory Hitachi, Ltd.     

Log-space constructible universal traversal sequences for cycles of length O(n4.03)

The paper presents a simple construction of polynomial length universal traversal sequences for cycles. These universal traversal sequences are log-space (even NC¹) constructible and are of length O(n^4.03). Our result improves the previously known upper-bound O(n^4.76) for log-space constructible universal traversal sequences for cycles.     

由一阶逻辑公式得到命题逻辑可满足性问题实例

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.     

基于成对约束的非线性维数约减框架

半监督维数约简是指借助于辅助信息与大量无标记样本信息从高维数据空间找到一个最优低维判别空间,便于后续的分类或聚类操作,它被看作是理解基因序列、文本与人脸图像等高维数据的有效方法。提出一个基于成对约束的半监督维数约简一般框架（SSPC）。该方法首先通过使用成对约束和无标号样本的内在几何结构学习一个判别邻接矩阵;其次,新方法应用学到的投影将原来高维空间中的数据映射到低维空间中,以至于聚类内的样本之间距离变得更加紧凑,而不同聚类间的样本之间距离变得尽可能得远。所提出的算法不仅能找到一个最佳的线性判别子空间,还可以揭示流形数据的非线性结构。在一些真实数据集上的实验结果表明,新方法的性能优于当前主流基于成对约束的维数约简算法的性能。     

Characterizations for functional dependency and Boyce-Codd normal form families

A functional dependency (fd) family was recently defined [20] as the set of all instances satisfying some set of functional dependencies. A Boyce-Codd normal form, abbreviated BCNF, family is defined here as an fd-family specified by some BCNF set of functional dependencies. The purpose of this paper is to present set-theoretic/algebraic characterizations relating to both types of families.Two characterizations of $\text{F}$($\text{I}$), the smallest fd-family containing the family $\text{I}$ of instances, are established. The first involves the notion of agreement, a concept related to that of a closed set of attributes. The second describes $\text{F}$($\text{I}$) as the smallest family of instances containing $\text{I}$ and closed under four specific operations on instances. Companion results are also given for BCNF- families.The remaining results concern characterizations involving the well-known operations of projection, join and union. Two characterizations for when the projection of an fd-family is again an fd-family are given. Several corollaries are obtained, including the effective decidability of whether a projection of an fd-family is an fd-family. The problem for BCNF-families disappears since it is shown that the projection of a BCNF-family is always a BCNF-family. Analogous to results for fd-families presented in [20], characterizations of when the join and union of BCNF-families are BCNF-families are given. Finally, the collections of all fd-families and all BCNF-families are characterized in terms of inverse projection operations and intersection.     

Computational complexity of some problems involving congruences on algebras

We prove that several problems concerning congruences on algebras are complete for nondeterministic log-space. These problems are: determining the congruence on a given algebra generated by a set of pairs, and determining whether a given algebra is simple or subdirectly irreducible. We also consider the problem of determining the smallest fully invariant congruence on a given algebra containing a given set of pairs. We prove that this problem is complete for nondeterministic polynomial time.     

Data reductions, fixed parameter tractability, and random weighted d-CNF satisfiability

Data reduction is a key technique in the study of fixed parameter algorithms. In the AI literature, pruning techniques based on simple and efficient-to-implement reduction rules also play a crucial role in the success of many industrial-strength solvers. Understanding the effectiveness and the applicability of data reduction as a technique for designing heuristics for intractable problems has been one of the main motivations in studying the phase transition of randomly-generated instances of NP-complete problems.In this paper, we take the initiative to study the power of data reductions in the context of random instances of a generic intractable parameterized problem, the weighted d-CNF satisfiability problem. We propose a non-trivial random model for the problem and study the probabilistic behavior of the random instances from the model. We design an algorithm based on data reduction and other algorithmic techniques and prove that the algorithm solves the random instances with high probability and in fixed-parameter polynomial time O(dknm) where n is the number of variables, m is the number of clauses, and k is the fixed parameter. We establish the exact threshold of the phase transition of the solution probability and show that in some region of the problem space, unsatisfiable random instances of the problem have parametric resolution proof of fixed-parameter polynomial size. Also discussed is a more general random model and the generalization of the results to the model.     

Manifold elastic net: a unified framework for sparse dimension reduction

It is difficult to find the optimal sparse solution of a manifold learning based dimensionality reduction algorithm. The lasso or the elastic net penalized manifold learning based dimensionality reduction is not directly a lasso penalized least square problem and thus the least angle regression (LARS) (Efron et al., Ann Stat 32(2):407–499, 2004), one of the most popular algorithms in sparse learning, cannot be applied. Therefore, most current approaches take indirect ways or have strict settings, which can be inconvenient for applications. In this paper, we proposed the manifold elastic net or MEN for short. MEN incorporates the merits of both the manifold learning based dimensionality reduction and the sparse learning based dimensionality reduction. By using a series of equivalent transformations, we show MEN is equivalent to the lasso penalized least square problem and thus LARS is adopted to obtain the optimal sparse solution of MEN. In particular, MEN has the following advantages for subsequent classification: (1) the local geometry of samples is well preserved for low dimensional data representation, (2) both the margin maximization and the classification error minimization are considered for sparse projection calculation, (3) the projection matrix of MEN improves the parsimony in computation, (4) the elastic net penalty reduces the over-fitting problem, and (5) the projection matrix of MEN can be interpreted psychologically and physiologically. Experimental evidence on face recognition over various popular datasets suggests that MEN is superior to top level dimensionality reduction algorithms.     

Simulated annealing — to cool or not

The optimization algorithm simulated annealing is considered. Presented is a class of problem instances and ‘neighbor selection’ matrices for which no monotone decreasing temperature sequence is optimal with respect to certain natural performance criteria. An algorithm called ‘threshold random search’ is introduced, and use is made of the fact that simulated annealing is a randomized version of threshold random search with deterministic thresholds.     

A GRASP×ELS for the vehicle routing problem with basic three-dimensional loading constraints

This paper addresses an extension of the capacitated vehicle routing problem where the client demand consists of three-dimensional weighted items (3L-CVRP). The objective is to design a set of trips for a homogeneous fleet of vehicles based at a depot node which minimizes the total transportation cost. Items in each vehicle trip must satisfy the three-dimensional orthogonal packing constraints. This problem is strongly connected to real-life transportation systems where the packing of items to be delivered by each vehicle can have a significant impact on the routes. We propose a new way to solve the packing sub-problem. It consists of a two-step procedure in which the z-constraints are first relaxed to get a (x,y) positioning of the items. Then, a compatible z-coordinate is computed to get a packing solution. Items can be rotated but additional constraints such as item fragility, support and LIFO are not considered. This method is included in a GRASP×ELS hybrid algorithm dedicated to the computation of VRP routes. The route optimization alternates between two search spaces: the space of VRP routes and the space of giant trips. The projection from one to the other is done by dedicated procedures (namely the Split and the concatenation algorithms). Moreover, a Local Search is defined on each search space. Furthermore, hash tables are used to store the result of the packing checks and thus save a substantial amount of CPU time. The effectiveness of our approach is illustrated by computational experiments on 3L-CVRP instances from the literature. A new set of realistic instances based on the 96 French districts are also proposed. They range from 19 nodes for the small instances to 255 nodes for the large instances and they can be stated as realistic since they are based on true travel distances in kilometers between French cities. The impact of the hash tables is illustrated as well.