(The following text has been copypasted to the SAT/SMT by example book.)
Maybe you got a program you want to test against different compilers, different optimization options, etc. Maybe this program is CPU intensive app, like Bitcoin miner, SETI@home client or whatever. And you're unsure, which compiler would produce the best code.
Say, you have 4 compilers, 4 optimization options and 4 computers to test everything. Full test will take one day. You can arrange all this like:
| Day | Computer 1 | Computer 2 | Computer 3 | Computer 4 | | | Compiler 1 | Compiler 2 | Compiler 3 | Compiler 4 | |--------+---------------+---------------+---------------+---------------| | Day 1 | Opt.options 1 | Opt.options 2 | Opt.options 3 | Opt.options 4 | | Day 2 | Opt.options 2 | Opt.options 3 | Opt.options 4 | Opt.options 1 | | Day 3 | Opt.options 3 | Opt.options 4 | Opt.options 1 | Opt.options 2 | | Day 4 | Opt.options 4 | Opt.options 1 | Opt.options 2 | Opt.options 3 |
After testing, you'll find a best pair of compiler and optimization options.
This is a Latin square. You saw it often in Sudoku form, which is also Latin square, but with additional constraints (9 3*3 boxes).
Thanks to Latin square, you could test all pairs in 4 days using only 4 computers. Even if you have no idea about Latin squares and will try to find this arrangement manually, you'll come with a solution similar to that, because there is no smaller solution.
Now the problem is harder: you have 4 frameworks/libraries/APIs to test. Finally, you want to find a best triple: compiler + optimization options + framework.
For the problem like that it would be hard to find a good arrangement manually. I'm using my small utility to find two Latin squares, that are mutually orthogonal to each other:
first: | mate: 0 1 2 3 | 0 3 1 2 1 0 3 2 | 1 2 0 3 2 3 0 1 | 2 1 3 0 3 2 1 0 | 3 0 2 1 concatenated: 00 13 21 32 11 02 30 23 22 31 03 10 33 20 12 01
Each pair in the final 'concatenated' (or superimposed) table is unique. Now add this 'concatenated' table to ours:
| Day | Computer 1 | Computer 2 | Computer 3 | Computer 4 | | | Compiler 1 | Compiler 2 | Compiler 3 | Compiler 4 | |-------+------------+------------+------------+------------| | Day 1 | 0+0 | 1+3 | 2+1 | 3+2 | | Day 2 | 1+1 | 0+2 | 3+0 | 2+3 | | Day 3 | 2+2 | 3+1 | 0+3 | 1+0 | | Day 4 | 3+3 | 2+0 | 1+2 | 0+1 |
Each pair of digits would reflect optimization options + framework. Thanks to MOLS (Mutually Orthogonal Latin Squares) you can test all triplets (compiler + optimization options + framework) (again) in 4 days using 4 computers.
Now the next problem: you also have 4 different operating systems. macOS, Windows, and maybe two flavours of Unix. 3 MOLS would help.
first: | mate 1: | mate 2: 0 1 2 3 | 0 2 3 1 | 0 3 1 2 1 0 3 2 | 1 3 2 0 | 1 2 0 3 2 3 0 1 | 2 0 1 3 | 2 1 3 0 3 2 1 0 | 3 1 0 2 | 3 0 2 1 first+mate 1 | first+mate 2 | mate 1+mate 2 00 12 23 31 | 00 13 21 32 | 00 23 31 12 11 03 32 20 | 11 02 30 23 | 11 32 20 03 22 30 01 13 | 22 31 03 10 | 22 01 13 30 33 21 10 02 | 33 20 12 01 | 33 10 02 21 first+mate 1+mate2: 000 123 231 312 111 032 320 203 222 301 013 130 333 210 102 021
These are 3 Latin squares where any pair of these 3 squares are orthogonal to each other. Hence, in the final table you see only unique triplets. Let's add this to our table:
| Day | Computer 1 | Computer 2 | Computer 3 | Computer 4 | | | Compiler 1 | Compiler 2 | Compiler 3 | Compiler 4 | |-------+------------+------------+------------+------------| | Day 1 | 0+0+0 | 1+2+3 | 2+3+1 | 3+1+2 | | Day 2 | 1+1+1 | 0+3+2 | 3+2+0 | 2+0+3 | | Day 3 | 2+2+2 | 3+0+1 | 0+1+3 | 1+3+0 | | Day 4 | 3+3+3 | 2+1+0 | 1+0+2 | 0+2+1 |
Each unique triplet is: optimization options + framework + OS. Again you need only 4 days and 4 computers to test each pair of these parameters and pick the best set of compiler + optimization options + framework + OS.
MOLS generation is straightforward using SAT solvers. Soon, I'll write about that too.
Unfortunately, MOLS generation has its limits too. Only small squares of order less than 10 are easy to generate. Generation of larger is a very hard problem. Despite of that, small MOLS are very useful.
Yes, I know about these lousy Disqus ads. Please use adblocker. I would consider to subscribe to 'pro' version of Disqus if the signal/noise ratio in comments would be good enough.