Efficient SAT-based techniques for Design of Experiments by using static variable ordering

摘要

Design of Experiments (DOE) is an important problem for ensuring the quality of EDA with applications to the evaluation of techniques and tools in all sub-fields of EDA, e.g., yield and variability optimization, error correcting codes, and software testing. DOE can be formulated as a Quasigroup Completion Problem (QCP). We propose and compare 23 heuristics for efficient solving of QCPs by translation to Boolean Satisfiability (SAT) and exploiting static Boolean variable ordering to solve the resulting SAT formulas. This comparison is based on both satisfiable and unsatisfiable instances with varying numbers of empty cells. The translation to SAT is done with the minimal (2-D) and extended (3-D) encodings by Kautz et al. The contributions of the paper include: 1) proposal and comparison of the 23 heuristics; 2) study of the benefits from the 3-D vs. the 2-D encoding, and from local symmetry-breaking constraints, given the static variable ordering heuristics; and 3) identification of the most efficient single heuristic, and portfolios of heuristics that can be run in parallel on multiple cores in a modern CPU. Compared to the default dynamic variable ordering heuristic in the SAT solver, when using static variable-ordering heuristics we achieve an average speedup of 2.8?? with the single best heuristic, 7.2?? with the best portfolio of two parallel heuristics, 13.6?? with the best portfolio of four parallel heuristics, and speedups on individual benchmarks of up to 3 orders of magnitude.