Plans regarding SAT competitions.
More...
Go to the source code of this file.
Detailed Description
Plans regarding SAT competitions.
 Todo:
 Update and completion of plans regarding SAT 2011

The SAT competitions are nearly finished now (except of the PB evaluation, which will be repeated).

The benchmarks were created, submitted, and are documented in Experimentation/Benchmarks/docus/SAT2011.hpp.

We need the results of the competition on our instances available in the library.

We should also provide full documentation of the AES instances as a LaTeX document with a description of the cipher. This should fit in with the generation of instances for SAT2012, discussed in "Benchmarks for
SAT 2012".

All results of the competition should be made available (in edited form, of course) on our benchmark sites.

Also links to competition pages are needed there.

Plus general comments and explanations.

The successful solvers need to be installed.

All todos need to be cleanedup; most of them removed (possible with transfer to docus).
 Todo:
 Benchmarks for SAT 2012

The deadline for:

SAT Challenge benchmark submission is 11/4/2012; http://baldur.iti.kit.edu/SATChallenge2012/submission.html .

PseudoBoolean registration is 13/4/2012; PseudoBoolean benchmark submission is 20/4/2012; http://www.cril.univartois.fr/PB12/ .

MaxSAT evaluation submission is 23/3/2012; http://maxsat.ia.udl.cat/introduction/ .

DONE (nothing to submit) QBF evaluation registration is Wednesday 29th February 2012.

DONE (nothing to submit) QBF benchmark submission is Thursday 15th March 2012.

MG has registered for both the SAT challenge and PseudoBoolean competition (so only the submission deadlines are relevant).

The specifications of each of the formats can be found at:

The categories for SAT 2012, the PseudoBoolean and MaxSAT competitions are (up to trivial renaming) the same as in 2011, discussed in 'Categories / "tracks" for SAT 2011' below.

Best in every series to have a mixture, from known to unknown instances, from nottoohard to likelyveryhard. So for each series we need:

an "easy" instance taking around 1 minute to solve;

several "mediumeasy" instances taking 515 minutes to solve;

several "medium" instances taking 1560 minutes to solve;

one or two "mediumhard" instances taking 60180 minutes to solve;

a "hard" instance taking a day or more to solve.

The SAT Challenge 2012 requires a 1 to 2 page (max 2) PDF document in the IEEE proceeding style, available at http://www.ieee.org/conferences_events/conferences/publishing/templates.html . These descriptions will be posted on the website.

DONE We should consider the format, and what instances we can provide for the QBF evaluation.

For the formats see below; it should be checked that these haven't changed from 2011.

For the categories see below; it should be checked that these haven't changed from 2011.
 Todo:
 Categories / "tracks" for SAT 2011

This todo should be reviewed and moved into the docus, with up to date links for SAT2012.

SAT competition:

Random uniform kSAT instances where only generators are allowed.

Applications where instances of industrial and practical interest are required.

Crafted where instances designed to be hard for SAT solvers, representing difficult puzzles, mathematical problems etc are required. One should specify whether these instances are SAT or UNSAT.

PseudoBoolean competition:

Pseudo Boolean Satisfaction, PBS, which involves deciding satisfiability for a set of PB constraints.

Pseudo Boolean Optimisation, PBO, which involves finding a model which optimises a given objective function.

Weighted boolean optimisation, WBO where pseudo boolean constraints have weights and then a solution must be found which minimises the sum of the weight of the falsified constraints.

For PBS and PBO, there are the following categories:

DEC  pure decision problems, where the solver must only find a solution but there is no objective function, and no weights.

OPT  an objective function is present which must be optimised but no weights are given to constraints.

SOFT  all weights in the weighted boolean optimisation problem are "soft", i.e., one doesn't use the notion of a "hard" constraint which must be satisfied.

PARTIAL  there is at least one "hard" weighted constraint in the weighted boolean optimisation problem, which must be satisfied.
For each of these, there are the following subcategories:

SMALLINT  the sum of the coefficients in any constraint is less than 2^21.

BIGINT  the sum of the coefficients in at least one constraint is greater than or equal to 2^21.

LIN  all constraints are linear.

NCL  at least one constraint is nonlinear.

MaxSAT competition:

Unweighted MaxSAT where the benchmark is a standard Dimacs CNF and the solver tries to find an assignment which minimises the number of falsified clauses.

Partial MaxSAT where the benchmark is a standard CNF file augmented with "hard" and "soft" indicators which are added as prefixes to each clause, such that the solver must find an assignment which minimises the number of falsified clauses but satisifies all "hard" clauses.

Weighted MaxSAT where each clause in the Dimacs file is prefixed with a positive integer weight and then the solver must find an assignment which minimises the sum of the weights of the clauses falsified by the assignment.

Partial Weighted MaxSAT where clauses are weighted as in weighted MaxSAT but there is a special "top" weight which can be used to denote "hard" clauses which must be satisfied as in partial MaxSAT.
Definition in file SATCompetition.hpp.