Finite Model Finding in First-Order Logic

Abstract

Finding finite models for first-order logic has a range of applications in Mathematics as well as Computer Science, for example in algebra or verification. This report gives a survey over finite model finding algorithms that have been used successfully in this context. The most direct approach is to view the problem as a general constraint solving problem and to develop a specialized constraint solver. Other approaches devise a sophisticated translation to a well-established logic, which then allows to take advantage of existing efficient solvers. In addition to describing these methods in their basic form crucial improvements for practical applications are presented. Finally, some questions for potential future research are formulated.