Abstract: The present paper deals with the SAT problem and the multiple methods to solve it, then shows how to use the SAT prover to crack first order logic problem. After that the details of our first order logic modal gener ator__FOLMG is given, it behaves well in comparison with MACE which is anot her good model generator.

Key words: SAT, model generation, propositional logic, first order logic