An Isomorph-Free SEM-Like Enumeration of Models
Thierry Boy de la Tour, Prakash Countcham · Electronic Notes in Theoretical Computer Science · 2005
We investigate the integration of the enumeration of finite models of a formula, including unit propagation and pruning mechanisms, as provided by the system SEM, into McKay's general method of isomorph-free exhaustive enumeration. The two techniques turn out to be nicely compatible, though this requires some adaptations, and to prove some non-trivial properties.