In this paper, we generalize the theory of a convex set relaxation for the maximum weight stable set problem due to Grotschel, Lovasz and Schrijver to the generalized stable set problem. We define a convex set which serves as a relaxation problem, and show that optimizing a linear function over the set can be done in polynomial time. This implies that the generalized stable set problem for perfect bidirected graphs is polynomial time solvable. Moreover, we prove that the convex set is a polytope if and only if the corresponding bidirected graph is perfect. The definition of the convex set is based on a semidefinite programming relaxation of Lovasz and Schrijver for the maximum weight stable set problem, and the equivalent representation using infinitely many convex quadratic inequalities proposed by Fujie and Kojima is particularly important for our proof.

Bidirected graphs which are generalizations of undirected graphs, have three types of edges: (+,+)-edges, (-,-)-edges and (+,-)-edges. Undirected graphs are regarded as bidirected graphs whose edges are all of type (+,+). The notion of perfection of undirected graphs can be naturally extended to bidirected graphs in terms of polytopes. The fact that a bidirected graph is perfect if and only if the undirected graph obtained by replacing all edges to (+,+) is perfect was independently proved by several researchers. This paper gives a polyhedral proof of the fact and introduces some new knowledge on perfect bidirected graphs.

This paper describes a new method for verifying designs at the RTL with respect to their specifications at the functional level. The base of the verification method shown here is the translation of the specification and design representations to graph models, where the descriptions common to both representations have a symbolic representation. These symbol labeled graphs are then simplified and, by solving the all node-pair path expression problem for them, a pair of regular expressions is obtained for every two nodes in the graphs. The first regular expression in each pair represents the flow of control and the second one the flow of data between the corresponding nodes. The process of verification is carried out by checking whether or not every pair of regular expressions of the specification has a corresponding pair in the design.