拉丁方是组合数学问题中一个重要的组合结构，有着重要的理论意义和广泛的应用。其中，符合Costas性质的拉丁方更是由于很好地和雷达、声纳等实际问题吻合而有着很高的研究意义。n阶的拉丁方是一个n*n的矩阵，矩阵每一个点都是n元集合中的一个元素，每一个元素在每行每列中都只出现一次。在Costas拉丁方中，每个元素所在的行和列恰好为一个Costas数组所对应的n阶矩阵，即矩阵的每一行、每一列上都有且仅有一个点，其中任意两点的连线形成的坐标向量在方向和长度上至少有一个不同。 关于单个的Costas拉丁方的存在性，已经有一些数学结果。2015年，苏州大学的朱烈教授提出了一个新的研究问题：正交的Costas拉丁方是否存在？两个拉丁方正交是指将两个拉丁方进行并置操作后（将矩阵对应单元格里的元素放一块构成元素对）得到的所有元素对中没有重复的元素对。由于六阶的正交拉丁方不可能存在，因此8阶以上的正交的Costas拉丁方是否存在都是未知的。此外，朱烈教授还提出了幂等的Costas拉丁方是否存在的问题。 对于组合设计问题的现实求解，目前主要有两类方法：构造性的数学方法和通过计算机程序的搜索。构造性的数学方法对于问题的复杂程度有一定局限性，比较复杂的问题模型无法使用此类方法。计算机程序搜索虽然最坏代价可能很高，但是可以求解很多比较复杂的问题模型。 本文提出了一个基于计算机工具的搜索Costas拉丁方的方法，利用Costas拉丁方的一些性质构造一阶逻辑约束公式，通过一阶逻辑有限模型产生工具SEM对Costas拉丁方的存在即正交Costas拉丁方的存在性进行搜索求解。提出横向矩阵作为矩阵的一种表达方式，降低约束公式的复杂度，加快工具对于问题的搜索速度。为了克服一阶逻辑无法表达算术运算的问题，我们构造了减法矩阵，将减法对应结果存于矩阵中，使得可以使用一阶逻辑公式表达带减法的Costas约束。本文使用了打破对称方法，加入打破对称约束条件避免了对于同构矩阵的重复搜索，大幅度减小了问题搜索空间的大小，大大提高了问题求解的效率。 本文主要针对8阶的Costas拉丁方做搜索求解，通过搜索确定了一共有312个不同构的8阶Costas拉丁方，其中幂等的有6个，而且所有8阶Costas拉丁方两两之间均不正交。