Intellectual property metering(12)

Abstract. We have developed the first hardware and software (intellectual property) metering scheme that enables reliable low overhead proofs for the number of manufactured parts and copied programs. The key idea is to make each design slightly different d

6.1 Graph Coloring

The NP-hard graph vertex coloring (GC) optimization seeks to color a given graph with as few colors as possible, such that no two adjacent vertices receive the same color.

Given a graph, our objective is to create as many as possible high quality solutions that are relatively close. By high quality, we mean that if the optimal solution is known,then all the solutions that we generate will not use any extra color. Therefore, the finger-printing techniques for GC cannot be used in this case, because they usually introduce overhead although they are very effective in creating new solutions.

The following steps illustrate our algorithm for GC solution generation.

1.Apply a graph coloring heuristic to color the given graph

and obtain a k -color

scheme as the seed solution.

2.For each node , calculate c(v), the number of different colors that v ’s neighbors

get.

3.Sort the nodes V in the increasing order of c(v).

4.For each node with , change v ’s color and report differ-

ent solutions.

5.For all pairs of nodes (u,v) with and , try different coloring

schemes for nodes u and v and report the new found solutions if any.

In next section, we will demonstrate the performance of this algorithm by experimen-tal results. It turns out that this simple strategy works very well in real-life graphs. Notice that no extra colors will be used in our approach, i.e., all the derived solutions will have the same quality as the seed solution. And these solutions differ from the seed solution only at the colors of one or two nodes.6.2 SAT

The boolean satisfiability problem (SAT ) seeks to decide, for a given formula, whether there is a truth assignment for its variables that makes the formula true. We necessarily assume that the SAT instance is satisfiable and that there is a large enough solution space to accommodate multiple solutions.

We use pre-processing techniques to create different but close solutions for the SAT problems. In particular, before we solve the SAT instance, we delete a selective subset of variables and essentially make them “don’t-cares”. Suppose we introduce k such “don’t-cares”, then we should be able to build 2k distinct solutions from one seed solution if it exists. Moreover, these 2k solutions will assign exactly the same value to the variables that are not selected, i.e., they are close.

We select the variables to be deleted iteratively and greedily based on the following criteria: for each variable v , let n v be the number of clauses that contains either v or v ’, and let s i be the length of the i th such clause. Define

(6)

1.

For each variable v in formula F , calculate c(v) and unmark v .2.

Select a unmarked v with the smallest c(v), delete both v and v’ from F to create a new formula F’.3.Apply a SAT solver to solve F’.G V E ,()v V ∈v V ∈c v ()k 1–<k 1–c v ()–c u ()k 1–<c v ()k 1–<c v ()12S i 1–1–----------------------i 1=n l ∑=