Ever since E. T. Parker constructed an orthogonal pair of $10\times10$ Latin squares in 1959, an orthogonal triple of $10\times10$ Latin squares has been one of the most sought-after combinatorial designs. Despite extensive work, the existence of such an orthogonal triple remains an open problem, though some negative results are known. In 1999, W. Myrvold derived some highly restrictive constraints in the special case in which one of the Latin squares in the triple contains a $4\times4$ Latin subsquare. In particular, Myrvold showed there were twenty-eight possible cases for an orthogonal pair in such a triple, twenty of which were removed from consideration. We implement a computational approach that quickly verifies all of Myrvold's nonexistence results and in the remaining eight cases finds explicit examples of orthogonal pairs -- thus explaining for the first time why Myrvold's approach left eight cases unsolved. As a consequence, the eight remaining cases cannot be removed by a strategy of focusing on the existence of an orthogonal pair; the third square in the triple must necessarily be considered as well. Our approach uses a Boolean satisfiability (SAT) solver to derive the nonexistence of twenty of the orthogonal pair types and find explicit examples of orthogonal pairs in the eight remaining cases. To reduce the existence problem into Boolean logic we use a duality between the concepts of transversal representation and orthogonal pair and we provide a formulation of this duality in terms of a composition operation on Latin squares. Using our SAT encoding, we find transversal representations (and equivalently orthogonal pairs) in the remaining eight cases in under two hours of computing on a large computing cluster.

翻译：自E. T. Parker于1959年构造出第一对正交的$10\times10$拉丁方以来，$10\times10$拉丁方的正交三元组便成为最受关注的组合设计问题之一。尽管已有大量研究，此类正交三元组的存在性仍是一个悬而未决的公开问题，尽管已知一些否定性结果。1999年，W. Myrvold在假设三元组中某个拉丁方包含一个$4\times4$拉丁子方的特殊情形下，推导出了一系列高度严格的约束条件。具体而言，Myrvold证明了在此类三元组中正交对可能存在28种情形，其中20种可被排除。我们实现了一种计算方法，快速验证了Myrvold的所有非存在性结果，并在剩余的8种情形中找到了正交对的显式示例——这首次解释了为何Myrvold的方法会遗留8种未解情形。由此推论，剩余8种情形无法通过仅关注正交对存在性的策略予以排除；三元组中的第三个拉丁方也必须纳入考量。我们的方法采用布尔可满足性（SAT）求解器来推导20种正交对类型的非存在性，并在剩余8种情形中找到正交对的显式示例。为将存在性问题转化为布尔逻辑，我们利用了横截表示与正交对概念之间的对偶性，并通过拉丁方上的复合运算给出了该对偶性的形式化表述。基于我们的SAT编码，我们在大型计算集群上通过不足两小时的计算，在剩余8种情形中找到了横截表示（等价于正交对）。