OKlibrary  0.2.1.6
Benchmarks.hpp File Reference

Benchmarks for submission to the 2011 SAT competition. More...

Go to the source code of this file.


Detailed Description

Benchmarks for submission to the 2011 SAT competition.

Todo:
Links
Todo:
Prepare benchmarks for SAT 2011
  • Other than the standard AES and small scale translations, the minimisation problems for the AES boxes (Sbox and field multiplications) should yield good benchmarks for weighted MaxSAT solvers.
  • Our benchmarks should come under the "Applications" category (see "Links").
  • We consider the following benchmarks for the SAT competition:
    • Full AES encryption and decryption for one round up to ten rounds using the "minimum" and "canonical" translations.
    • Full AES key discovery for one round using the "minimum" and "canonical" translations.
    • AES key discovery for one round up to three rounds for the 64-bit 4x4 with 4-bit field elements AES variant using "minimum" and "canonical" translations (one round here is currently the limit of what we are able to solve).
  • We consider the following benchmarks for the pseudo boolean competition:
    • minimising the 8-bit Sbox using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.
    • minimising the 8-bit multiplications (03,09,11,13,14) using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.
    • minimising the 8-bit field inversion using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.
    • minimising the 8-bit Sbox linear multiplication using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.
  • For the MaxSAT competition, we should consider the same problems as with the PseudoBoolean, but simply using a translation of the minimum transversal problems into MaxSAT problems, rather than pseudo boolean.
  • We should further specify each of the above benchmarks and move them into separate todos with instructions on how to generate each instance, their statistics and so on. This information can then be moved into their respective accompanying documents (see "Supporting documents" in Experimentation/Investigations/plans/SATCompetition.hpp .
  • For the MaxSAT competition, the instances are generated by:
    maxima> output_ss_sbox_fullcnf_stdname(2,4,ss_polynomial_2_4);
    maxima> output_ss_sbox_fullcnf_stdname(2,8,ss_polynomial_2_8);
    maxima> for e in [3,9,11,13,14] do output_ssmult_fullcnf_stdname(e,2,8,ss_polynomial_2_8);
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_sbox_2_4_full.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > sbox_4_shg.wcnf
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_sbox_2_8_full.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > sbox_8_shg.wcnf
    shell> for x in 3 9 11 13 14; do QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG ss_byte2_8_field_mul_full_${x}.cnf | MinOnes2WeightedMaxSAT-O3-DNDEBUG > mul_8_${x}_shg.wcnf; done
       
  • For the PseudoBoolean competition, the instances are generated by:
    maxima> output_ss_sbox_fullcnf_stdname(2,4,ss_polynomial_2_4);
    maxima> output_ss_sbox_fullcnf_stdname(2,8,ss_polynomial_2_8);
    maxima> for e in [3,9,11,13,14] do output_ssmult_fullcnf_stdname(e,2,8,ss_polynomial_2_8);
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_sbox_2_4_full.cnf | MinOnes2PseudoBoolean-O3-DNDEBUG > sbox_4_shg.pb
    shell> QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG AES_sbox_2_8_full.cnf | MinOnes2PseudoBoolean-O3-DNDEBUG > sbox_8_shg.pb
    shell> for x in 3 9 11 13 14; do QuineMcCluskeySubsumptionHypergraph-n16-O3-DNDEBUG ss_byte2_8_field_mul_full_${x}.cnf | MinOnes2PseudoBoolean-O3-DNDEBUG > mul_8_${x}_shg.pb; done
       
  • DONE (see Satisfiability/Interfaces/InputOutput/MinOnes2WeightedMaxSAT.cpp) We need proper translations of the minimum hypergraph transversal problem into a weighted MaxSAT problem. See "Add MinOnes2WCNF output clause-set adaptor" in Interfaces/InputOutput/plans/ClauseSetAdaptors.hpp.
  • DONE (see Satisfiability/Interfaces/InputOutput/MinOnes2PseudoBoolean.cpp) We also need proper translations of the minimum hypergraph transversal problem into a pseudo-boolean problem.

Definition in file Benchmarks.hpp.