An Improvement of Herbrands Theorem and Its Application to Model Generation Theorem Proving

This paper presents an improvement of Herbrand's theorem.We propose a method for specifying a sub- universe of the Herbrand universe of a clause set S for each argument of predicate symbols and function symbols in S. We prove that a clause set S is unsatisfiable if and only if there is a finite unsatisfiable set of ground instances of clauses of S that are derived by only instantiating each variable,which appears as an argument of predicate symbols or function symbols,in S over its corresponding argument's sub-universe of the Herbrand universe of S.Because such sub-universes are usually smaller(sometimes considerably)than the Herbrand universe of S,the number of ground instances may decrease considerably in many cases.We present an algorithm for automatically deriving the sub-universes for arguments in a given clause set,and show the correctness of our improvement.Moreover,we introduce an application of our approach to model generation theorem proving for non-range-restricted problems,show the range-restriction transformation algorithm based on our improvement and provide examples on benchmark problems to demonstrate the power of our approach.     

Generalized Moment Theorem and Its Application to Distributed-Parameter Control Systems

In this paper, we generalize the original moment theorem to the problem of existence of a linear operator with minimum norm under some constraint conditions in an abstract normed space. The results are applied to a class of largest controllable set and optimal control problems for distributed parameter systems.     

A characterization of answer sets for logic programs

Checking if a program has an answer set, and if so, compute its answer sets are just some of the important problems in answer set logic programming. Solving these problems using Gelfond and Lifschitz's original definition of answer sets is not an easy task. Alternative characterizations of answer sets for nested logic pro- grams by Erdem and Lifschitz, Lee and Lifschitz, and You et al. are based on the completion semantics and various notions of tightness. However, the notion of tightness is a local notion in the sense that for different answer sets there are, in general, different level mappings capturing their tightness. This makes it hard to be used in the design of algorithms for computing answer sets. This paper proposes a characterization of answer sets based on sets of generating rules. From this char- acterization new algorithms are derived for computing answer sets and for per- forming some other reasoning tasks. As an application of the characterization a sufficient and necessary condition for the equivalence between answer set seman- tics and completion semantics has been proven, and a basic theorem is shown on computing answer sets for nested logic programs based on an extended notion of loop formulas. These results on tightness and loop formulas are more general than that in You and Lin's work.     

Design and Performance Evaluation of Sequence Partition Algorithms

Tradeoffs between time complexities and solution optimalities are important when selecting algorithms for an NP-hard problem in different applications. Also, the distinction between theoretical upper bound and actual solution optimality for realistic instances of an NP-hard problem is a factor in selecting algorithms in practice. We consider the problem of partitioning a sequence of n distinct numbers into minimum number of monotone （increasing or decreasing） subsequences. This problem is NP-hard and the number of monotone subsequences can reach [√2n＋1/1-1/2]in the worst case. We introduce a new algorithm, the modified version of the Yehuda-Fogel algorithm, that computes a solution of no more than [√2n＋1/1-1/2]monotone subsequences in O（n^1.5） time. Then we perform a comparative experimental study on three algorithms, a known approximation algorithm of approximation ratio 1.71 and time complexity O（n^3）, a known greedy algorithm of time complexity O（n^1.5 log n）, and our new modified Yehuda-Fogel algorithm. Our results show that the solutions computed by the greedy algorithm and the modified Yehuda-Fogel algorithm are close to that computed by the approximation algorithm even though the theoretical worst-case error bounds of these two algorithms are not proved to be within a constant time of the optimal solution. Our study indicates that for practical use the greedy algorithm and the modified Yehuda-Fogel algorithm can be good choices if the running time is a major concern.     

Satisfiability with Index Dependency

We study the Boolean satisfiability problem (SAT) restricted on input formulas for which there are linear arithmetic constraints imposed on the indices of variables occurring in the same clause.This can be seen as a structural counterpart of Schaefer’s dichotomy theorem which studies the SAT problem with additional constraints on the assigned values of variables in the same clause.More precisely,let k-SAT(m,A) denote the SAT problem restricted on instances of k-CNF formulas,in every clause of which the indices of the last k m variables are totally decided by the first m ones through some linear equations chosen from A.For example,if A contains i3 = i1 + 2i2 and i4 = i2 i1 + 1,then a clause of the input to 4-SAT(2,A) has the form yi1 ∨ yi2 ∨ yi1+2i2 ∨ yi2 i1+1,with yi being xi or xi.We obtain the following results: 1) If m 2,then for any set A of linear constraints,the restricted problem k-SAT(m,A) is either in P or NP-complete assuming P = NP.Moreover,the corresponding #SAT problem is always #P-complete,and the Max-SAT problem does not allow a polynomial time approximation scheme assuming P = NP.2) m = 1,that is,in every clause only one index can be chosen freely.In this case,we develop a general framework together with some techniques for designing polynomial-time algorithms for the restricted SAT problems.Using these,we prove that for any A,#2-SAT(1,A) and Max-2-SAT(1,A) are both polynomial-time solvable,which is in sharp contrast with the hardness results of general #2-SAT and Max-2-SAT.For fixed k 3,we obtain a large class of non-trivial constraints A,under which the problems k-SAT(1,A),#k-SAT(1,A) and Max-k-SAT(1,A) can all be solved in polynomial time or quasi-polynomial time.     

Analysis of nonlinear electrical circuits using bernstein polynomials

In electrical circuit analysis, it is often necessary to find the set of all direct current (d.c.) operating points (either voltages or currents) of nonlinear circuits. In general, these nonlinear equations are often represented as polynomial systems. In this paper, we address the problem of finding the solutions of nonlinear electrical circuits, which are modeled as systems of n polynomial equations contained in an n-dimensional box. Branch and Bound algorithms based on interval methods can give guaranteed enclosures for the solution. However, because of repeated evaluations of the function values, these methods tend to become slower. Branch and Bound algorithm based on Bernstein coefficients can be used to solve the systems of polynomial equations. This avoids the repeated evaluation of function values, but maintains more or less the same number of iterations as that of interval branch and bound methods. We propose an algorithm for obtaining the solution of polynomial systems, which includes a pruning step using Bernstein Krawczyk operator and a Bernstein Coefficient Contraction algorithm to obtain Bernstein coefficients of the new domain. We solved three circuit analysis problems using our proposed algorithm. We compared the performance of our proposed algorithm with INTLAB based solver and found that our proposed algorithm is more efficient and fast.     

Improved method to generate path-wise test data

Gupta et al.,propsed a method ,which is referred to as the Iterative Relaxation Method ,to generate test data for a given path in a program by linearizing the predicate functions.In this paper,a model language is presented and the properties of static and dynamic data depen-dencies are investigated ,The notions in the Interative Relaxation Method are defined formally.The predicate slice proposed by Gupta et al.is extended to path-wise static slice.The correctness of the constructional algorithm is proved afterward The improvement shows that the constructions of predicate slice and input dependency set can be omitted .The equivalence of systems of constraints generated by both methods is proved ,The prototype of path-wise test data generator is presented in this paper,The experiments show shat our method is practical ,and fits the path-wise automatic generation of test data for both whicte -bos testing and black-blx testing.     

Penalty Formulations and Trap-Avoidance Strategies for Solving Hard Satisfiability Problems

In this paper we study the solution of SAT problems formulated as discrete decision and discrete constrained optimization problems. Constrained formulations are better than traditional unconstrained formulations because violated constraints may provide additional forces to lead a search towards a satisfiable assignment. We summarize the theory of extended saddle points in penalty formulations for solving discrete constrained optimization problems and the associated discrete penalty method (DPM). We then examine various formulations of the objective function, choices of neighborhood in DPM, strategies for updating penalties, and heuristics for avoiding traps. Experimental evaluations on hard benchmark instances pinpoint that traps contribute significantly to the inefficiency of DPM and force a trajectory to repeatedly visit the same set of or nearby points in the original variable space. To address this issue, we propose and study two trap-avoidance strategies. The first strategy adds extra penalties on unsatisfied clauses inside a trap, leading to very large penalties for unsatisfied clauses that are trapped more often and making these clauses more likely to be satisfied in the future. The second strategy stores information on points visited before, whether inside traps or not, and avoids visiting points that are close to points visited before. It can be implemented by modifying the penalty function in such a way that, if a trajectory gets close to points visited before, an extra penalty will take effect and force the trajectory to a new region. It specializes to the first strategy because traps are special cases of points visited before. Finally, we show experimental results on evaluating benchmarks in the DIMACS and SATLIB archives and compare our results with existing results on GSAT, WalkSAT, LSDL, and Grasp. The results demonstrate that DPM with trap avoidance is robust as well as effective for solving hard SAT problems.     

A fast successive over-relaxation algorithm for force-directed network graph drawing

Force-directed approach is one of the most widely used methods in graph drawing research. There are two main problems with the traditional force-directed algorithms. First, there is no mature theory to ensure the convergence of iteration sequence used in the algorithm and further, it is hard to estimate the rate of convergence even if the convergence is satisfied. Second, the running time cost is increased intolerablely in drawing largescale graphs, and therefore the advantages of the force-directed approach are limited in practice. This paper is focused on these problems and presents a sufficient condition for ensuring the convergence of iterations. We then develop a practical heuristic algorithm for speeding up the iteration in force-directed approach using a successive over-relaxation (SOR) strategy. The results of computational tests on the several benchmark graph datasets used widely in graph drawing research show that our algorithm can dramatically improve the performance of force-directed approach by decreasing both the number of iterations and running time, and is 1.5 times faster than the latter on average.     

Energy Efficiency of a Multi-Core Processor by Tag Reduction

We consider the energy saving problem for caches on a multi-core processor.In the previous research on low power processors,there are various methods to reduce power dissipation.Tag reduction is one of them.This paper extends the tag reduction technique on a single-core processor to a multi-core processor and investigates the potential of energy saving for multi-core processors.We formulate our approach as an equivalent problem which is to find an assignment of the whole instruction pages in the physical memory to a set of cores such that the tag-reduction conflicts for each core can be mostly avoided or reduced.We then propose three algorithms using different heuristics for this assignment problem.We provide convincing experimental results by collecting experimental data from a real operating system instead of the traditional way using a processor simulator that cannot simulate operating system functions and the full memory hierarchy.Experimental results show that our proposed algorithms can save total energy up to 83.93% on an 8-core processor and 76.16% on a 4-core processor in average compared to the one that the tag-reduction is not used for.They also significantly outperform the tag reduction based algorithm on a single-core processor.     

Fault Diagnosis Based on MultiKernel Classification and Information Fusion Decision

In machine learning and statistics, classification is the a new observation belongs, on the basis of a training set of data problem of identifying to which of a set of categories （sub-populations） containing observations （or instances） whose category membership is known. SVM （support vector machines） are supervised learning models with associated learning algorithms that analyze data and recognize patterns, used for classification and regression analysis. The basic SVM takes a set of input data and predicts, for each given input, which of two possible classes fon~as the output, making it a non-probabilistic binary linear classifier. In pattern recognition problem, the selection of the features used for characterization an object to be classified is importance. Kernel methods are algorithms that, by replacing the inner product with an appropriate positive definite function, impticitly perform a nonlinear mapping 4~ of the input data in Rainto a high-dimensional feature space H. Cover＇s theorem states that if the transformation is nonlinear and the dimensionality of the feature space is high enough, then the input space may be transformed into a new feature space where the patterns are linearly separable with high probability.     

A self-adaptive linear evolutionary algorithm for solving constrained optimization problems

In many real-world applications of evolutionary algorithms, the fitness of an individual requires a quantitative measure. This paper proposes a self-adaptive linear evolutionary algorithm (ALEA) in which we introduce a novel strategy for evaluating individual’s relative strengths and weaknesses. Based on this strategy, searching space of constrained optimization problems with high dimensions for design variables is compressed into two-dimensional performance space in which it is possible to quickly identify ‘good’ individuals of the performance for a multiobjective optimization application, regardless of original space complexity. This is considered as our main contribution. In addition, the proposed new evolutionary algorithm combines two basic operators with modification in reproduction phase, namely, crossover and mutation. Simulation results over a comprehensive set of benchmark functions show that the proposed strategy is feasible and effective, and provides good performance in terms of uniformity and diversity of solutions.     

受约束时滞系统的抗饱和补偿器增益设计

Systems that are subject to both time-delay in state and input saturation are considered.We synthesize the anti-windup gain to enlarge the estimation of domain of attraction while guaran-teeing the stability of the closed-loop system. An ellipsoid and a polyhedral set are used to bound the state of the system, which make a new sector condition valid. Other than an iterative algorithm, a direct designing algorithm is derived to compute the anti-windup compensator gain, which reduces the conservatism greatly. We analyze the delay-independent and delay-dependent cases, respectively. Finally, an optimization algorithm in the form of LMIs is constructed to compute the compensator gain which maximizes the estimation of domain of attraction. Numerical examples are presented to demonstrate the effectiveness of our approach.     

Eliminating redundant search space on backtracking for forward chaining theorem proving

This paper introduces some improvements on the intelligent backtracking strategy for forward chaining theorem proving. How to decide a minimal useful consequent atom set for a refutation derived at a node in a proof tree is discussed. In most cases, an unnecessary non-Horn clause used for forward chaining will be split only once. The increase of the search space by invoking unnecessary forward chaining clauses will be nearly linear, not exponential anymore.In this paper, the principle of the proposed method and its correctness are introduced. Moreover,some examples are provided to show that the proposed approach is powerful for forward chaining theorem proving.     

On Isomorphism Testing of Groups with Normal Hall Subgroups

A normal Hall subgroup N of a group G is a normal subgroup with its order coprime with its index.SchurZassenhaus theorem states that every normal Hall subgroup has a complement subgroup,that is a set of coset representatives H which also forms a subgroup of G.In this paper,we present a framework to test isomorphism of groups with at least one normal Hall subgroup,when groups are given as multiplication tables.To establish the framework,we first observe that a proof of Schur-Zassenhaus theorem is constructive,and formulate a necessary and sufficient condition for testing isomorphism in terms of the associated actions of the semidirect products,and isomorphisms of the normal parts and complement parts.We then focus on the case when the normal subgroup is abelian.Utilizing basic facts of representation theory of finite groups and a technique by Le Gall (STACS 2009),we first get an efficient isomorphism testing algorithm when the complement has bounded number of generators.For the case when the complement subgroup is elementary abelian,which does not necessarily have bounded number of generators,we obtain a polynomial time isomorphism testing algorithm by reducing to generalized code isomorphism problem,which asks whether two linear subspaces are the same up to permutation of coordinates.A solution to the latter can be obtained by a mild extension of the singly exponential (in the number of coordinates) time algorithm for code isomorphism problem developed recently by Babai et al.(SODA 2011).Enroute to obtaining the above reduction,we study the following computational problem in representation theory of finite groups: given two representations ρ and τ of a group H over Zpd,p a prime,determine if there exists an automorphism φ : H → H ,such that the induced representation ρφ = ρφ and τ are equivalent,in time poly(|H |,pd).     

A programmable approach to maintenance of a finite knowledge base

In this paper,we present a programmable method of revising a finite clause set.We first present a procedure whose formal parameters are a consistent clause set Γand a clause A and whose output is a set of minimal subsets of Γwhich are inconsistent with A.The maximal consistent subsets can be generated from all minimal inconsistent subsets.We develop a prototype system based on the above procedure,and discuss the implementation of knowledge base maintenance.At last,we compare the approach presented in this paper with other related approaches,The main characteristic of the approach is that it can be implemented by a computer program.     

Complexities of Homomorphism and Isomorphism for Definite Logic Programs

A homomorphism (?) of logic programs from P to P' is a function mapping Atoms(P) to Atoms(P') and it preserves complements and program clauses. For each definite program clause a←a1,...,an∈P it implies that (?)(a)←(?)(a1),...,(?)(an) is a program clause of P'. A homomorphism (?) is an isomorphism if (?) is a bijection. In this paper, the complexity of the decision problems on homomorphism and isomorphism for definite logic programs is studied. It is shown that the homomorphism problem (HOM-LP) for definite logic programs is NP-complete, and the isomorphism problem (ISO-LP) is equivalent to the graph isomorphism problem (GI).     

Exact Computation of the Topology and Geometric Invariants of the Voronoi Diagram of Spheres in 3D

In this paper, we are addressing the exact computation of the Delaunay graph (or quasi-triangulation) and the Voronoi diagram of spheres using Wu’s algorithm. Our main contributions are first a methodology for automated derivation of invariants of the Delaunay empty circumsphere predicate for spheres and the Voronoi vertex of four spheres, then the application of this methodology to get all geometrical invariants that intervene in this problem and the exact computation of the Delaunay graph and the Voronoi diagram of spheres. To the best of our knowledge, there does not exist a comprehensive treatment of the exact computation with geometrical invariants of the Delaunay graph and the Voronoi diagram of spheres. Starting from the system of equations defining the zero-dimensional algebraic set of the problem, we are applying Wu’s algorithm to transform the initial system into an equivalent Wu characteristic (triangular) set. In the corresponding system of algebraic equations, in each polynomial (except the first one), the variable with higher order from the preceding polynomial has been eliminated (by pseudo-remainder computations) and the last polynomial we obtain is a polynomial of a single variable. By regrouping all the formal coefficients for each monomial in each polynomial, we get polynomials that are invariants for the given problem. We rewrite the original system by replacing the invariant polynomials by new formal coefficients. We repeat the process until all the algebraic relationships (syzygies) between the invariants have been found by applying Wu’s algorithm on the invariants. Finally, we present an incremental algorithm for the construction of Voronoi diagrams and Delaunay graphs of spheres in 3D and its application to Geodesy.