graphs instead of the original input graphs.3 This introduced methods NM*
and ZV*. For completeness of the evaluation, we introduced HS*, too.

For each method, for each value of parameter p, we present one plot that shows the percentage of successes in isomorphic subgraph matching for each value of m. The plots are presented in figures 2,3, and 4. It can be noted that the accuracy of ZV and ZV* generally rises much later than for the other methods. NM* obviously performs the best.

In Table 2, for each method, we present the overall accuracy in the experiment and the total time spent for the experiment.

| NM       | NM*   | HS   | HS*    | ZV     | ZV*   |      |
|----------|-------|------|--------|--------|-------|------|
| Accuracy | 27.3  | 37.8 | 17.5   | 17.5   | 13.9  | 15.0 |
| Time     | 2062s | 838s | 11511s | 11730s | 349s  | 230s |

Table 2: Overall accuracy and time needed for the experiment, for each method used.

The complement trick obviously improved NM and ZV methods. As expected, it did not affect the HS method. For NM* and ZV* methods, apart from boosting the accuracy, the computation time is significantly reduced. For NM method, this modification reduces the computation time for solving the assignment problem in NM update rule, since it reduces the number of nodes to be matched in the cases when this number can be large (dense graphs).

## 5.2. The Classification Of Boolean Formulae

Here we present the problem of the classification of Boolean formulae which we use to show that our method can capture a meaningful similarity in a real world problem.

Various important practical problems can be modeled in Boolean logic including problems in electronic design automation, software and hardware verification, scheduling, timetabling, artificial intelligence, and other domains. Each instance of the problem is represented by a Boolean formula. Classification of Boolean formulae has been investigated in order to automatically tune SAT
solvers (systems for checking the satisfiability of Boolean formulae) that is a practically important and challenging problem. A very reliable approach to Boolean formulae classification is based on measuring the distances between the formulae [14]. In that approach, in order to compute the distance between the formulae, they are represented by numerical vectors of some syntactical features, that can be computed for each formula. However, Boolean formulae have a natural variable-clause graph representation [15] that could be used for their classification.