SEM: a System for Enumerating Models
Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence. Automated Reasoning. Pages 298-302.
Abstract
Model generation can be regarded as a special case of the Constraint Satisfaction Problem (CSP). It has many app lications in AI, computer science and mathematics. In this paper, we describe SEM , a System for Enumerating finite Models of first-order many-sorted theories. To the best of our knowledge , SEM outperforms any other finite model generation system on many test problems. The high performance of SEM relies on the following two techniques: (a) an efficient implementation of constraint propagation which requires little dynamic allocation of storage; (b) a powerful heuristic which eliminates many isomorphic partial models during the search. We will present the basic algorithm of SEM along with these two techniques. Our experimental results show that general purpose finite model generators are indeed useful in many applications.
@inproceedings{ijcai1995p39,
title = {SEM: a System for Enumerating Models},
author = {Zhang, Jian and Zhang, Hantao},
booktitle = {Proceedings of the Fourteenth International Joint Conference on
Artificial Intelligence, {IJCAI-95}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Chris S. Mellish},
pages = {298--302},
year = {1995},
note = {Automated Reasoning},
url = {https://ijcai.org/proceedings/1995/39},
}
TY - CPAPER TI - SEM: a System for Enumerating Models AU - Zhang, Jian AU - Zhang, Hantao T2 - Proceedings of the Fourteenth International Joint Conference on Artificial Intelligence, IJCAI-95 PB - International Joint Conferences on Artificial Intelligence PY - 1995 SP - 298 EP - 302 UR - https://ijcai.org/proceedings/1995/39 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
