Extension and equivalence problems for clause minimal formulae

Inspired by the notion of minimal unsatisfiable formulae we first introduce and study the class of clause minimal formulae. A CNF formula F is said to be clause minimal if any proper subformula of F is not equivalent to F. We investigate the equivalence and extension problems for clause minimal formulae. The extension problem is the question whether for two formulae F and H there is some formula G such that F + G is equivalent to H. Generally, we show that these problems are intractable. Then we discuss the complexity of these problems restricted by various parameters and constraints. In the last section we ask several open questions in this area.     

DNA-based algorithms for learning Boolean formulae

We apply a DNA-based massively parallel exhaustive search to solving the computational learning problems of DNF (disjunctive normal form) Boolean formulae. Learning DNF formulae from examples is one of the most important open problems in computational learning theory and the problem of learning 3-term DNF formulae is known as intractable if RP NP. We propose new methods to encode any k-term DNF formula to a DNA strand, evaluate the encoded DNF formula for a truth-value assignment by using hybridization and primer extension with DNA polymerase, and find a consistent DNF formula with the given examples. By employing these methods, we show that the class of k-term DNF formulae (for any constant k) and the class of general DNF formulae are efficiently learnable on DNA computer.Second, in order for the DNA-based learning algorithm to be robust for errors in the data, we implement the weighted majority algorithm on DNA computers, called DNA-based majority algorithm via amplification (DNAMA), which take a strategy of ``amplifying' the consistent (correct) DNA strands. We show a theoretical analysis for the mistake bound of the DNA-based majority algorithm via amplification, and imply that the amplification to ``double the volumes' of the correct DNA strands in the test tube works well.     

一类可分离SAT问题的O(1.890n)精确算法

布尔可满足性问题（SAT）是指对于给定的布尔公式,是否存在一个可满足的真值指派.这是第1个被证明的NP完全问题,一般认为不存在多项式时间算法,除非P=NP.学者们大都研究了子句长度不超过k的SAT问题（k-SAT）,从全局搜索到局部搜索,给出了大量的相对有效算法,包括随机算法和确定算法.目前,最好算法的时间复杂度不超过O（（2-2/k）ⁿ）,当k=3时,最好算法时间复杂度为O（1.308ⁿ）.而对于更一般的与子句长度k无关的SAT问题,很少有文献涉及.引入了一类可分离SAT问题,即3-正则可分离可满足性问题（3-RSSAT）,证明了3-RSSAT是NP完全问题,给出了一般SAT问题3-正则可分离性的O（1.890ⁿ）判定算法.然后,利用矩阵相乘算法的研究成果,给出了3-RSSAT问题的O（1.890ⁿ）精确算法,该算法与子句长度无关.     

Minimal proper interval completions

Given an arbitrary graph G=(V,E) and a proper interval graph H=(V,F) with E⊆F we say that H is a proper interval completion of G. The graph H is called a minimal proper interval completion of G if, for any sandwich graph H^′=(V,F^′) with E⊆F^′⊂F, H^′ is not a proper interval graph. In this paper we give a O(n+m) time algorithm computing a minimal proper interval completion of an arbitrary graph. The output is a proper interval model of the completion.     

Simplification in a satisfiability checker for VLSI applications

INSTEP is a satisfiability checker designed for the original purpose of solving a specific target set of problems in the formal verification of VLSI circuits. These are real-world problems concerning a sequential circuit that is part of a commercial chip manufactured by Texas Instruments. The program has succeeded in solving these problems, which require satisfiability checking for combinational representations containing up to around 10 000 variables and a graphical representation of around 17 000 nodes. It has also been successfully applied to a number of standard benchmark problems in combinational circuit verification. Results on these benchmarks are overall competitive with those for the widely used method based onbinary decision diagrams, and for the first time demonstrate the solution in polynomial time of certain benchmarks involving combinational multipliers.A central part of the INSTEP algorthim is simplification. Most simplifications that take place in previous tautology checkers consist of the replacement of a formula by a shorter formula that is logically equivalent. Most simplifications in INSTEP replace a formula by another formula which isnot logically equivalent, but such that satisfiability is nevertheless preserved. These new simplifications depend on the pattern of occurrence of one or more variables and particularly on theirpolarity.The simplifications used by INSTEP rest on several new theorems in an area of propositional calculus (or Boolean algebra) which is crucial to the general theory of effective simplification of propositional formulas. The primary purpose of the present paper is to demonstrate these theorems and explain the simplifications that depend on them.For the present paper we have tried INSTEP on the well-known pigeonhole problem. So far as we know INSTEP is the first implemented program to produce proofs of polynomial length for pigeonhole problems. It also produces these proofs in polynomial time.     

H∞ sampled-data synthesis and related numerical issues

In this paper we present a new, compact derivation of state-space formulae for the so-called discretisation-based solution of the H_∞ sampled-data control problem. Our approach is based on the established technique of continuous time-lifting, which is used to isometrically map the continuous-time, linear, periodically time-varying, sampled-data problem to a discretetime, linear, time-invariant problem. State-space formulae are derived for the equivalent, discrete-time problem by solving a set of two-point, boundary-value problems. The formulae accommodate a direct feed-through term from the disturbance inputs to the controlled outputs of the original plant and are simple, requiring the computation of only a single matrix exponential. It is also shown that the resultant formulae can be easily re-structured to give a numerically robust algorithm for computing the state-space matrices.     

Redundancy in logic II: 2CNF and Horn propositional formulae

We report results about the redundancy of formulae in 2CNF form. In particular, we give a slight improvement over the trivial redundancy algorithm and give some complexity results about some problems related to finding Irredundant Equivalent Subsets (i.e.s.) of 2CNF formulae. The problems of checking whether a 2CNF formula has a unique i.e.s. and checking whether a clause in is all its i.e.s.'s are polynomial. Checking whether a 2CNF formula has an i.e.s. of a given size and checking whether a clause is in some i.e.s.'s of a 2CNF formula are polynomial or NP-complete depending on whether the formula is cyclic. Some results about Horn formulae are also reported.     

A zero compensation approach to singular H2 and H∞ problems

In this work we analyse singular H² and H^∞ problems for which the usual Riccati equations become ill-posed owing to the existence of plant zeros at infinity. We adopt a two-step approach to the analysis. First we replace the usual Riccati equations with two generalized eigenproblems; these problems are always well-posed. Next we extract those structural elements which pertain to the troublesome plant zeros. We do this by introducing pre-compensators which cancel the offending zeros. In so doing, we temporarily relax the controller properness constraint that is traditionally imposed in H² and H^∞ problems by allowing pole-zero cancellations between the plant and controller at infinity. Since no significant added complexity of analysis results, we also treat the case of singularity due to finite jω-axis plant zeros by relaxing the internal stability requirement and allowing finite jω-axis pole-zero cancellations. The resultant theory allows us to specify necessary and sufficient conditions for the existence of solutions to singular H² and H^∞ problems. The existence conditions and the resultant control laws are expressed directly in terms of the eigenvalues and eigenvectors of two Hamiltonian matrices associated with the problem. The theory also gives some insight into the character of the subset of all proper, internally stabilizing solutions, including whether this set is nonempty. An example is included.     

All-pairs shortest paths and the essential subgraph

The essential subgraph H of a weighted graph or digraphG contains an edge (v, w) if that edge is uniquely the least-cost path between its vertices. Let s denote the number of edges ofH. This paper presents an algorithm for solving all-pairs shortest paths onG that requires O(ns+n² logn) worst-case running time. In general the time is equivalent to that of solvingn single-source problems using only edges inH. For general models of random graphs and digraphsG, s=0(n logn) almost surely. The subgraphH is optimal in the sense that it is the smallest subgraph sufficient for solving shortest-path problems inG. Lower bounds on the largest-cost edge ofH and on the diameter ofH andG are obtained for general randomly weighted graphs. Experimental results produce some new conjectures about essential subgraphs and distances in graphs with uniform edge costs.Much of this research was carried out while the author was a Visiting Fellow at the Center for Discrete Mathematics and Theoretical Computer Science (DIMACS).