Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
10329751 | Electronic Notes in Theoretical Computer Science | 2005 | 23 Pages |
Abstract
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.
Keywords
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Thierry Boy de la Tour, Prakash Countcham,