OKlibrary  0.2.1.6
SboxCNF.mac
Go to the documentation of this file.
00001 /* Matthew Gwynne, 28.4.2008 (Swansea) */
00002 /* Copyright 2008 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software$ you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library$ either version 3 of the
00006 License, or any later version. */
00007 
00022 /* Generated by
00023 
00024 maxima> output_rijnsbox_fullcnf_stdname();
00025 shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_Sbox_full.cnf > AES_Sbox_shg.cnf
00026 shell> cat AES_Sbox_shg.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > AES_Sbox_shg.wcnf
00027 shell> ubcsat-okl  -alg gsat -w -runs 100 -cutoff 40000000 -wtarget 294 -solve 1 -seed 3213901809 -i AES_Sbox_shg.wcnf -r model AES_Sbox_s294.ass;
00028 shell> cat  AES_Sbox_full.cnf_primes | FilterDimacs AES_Sbox_s294.ass > AES_Sbox_s294.cnf
00029 maxima> SboxMinCNF : read_fcl_f("AES_Sbox_s294.cnf");
00030 
00031 Statistics : [16,294,1939,8,6]
00032 
00033 */
00034 
00035 SboxMinCNF : [[1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16],
00036        [{-10,-9,-7,-6,-5,3,4},{-10,-9,-8,2,3,5,7},{-10,-8,-1,2,3,5,9},
00037         {-4,-3,-1,7,9,10},{-11,-9,-6,-1,2,7},{-10,-3,1,2,8,11},
00038         {-10,-7,-3,4,8,11},{-12,-7,-4,-2,1,5,6},{-12,-9,-7,-5,-1,4,6},
00039         {-12,-6,-3,-1,2,4,7,9},{-12,-6,-3,-1,8,9},{-12,-7,-5,-3,6,10},
00040         {-12,-11,-8,-6,-4,10},{-12,-4,-2,-1,5,11},{-12,-9,-6,-2,-1,8,11},
00041         {-12,-8,-6,7,9,10,11},{-9,-5,-4,-3,-2,12},{-5,-2,3,6,10,12},
00042         {2,4,7,8,10,12},{-8,-5,-4,3,9,10,12},{-11,-7,-6,-4,1,12},
00043         {-11,-2,3,5,6,7,12},{-11,-8,-3,-1,4,5,12},{-11,-7,-6,-5,2,9,12},
00044         {-6,2,3,7,11,12},{-9,-2,1,8,11,12},{-10,-8,-1,9,11,12},
00045         {-13,-9,-8,-6,-4,2,7},{-13,-5,-4,-3,1,9},{-13,-11,2,5,7,8,9},
00046         {-13,-11,-8,-3,6,10},{-13,-10,6,7,9,11},{-13,-4,3,6,10,11},
00047         {-13,-12,1,4,6,8},{-13,-12,-10,-2,7,8},{-13,-12,-11,-8,-5,1,2},
00048         {-13,-12,-11,-6,3,9},{-13,-12,-11,-5,1,2,10},{-13,-4,1,5,9,12},
00049         {-13,-10,-5,2,4,12},{-13,-7,3,4,5,11,12},{-5,-4,-2,1,3,13},
00050         {-9,-5,-4,-1,3,6,13},{-9,-5,1,7,8,13},{-11,-10,-6,5,9,13},
00051         {-8,1,5,9,11,13},{-12,-4,2,7,8,13},{-12,-10,-9,-6,-5,-3,2,13},
00052         {-12,-10,-7,-3,4,9,13},{-12,-10,-7,5,11,13},{-8,-5,-3,11,12,13},
00053         {-14,-9,-6,-3,4,5,7},{-14,-9,-7,2,3,8},{-14,-11,-8,-7,-6,-1},
00054         {-14,-11,-3,-2,4,8},{-14,-11,-9,-8,-4,-3,2},{-14,-3,4,5,6,11},
00055         {-14,-7,-3,2,6,11},{-14,1,3,5,7,11},{-14,-9,-5,6,7,10,11},
00056         {-14,-12,-1,4,5,6},{-14,-12,3,6,7,8},{-14,-12,-7,1,5,10},
00057         {-14,-12,-11,-10,-8,-1},{-14,-12,-11,-8,-7,-2,10},{-14,-10,-2,3,8,12},
00058         {-14,-11,-4,5,10,12},{-14,-9,-8,3,6,11,12},{-14,-13,-10,-9,-4,-3,5},
00059         {-14,-13,-12,-10,1,11},{-14,-13,-8,-5,4,12},{-14,-4,-3,-2,8,13},
00060         {-14,-8,-2,1,9,13},{-14,-9,-7,2,10,13},{-14,-3,-1,7,8,11,13},
00061         {-14,-11,-9,-7,-2,12,13},{-14,-4,-1,5,11,12,13},{-7,-2,-1,3,9,14},
00062         {-7,-6,2,5,9,14},{-10,-7,-5,3,6,14},{-10,-5,2,3,7,14},
00063         {-10,-3,4,6,7,9,14},{-9,-8,-5,2,10,14},{-11,-6,-2,-1,3,14},
00064         {-11,-5,-3,6,8,14},{-11,-7,-5,-2,1,4,9,14},{-11,-10,-9,-6,-1,14},
00065         {-11,-3,1,7,9,10,14},{-9,3,4,5,8,11,14},{-12,-5,-1,3,7,14},
00066         {-12,-11,-9,-3,5,8,14},{-13,-3,1,4,9,14},{-13,-10,-9,-7,-6,1,14},
00067         {-13,-8,-7,-4,6,11,14},{-13,-12,-6,2,4,5,14},{-13,-12,-6,-4,3,10,14},
00068         {-6,-3,2,5,13,14},{-5,-4,1,6,8,9,13,14},{-4,-3,2,7,12,13,14},
00069         {-15,-6,-4,-3,1,8,9},{-15,-5,-3,2,4,10},{-15,-5,1,2,3,7,10},
00070         {-15,-1,3,4,7,9,10},{-15,-11,-6,-5,-3,4},{-15,-11,-10,-7,-2,3,4},
00071         {-15,-11,-10,-3,5,9},{-15,-11,1,3,5,10},{-15,-5,-1,2,3,4,11},
00072         {-15,-12,-3,-1,5,11},{-15,-12,-10,-5,-1,4,9,11},
00073         {-15,-9,-7,-4,-1,11,12},{-15,-13,-3,-2,5,9},{-15,-13,-5,-3,2,11},
00074         {-15,-13,-6,-4,5,7,11},{-15,-12,-8,-4,3,13},{-15,-12,-10,-3,8,11,13},
00075         {-15,-7,-6,10,12,13},{-15,-14,-10,-9,-7,-3,-2,1},{-15,-14,3,5,8,10},
00076         {-15,-14,-11,-5,-3,2,6},{-15,-14,-11,-8,2,3,5},
00077         {-15,-14,-13,-5,-2,3,7},{-15,-14,-13,6,7,8},{-15,-14,-13,-9,3,5},
00078         {-15,-14,-13,-5,-2,-1,8,10},{-15,-14,-11,-10,3,7,13},
00079         {-15,-8,-5,-3,-2,6,14},{-15,-9,-7,3,5,14},{-15,-11,-10,-8,6,7,14},
00080         {-15,-12,-4,3,10,14},{-15,-1,3,6,12,14},{-15,-2,1,3,4,8,12,14},
00081         {-15,-5,-4,-1,13,14},{-15,-8,-7,-3,10,13,14},{-15,-6,3,8,11,13,14},
00082         {-7,2,6,8,9,15},{-10,-7,-2,1,4,15},{-10,-9,-7,-6,-1,5,15},
00083         {-3,-2,-1,4,7,10,15},{-11,2,3,5,10,15},{-10,3,6,9,11,15},
00084         {-12,-11,5,7,10,15},{-11,-10,1,7,12,15},{-2,-1,4,11,12,15},
00085         {-6,-5,8,11,12,15},{-13,-10,-7,-1,8,15},{-13,-10,-9,-5,-4,15},
00086         {-13,-12,-3,6,9,15},{-13,-6,-2,5,10,12,15},{1,4,5,8,10,13,15},
00087         {-11,-9,-2,1,7,13,15},{-12,-6,-5,3,13,15},{-14,-11,-8,-7,1,4,15},
00088         {-14,-11,-4,-1,2,10,15},{-14,-13,-9,-7,-2,10,15},
00089         {-14,-13,-11,-2,-1,5,15},{-14,-8,-1,12,13,15},
00090         {-14,-11,-10,-1,6,12,13,15},{-11,-7,5,6,14,15},{-6,-2,1,5,11,14,15},
00091         {-12,-10,-5,-4,-3,14,15},{-9,4,11,12,14,15},{-12,-9,6,10,13,14,15},
00092         {-7,-1,12,13,14,15},{-11,-5,4,12,13,14,15},{-16,-10,-2,3,4,5},
00093         {-16,-7,-5,3,6,8,10},{-16,-9,-4,-3,1,8,10},{-16,-1,2,7,9,10},
00094         {-16,-11,-1,2,3,8},{-16,-7,1,3,10,11},{-16,1,2,5,7,10,11},
00095         {-16,-3,-2,8,9,10,11},{-16,-12,-6,-4,2,8},{-16,-12,-10,-9,6,8},
00096         {-16,-7,1,4,5,6,12},{-16,-10,-8,-5,9,12},{-16,-13,-4,5,6,7},
00097         {-16,-13,-10,-5,-4,9},{-16,-13,-11,-1,6,7},{-16,-13,-11,-9,-5,-2,1,3},
00098         {-16,-13,-9,-6,-5,7,11},{-16,-13,-8,-7,-6,10,11},{-16,-13,-12,-7,5,8},
00099         {-16,-6,3,4,8,13},{-16,-8,-7,2,6,10,13},{-16,-4,-2,8,9,10,13},
00100         {-16,-11,-10,-7,-4,6,13},{-16,-10,2,3,6,11,13},{-16,-12,-8,-3,1,7,13},
00101         {-16,-12,-9,-3,-2,4,13},{-16,-4,-2,5,6,11,12,13},
00102         {-16,-14,-7,-6,-1,2,8},{-16,-14,-11,-6,-4,3},{-16,-14,-12,-3,-2,6,7},
00103         {-16,-14,-12,-8,-5,-4,11},{-16,-14,-3,2,4,5,12},
00104         {-16,-14,-12,-5,4,6,13},{-16,-9,-3,1,4,5,7,14},{-16,-8,-6,4,10,14},
00105         {-16,-4,7,8,10,14},{-16,-11,-10,-4,5,14},{-16,-12,-8,-6,-5,-2,14},
00106         {-16,-12,-5,1,11,14},{-16,-13,-8,4,6,11,14},{-16,1,8,9,10,11,13,14},
00107         {-16,-12,6,7,10,13,14},{-16,-12,-11,6,9,13,14},{-16,-15,-8,-7,-6,1,2},
00108         {-16,-15,-11,-8,-7,-1,6},{-16,-15,-11,-10,-9,1,2,6},
00109         {-16,-15,-9,-6,5,12},{-16,-15,-5,-2,7,11,13},
00110         {-16,-15,-14,-10,-6,-5,8},{-16,-15,-14,-8,-2,13},
00111         {-16,-15,-14,4,7,9,13},{-16,-15,-3,-1,12,14},{-16,-9,-6,-5,1,15},
00112         {-16,-9,-7,2,8,10,15},{-16,-11,-6,-5,-3,-2,15},{-16,-3,2,6,11,15},
00113         {-16,-8,-7,-5,-1,11,15},{-16,-12,-6,-3,5,9,15},
00114         {-16,-10,-6,-4,5,12,15},{-16,-13,-12,-2,7,9,15},
00115         {-16,-8,-6,-4,10,13,15},{-16,-14,-6,4,8,15},{-16,-14,-9,-8,2,3,6,15},
00116         {-16,-14,1,2,7,9,15},{-16,-14,-12,-1,4,5,15},{-16,-10,2,6,7,14,15},
00117         {-16,-11,2,3,14,15},{-5,-4,-2,-1,3,9,16},{-11,-6,-5,-2,3,16},
00118         {-9,-8,-2,7,11,16},{-12,-9,-8,3,4,16},{-12,-7,-5,4,10,16},
00119         {-12,-11,-2,1,3,9,16},{-6,-5,-4,2,3,9,12,16},{-10,-6,-3,7,9,12,16},
00120         {-13,-5,-4,-3,-2,-1,16},{-13,-11,-10,-3,1,16},{-13,-6,-2,1,10,11,16},
00121         {-13,-12,-8,-6,-2,-1,5,16},{-13,-11,1,2,12,16},{-3,-2,-1,6,13,16},
00122         {-8,1,4,7,13,16},{-2,4,5,9,13,16},{-10,-7,2,3,6,13,16},
00123         {-11,-10,-2,1,13,16},{-6,1,5,11,12,13,16},{-14,-5,-4,1,2,9,16},
00124         {-14,-6,-5,4,8,10,16},{-14,-11,-9,-3,5,8,16},{-14,1,4,9,11,16},
00125         {-14,-12,-9,-6,-5,-3,16},{-14,-12,-10,-6,8,9,16},
00126         {-14,-13,-3,2,5,10,16},{-7,2,3,4,14,16},{-10,-8,1,9,14,16},
00127         {4,7,10,11,14,16},{-12,-9,-7,-2,1,10,14,16},{-9,-6,8,12,14,16},
00128         {-4,-3,5,10,12,14,16},{-13,-9,-2,1,7,14,16},{-13,-9,-3,2,8,14,16},
00129         {-13,-3,-1,6,8,12,14,16},{-8,3,9,13,14,16},{-15,-4,-3,5,6,16},
00130         {-15,-9,-8,-3,4,16},{-15,-11,-10,-9,-5,-4,8,16},{-15,-12,-9,2,6,16},
00131         {-15,-13,-10,-7,-4,3,16},{-15,-13,-10,-1,3,9,12,16},{-15,5,6,8,13,16},
00132         {-15,-7,2,11,13,16},{-15,-14,2,3,10,16},{-15,-14,-12,-10,-6,11,13,16},
00133         {-15,-13,-7,-5,9,14,16},{-7,-4,-2,-1,3,15,16},{-8,-5,-1,4,15,16},
00134         {-8,-3,1,6,15,16},{-9,3,5,7,8,15,16},{-10,1,2,8,15,16},
00135         {-11,-8,-4,6,15,16},{-9,-4,1,5,11,15,16},{-12,-1,2,7,15,16},
00136         {-5,-4,3,8,12,15,16},{-14,-7,-6,-4,15,16},{-14,-7,5,9,10,11,15,16},
00137         {-12,-8,-7,11,14,15,16},{4,6,9,12,14,15,16},{-7,-6,-3,13,14,15,16},
00138         {-4,5,7,11,13,14,15,16}]]$
00139