Abstract
An Automated Finite First-Order Model Generator Has Been Developed. the Problem is Viewed as a First-Order Satisfiability Problem. Most Existing Model Generators Reduce the Problem to Propositional Satisfiability by Converting the Input First-Order Clauses into Propositional Clauses. This Generator, Unlike Others, Stores the Input First-Order Clauses and Solves the Problem Directly. It Uses an Exhaustive Backtracking Algorithm with Weight-Based Splitting. a Negative Constraint Propagation is Implemented to Reduce the Number of Decision Points and Thus to Speed Up the Search. © 1997 ACM.
Recommended Citation
O. Shumsky et al., "Direct Finite First-Order Model Generation with Negative Constraint Propagation Heuristic," Proceedings of the ACM Symposium on Applied Computing, pp. 25 - 29, Association for Computing Machinery, Jan 1997.
The definitive version is available at https://doi.org/10.1145/331697.331704
Department(s)
Computer Science
International Standard Book Number (ISBN)
978-089791850-3
Document Type
Article - Conference proceedings
Document Version
Citation
File Type
text
Language(s)
English
Rights
© 2023 Association for Computing Machinery, All rights reserved.
Publication Date
01 Jan 1997
