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 64bit 4x4 with 4bit 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 8bit Sbox using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.

minimising the 8bit 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 8bit field inversion using a translation of the optimisation problem for the minimum hypergraph transversal problem, using the subsumption hypergraph.

minimising the 8bit 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> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG AES_sbox_2_4_full.cnf  MinOnes2WeightedMaxSATO3DNDEBUG > sbox_4_shg.wcnf
shell> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG AES_sbox_2_8_full.cnf  MinOnes2WeightedMaxSATO3DNDEBUG > sbox_8_shg.wcnf
shell> for x in 3 9 11 13 14; do QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG ss_byte2_8_field_mul_full_${x}.cnf  MinOnes2WeightedMaxSATO3DNDEBUG > 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> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG AES_sbox_2_4_full.cnf  MinOnes2PseudoBooleanO3DNDEBUG > sbox_4_shg.pb
shell> QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG AES_sbox_2_8_full.cnf  MinOnes2PseudoBooleanO3DNDEBUG > sbox_8_shg.pb
shell> for x in 3 9 11 13 14; do QuineMcCluskeySubsumptionHypergraphn16O3DNDEBUG ss_byte2_8_field_mul_full_${x}.cnf  MinOnes2PseudoBooleanO3DNDEBUG > 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
clauseset 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 pseudoboolean problem.
Definition in file Benchmarks.hpp.