Efficient recognition of trace languages defined by repeat-until loops

A sequence of operations may be validly reordered, provided that only pairs of independent operations are commuted. Focusing on a program scheme, idealized as a local finite automaton, we consider the problem of checking whether a given string is a valid permutation of a word recognized by the automaton. Within the framework of trace theory, this is the membership problem for rational trace languages. Existing general algorithms, although time-polynomial, have unbounded degree related to some properties of the dependence graph. Here we present two original linear-time solutions. A straightforward algorithm is suitable for any finite automaton such that all the transitions starting from the same state are labelled by dependent symbols. The second approach is currently restricted to automata representing programs of nested repeat-until loops. Using integer compositions to represent loop iterations and under suitable conditions, the algorithm constructs the syntax tree of a possible word equivalent to the input string. The same procedures show that, under our hypotheses, the uniform version of the membership problem (which is NP-complete in the general case) is solvable in polynomial time.     

Buyer-supplier games: Optimization over the core

In a buyer-supplier game, a special type of assignment game, a distinguished player, called the buyer, wishes to purchase some combinatorial structure. A set of players, called suppliers, offer various components of the structure for sale. Any combinatorial minimization problem can be transformed into a buyer-supplier game. While most previous work has been concerned with characterizing the core of buyer-supplier games, in this paper we study optimization over the set of core vectors. We give a polynomial time algorithm for optimizing over the core of any buyer-supplier game for which the underlying minimization problem is solvable in polynomial time. In addition, we show that it is hard to determine whether a given vector belongs to the core if the base minimization problem is not solvable in polynomial time. Finally, we introduce and study the concept of focus point price, which answers the question: If we are constrained to play in equilibrium, how much can we lose by playing the wrong equilibrium?     

Quantitatively fair scheduling

We consider finite graphs whose edges are labeled with elements, called colors, taken from a fixed finite alphabet. We study the problem of determining whether there is an infinite path where either (i) all colors occur with a fixed asymptotic frequency, or (ii) there is a constant that bounds the difference between the occurrences of any two colors for all prefixes of the path. These properties can be viewed as quantitative refinements of the classical notion of fair path in a concurrent system, whose simplest form checks whether all colors occur infinitely often. Our notions provide stronger criteria, particularly suitable for scheduling applications based on a coarse-grained model of the jobs involved. In particular, they enforce a given set of priorities among the jobs involved in the system. We show that both problems we address are solvable in polynomial time, by reducing them to the feasibility of a linear program. We also consider two-player games played on finite colored graphs where the goal is one of the above frequency-related properties. For all the goals, we show that the problem of checking whether there exists a winning strategy is Co-NP-complete.     

Exact satisfiability,a natural extension of set partition,and its average case behavior

The problem of determining whether a Boolean formula in conjunctive normal form is satisfiable in such a way that in each clause exactly one literal is set true, and all the other literals are set false is called the exact satisfiability problem. The exact satisfiability problem is well known to be NP-complete [5] and it contains the well known set partitioning problem as a special case. We study here the average time complexity of a simple backtracking strategy for solving the exact satisfiability problem under two probability models, the constant density model and the constant degree model. For both models we present results sharply separating classes of instances solvable in low degree polynomial time in the average from classes for which superpolynomial or exponential time is needed in the average.     

On a decision procedure for quantified linear programs

Quantified linear programming is the problem of checking whether a polyhedron specified by a linear system of inequalities is non-empty, with respect to a specified quantifier string. Quantified linear programming subsumes traditional linear programming, since in traditional linear programming, all the program variables are existentially quantified (implicitly), whereas, in quantified linear programming, a program variable may be existentially quantified or universally quantified over a continuous range. In this paper, the term linear programming is used to describe the problem of checking whether a system of linear inequalities has a feasible solution. On account of the alternation of quantifiers in the specification of a quantified linear program (QLP), this problem is non-trivial. QLPs represent a class of declarative constraint logic programs (CLPs) that are extremely rich in their expressive power. The complexity of quantified linear programming for arbitrary constraint matrices is unknown. In this paper, we show that polynomial time decision procedures exist for the case in which the constraint matrix satisfies certain structural properties. We also provide a taxonomy of quantified linear programs, based on the structure of the quantifier string and discuss the computational complexities of the constituent classes. This research has been supported in part by the Air Force Office of Scientific Research under contract FA9550-06-1-0050.     

Scalable satisfiability checking and test data generation from modeling diagrams

We explore the automatic generation of test data that respect constraints expressed in the Object-Role Modeling (ORM) language. ORM is a popular conceptual modeling language, primarily targeting database applications, with significant uses in practice. The general problem of even checking whether an ORM diagram is satisfiable is quite hard: restricted forms are easily NP-hard and the problem is undecidable for some expressive formulations of ORM. Brute-force mapping to input for constraint and SAT solvers does not scale: state-of-the-art solvers fail to find data to satisfy uniqueness and mandatory constraints in realistic time even for small examples. We instead define a restricted subset of ORM that allows efficient reasoning yet contains most constraints overwhelmingly used in practice. We show that the problem of deciding whether these constraints are consistent (i.e., whether we can generate appropriate test data) is solvable in polynomial time, and we produce a highly efficient (interactive speed) checker. Additionally, we analyze over 160 ORM diagrams that capture data models from industrial practice and demonstrate that our subset of ORM is expressive enough to handle their vast majority.     

On the implication problem for probabilistic conditionalindependency

The implication problem is to test whether a given set of independencies logically implies another independency. This problem is crucial in the design of a probabilistic reasoning system. We advocate that Bayesian networks are a generalization of standard relational databases. On the contrary, it has been suggested that Bayesian networks are different from the relational databases because the implication problem of these two systems does not coincide for some classes of probabilistic independencies. This remark, however, does not take into consideration one important issue, namely, the solvability of the implication problem. In this comprehensive study of the implication problem for probabilistic conditional independencies, it is emphasized that Bayesian networks and relational databases coincide on solvable classes of independencies. The present study suggests that the implication problem for these two closely related systems differs only in unsolvable classes of independencies. This means there is no real difference between Bayesian networks and relational databases, in the sense that only solvable classes of independencies are useful in the design and implementation of these knowledge systems. More importantly, perhaps, these results suggest that many current attempts to generalize Bayesian networks can take full advantage of the generalizations made to standard relational databases     

Finding the longest common nonsuperstring in linear time

String inclusion and non-inclusion problems have been vigorously studied in such diverse fields as molecular biology, data compression, and computer security. Among the well-known string inclusion or non-inclusion notions, we are interested in the longest common nonsuperstring. Given a set of strings, the longest common nonsuperstring problem is finding the longest string that is not a superstring of any string in the given set. It is known that the longest common nonsuperstring problem is solvable in polynomial time.In this paper, we propose an efficient algorithm for the longest common nonsuperstring problem. The running time of our algorithm is linear with respect to the sum of the lengths of the strings in the given set, using generalized suffix trees.     

Equivalence of propositional Prolog programs

We show that the equivalence problem for propositional Prolog programs is coNP-complete. Considering yes-no answers only the modified equivalence problem is solvable in polynomial time. Furthermore, the problem whether a program does not terminate for some question is NP-complete. For a fixed question the loop problem can be decided in linear time.The work of this author was supported by the Studienstiftung des Deutschen Volkes.     

The complexity of propositional implication

The question whether a set of formulae Γ implies a formula φ is fundamental. The present paper studies the complexity of the above implication problem for propositional formulae that are built from a systematically restricted set of Boolean connectives. We give a complete complexity-theoretic classification for all sets of Boolean functions in the meaning of Post's lattice and show that the implication problem is efficiently solvable only if the connectives are definable using the constants {0,1} and only one of {∧,∨,⊕}. The problem remains coNP-complete in all other cases. We also consider the restriction of Γ to singletons which makes the problem strictly easier in some cases.     

Random walks for selected boolean implication and equivalence problems

This paper is concerned with the design and analysis of a random walk algorithm for the 2CNF implication problem (2CNFI). In 2CNFI, we are given two 2CNF formulas f₁{\phi_{1}} and f₂{\phi_{2}} and the goal is to determine whether every assignment that satisfies f₁{\phi_{1}} , also satisfies f₂{\phi_{2}} . The implication problem is clearly coNP-complete for instances of kCNF, k ≥ 3; however, it can be solved in polynomial time, when k ≤ 2. The goal of this paper is to provide a Monte Carlo algorithm for 2CNFI with a bounded probability of error. The technique developed for 2CNFI is then extended to derive a randomized, polynomial time algorithm for the problem of checking whether a given 2CNF formula Nae-implies another 2CNF formula.     

Reachability of Patterned Conditional Pushdown Systems

Conditional pushdown systems (CPDSs) extend pushdown systems by associating each transition rule with a regular language over the stack alphabet. The goal is to model program verification problems that need to examine the runtime call stack of programs. Examples include security property checking of programs with stack inspection, compatibility checking of HTML5 parser specifications, etc. Esparza et al. proved that the reachability problem of CPDSs is EXPTIME-complete, which prevents the existence of an algorithm tractable for all instances in general. Driven by the practical applications of CPDSs, we study the reachability of patterned CPDS (pCPDS) that is a practically important subclass of CPDS, in which each transition rule carries a regular expression obeying certain patterns. First, we present new saturation algorithms for solving state and configuration reachability of pCPDSs. The algorithms exhibit the exponential-time complexity in the size of atomic patterns in the worst case. Next, we show that the reachability of pCPDSs carrying simple patterns is solvable in fixed-parameter polynomial time and space. This answers the question on whether there exist tractable reachability analysis algorithms of CPDSs tailored for those practical instances that admit efficient solutions such as stack inspection without exception handling. We have evaluated the proposed approach, and our experiments show that the pattern-driven algorithm steadily scales on pCPDSs with simple patterns.

     

Optimal register allocation for SSA-form programs in polynomial time

This paper gives a constructive proof that the register allocation problem for a uniform register set is solvable in polynomial time for SSA-form programs.     

Unshuffling a square is NP-hard

A shuffle of two strings is formed by interleaving the characters into a new string, keeping the characters of each string in order. A string is a square if it is a shuffle of two identical strings. There is a known polynomial time dynamic programming algorithm to determine if a given string z is the shuffle of two given strings x, y; however, it has been an open question whether there is a polynomial time algorithm to determine if a given string z is a square. We resolve this by proving that this problem is NP-complete via a many-one reduction from 3-Partition.     

Algorithms for tractable compliance problems

In general the problem of verifying whether a structured business process is compliant with a given set of regulations is NP-hard. The present paper focuses on identifying a tractable subset of this problem, namely verifying whether a structured business process is compliant with a single global obligation. Global obligations are those whose validity spans for the entire execution of a business process. We identify two types of obligations: achievement and maintenance.In the present paper we firstly define an abstract framework capable to model the problem and secondly we define procedures and algorithms to deal with the compliance problem of checking the compliance of a structured business process with respect to a single global obligation. We show that the algorithms proposed in the paper run in polynomial time.     

Discovering Network Topology in the Presence of Byzantine Faults

We pose and study the problem of Byzantine-robust topology discovery in an arbitrary asynchronous network. The problem is an abstraction of fault-tolerant routing. We formally state the weak and strong versions of the problem. The weak version requires that either each node discovers the topology of the network or at least one node detects the presence of a faulty node. The strong version requires that each node discovers the topology regardless of faults. We focus on noncryptographic solutions to these problems. We explore their bounds. We prove that the weak topology discovery problem is solvable only if the connectivity of the network exceeds the number of faults in the system. Similarly, we show that the strong version of the problem is solvable only if the network connectivity is more than twice the number of faults. We present solutions to both versions of the problem. The presented algorithms match the established graph connectivity bounds. The algorithms do not require the individual nodes to know either the diameter or the size of the network. The message complexity of both programs is low polynomial with respect to the network size. We describe how our solutions can be extended to add the property of termination, handle topology changes, and perform neighborhood discovery.     

Preemptive open shop scheduling with multiprocessors: polynomial cases and applications

This paper addresses a multiprocessor generalization of the preemptive open-shop scheduling problem. The set of processors is partitioned into two groups and the operations of the jobs may require either single processors in either group or simultaneously all processors from the same group. We consider two variants depending on whether preemptions are allowed at any fractional time points or only at integer time points. We reduce the former problem to solving a linear program in strongly polynomial time, while a restricted version of the second problem is solved by rounding techniques. Applications to course scheduling and hypergraph edge coloring are also discussed.     

Generalized approximate regularities in strings

We concentrate on generalized string regularities and study the minimum approximate λ-cover problem and the minimum approximate λ-seed problem of a string. Given a string x of length n and an integer λ, the minimum approximate λ-cover (respectively, seed) problem is to find a set of λ substrings each of equal length that covers x (respectively, a superstring of x) with the minimum error, under a variety of distance models containing the Hamming distance, the edit distance and the weighted edit distance. Both problems can be solved in polynomial time.     

The implication problem for ‘closest node’ functional dependencies in complete XML documents

With the growing use of XML as a format for the permanent storage of data, the study of functional dependencies in XML (XFDs) is of fundamental importance in a number of areas such as understanding how to effectively design XML databases without redundancy or update problems, and data integration. In this article we investigate a particular type of XFD, called a weak ‘closest node’ XFD, that has been shown to extend the classical notion of a functional dependency in relational databases. More specifically, we investigate the implication problem for weak ‘closest node’ XFDs in the context of XML documents with no missing information. The implication problem is the most important one in dependency theory, and is the problem of determining if a set of dependencies logically implies another dependency. Our first, and main, contribution is to provide an axiom system for XFD implication. We prove that our axiom system is both sound and complete, and we then use this result to develop a sound and complete quadratic time closure algorithm for XFD implication. Our second contribution is to investigate the implication problem for XFDs in the presence of a Document Type Definition (DTD). We show that for a class of DTDs called structured DTDs, the implication problem for a set of XFDs and a structured DTD can be converted to the implication problem for a set of XFDs alone, and so is axiomatizable and efficiently solvable by the first contribution. We do this by augmenting the original set of XFDs with additional XFDs generated from the structure of the DTD.     

Dichotomies in the Complexity of Solving Systems of Equations over Finite Semigroups

We consider the problem of testing whether a given system of equations over a fixed finite semigroup S has a solution. For the case where S is a monoid, we prove that the problem is computable in polynomial time when S is commutative and is the union of its subgroups but is NP-complete otherwise. When S is a monoid or a regular semigroup, we obtain similar dichotomies for the restricted version of the problem where no variable occurs on the right-hand side of each equation. We stress connections between these problems and constraint satisfaction problems. In particular, for any finite domain D and any finite set of relations Γ over D, we construct a finite semigroup S_Γ such that CSP(Γ) is polynomial-time equivalent to the satifiability problem for systems of equations over S_Γ.