Non-isomorphic CNF Generation

The Graph Isomorphism (GI) Class is the class of all the problems equivalent to the Graph Isomorphism problem, that is not known to be solvable in polynomial time nor to be NP-complete. GI thus is a very interesting complexity class that may be in NP-intermediate. In this work we focus on the CNF Syntactic Formula Isomorphism (CSFI) problem, that has been proved to be GI-complete, and we present a formal approach to the definition of “trivial non-isomorphic” instances and an algorithm to generate “non-trivial” instances. The applications of such generator are twofold: on the one side we can use it to compare deterministic algorithms, and on the other side, following recent approaches for NP-complete problems such as SAT and TSP, we can also use the generated instances to train neural networks.