adding support for isymganak

[IbrahimElk]

isymganak is a model counter that improves cache efficiency
in DPLL-based solvers by identifying structurally
identical components (for example, A ∨ B and C ∨ D) and reusing their
cached model counts.

Using this model counter's traces to construct a circuit is less straightforward
than it might seem. When a cached component is reused, its variables must be
renamed to match the current component, otherwise the circuit would not correspond
to the input CNF. A mapping from the cached component's variables to those of
the current component is therefore necessary.

Such a mapping is fairly easy to derive, but is not currently stored by the solver.
Since isymganak uses canonical-form isomorphism checking via NAUTY, the cached
components need to store the lab array. After a sparsenauty call:

for (unsigned i = 0; i < n; i++) {
    lab[i] = i;
}
sparsegraph *canonical_graph = new sparsegraph();
SG_INIT(*canonical_graph);
sparsenauty(graph, lab, ptn, orbits, &options, &stats, canonical_graph);

the contents of lab on return give the labelling of the input graph corresponding
to the canonical form. In other words, lab encodes the permutation $\pi$ mapping
each variable to its position in the canonical form. Given two isomorphic
components $A$ and $B$ with their respective permutations:

$$\pi_A : \text{vars}(A) \to \text{canonical form}$$ $$\pi_B : \text{vars}(B) \to \text{canonical form}$$

one can obtain a concrete bijection between their variables:

$$\sigma = \pi_B^{-1} \circ \pi_A : \text{vars}(A) \to \text{vars}(B)$$

This $\sigma$ is exactly the renaming needed to reuse $A$'s cached result for $B$ (or vice versa).

As a further direction, it may be possible to transform the DNNF circuit produced
by isymganak into a more succinct circuit (other dan DNNF) by explicitly labelling
nodes/subtrees that were derived from symmetric component caching.