SATCompetition.hpp File Reference

Plans regarding SAT competitions. More...

Go to the source code of this file.

Detailed Description

Plans regarding SAT competitions.

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 cleaned-up; most of them removed (possible with transfer to docus).
Benchmarks for SAT 2012
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 k-SAT 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 sub-categories:
      • 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 non-linear.
  • 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.