命题逻辑可满足性(SAT)问题和有限论域一阶逻辑模型搜索(FOLMS)问题是计算机理论科学中的经典问题，不仅在理论上有着重要的地位，而且在许多实际问题中得到了广泛的应用。多年来，学者们针对SAT问题进行了大量的研究，得到了许多有效的算法和工具；而FOLMS问题的研究虽然取得了一定的成果，但仍然显得较为薄弱。本文的工作是将这两个问题结合起来考虑，利用SAT问题的研究成果，结合FOLMS问题本身的特点，来改进FOLMS算法和工具。 为了利用现有的高效SAT工具，研究了如何将FOLMS问题转换为SAT问题来求解，提出了一个新的转换算法，它能更好的利用SAT工具同时在转换效率上也有所提高。另一项研究工作是关于如何在转换法中利用FOLMS问题所具有的同构现象，通过添加约束从而减少转换所得的SAT问题的搜索空间。实验表明，这样的算法和约束是有效的，可以用来解决数学研究和实际应用中的许多问题。基于上述的算法，实现了一个实用的自动转换工具SAGE。 为了提高FOLMS本身搜索算法的效率，研究了如何借鉴SAT问题算法现有研究成果来改进搜索算法。提出了一个新的直接搜索算法，它使用了在SAT问题中行之有效的冲突分析和学习机制。在具体实现该算法时，考虑了使用内嵌命题逻辑公式集和SAT工具来提高其实用性和效率。基于上述的算法和原有的FOLMS直接搜索工具SEM，实现了SEMLL工具。