Vakili, AmirhosseinDay, Nancy A.2020-07-062020-07-062016https://dx.doi.org/10.1007/978-3-319-48989-6_41http://hdl.handle.net/10012/16034This is a post-peer-review, pre-copyedit version of a paper presented at the International Symposium on Formal Methods. The final authenticated version is available online at: https://dx.doi.org/10.1007/978-3-319-48989-6_41The problem of finite model finding, finding a satisfying model for a set of first-order logic formulas for a finite scope, is an important step in many verification techniques. In MACE-style solvers, the problem is mapped directly to a SAT problem. We investigate an alternative solution of mapping the problem to the logic of equality with uninterpreted functions (EUF), a decidable logic with many well-supported tools (e.g., SMT solvers). EUF reasoners take advantage of the typed functional structures found in the formulas to improve performance. The challenge is that EUF reasoning is not inherently finite scope. We present an algorithm for mapping a finite model finding problem to an equisatisfiable EUF problem. We present results that show our method has better overall performance than existing tools on a range of problems.enfinite model findingequality with uninterpreted functionsfinite scopekodkodsymmetry breaking predicatesConference Paper