Finding Orthogonal Arrays Using Satisfiability Checkers and Symmetry Breaking Constraints

Orthogonal arrays are very important combinatorial objects which call be used in software testing and other areas. Mathematical methods for constructing such arrays have been studied extensively in the past decades. In contrast, computer search techniques, in particular exhaustive search methods, are rarely used to solve the problem. In this paper, we present all algorithm which finds orthogonal arrays of given sizes or show,, their non-existence. The algorithm is essentially a backtrack search procedure, but enhanced with some novel symmetry breaking (isomorphism elimination) techniques. The orthogonal array is generated column by column, and the constraints are checked by an efficient SAT solver or pseudo-Boolean constraint solver. We have implemented a tool called BOAS (Backtrack-style OA Searcher) using MiniSat and PBS. Experimental results show that our tool can find many orthogonal arrays quickly, especially those with strength higher than 2.