From 7adbcb6a4d7e1365a8fc3abc20b415df9fd32732 Mon Sep 17 00:00:00 2001 From: Markus Iser Date: Mon, 5 Feb 2024 12:43:34 +0100 Subject: [PATCH] update more self-contained regarding io formats --- README.md | 7 +-- benchmarks.html | 27 +++++---- index.html | 7 +-- navigation.html | 2 +- certificates.html => output.html | 40 ++++++++++--- rules.html | 99 ++++++++++---------------------- tracks.html | 10 ++-- 7 files changed, 88 insertions(+), 104 deletions(-) rename certificates.html => output.html (78%) diff --git a/README.md b/README.md index e17d51d..ef4e016 100644 --- a/README.md +++ b/README.md @@ -16,17 +16,16 @@ The 2024 SAT Competition will consist of the following tracks: ## New This Year -**New SAT Checker** +**Partial satisfying assignments allowed** -We will replace the satisfying assignments checker that has traditionally been used in SAT competitions with a new checker that is part of the verified GRAT checker. -This will allow partial models to be accepted as long as every clause of the original SAT instance is satisfied. +We will replace the satisfying assignments checker that has traditionally been used in SAT competitions. This will allow partial models to be accepted as long as every clause of the original SAT instance is satisfied. See also https://satcompetition.github.io/2024/output.html#satassign ## Aspects to Highlight **Bring Your Own Benchmarks (BYOB)** -Each Main track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). At least 10 of those benchmarks should be "interesting": not too easy (i.e., not solved by MiniSat within one minute on modern hardware) or not too hard (unsolvable by the participant's own solver within one hour on a computer similar to the nodes of the StarExec cluster). +Each Main Track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). At least 10 of those benchmarks should neither be too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour). **PAR-2 Scoring Scheme** diff --git a/benchmarks.html b/benchmarks.html index d173a16..3578b65 100644 --- a/benchmarks.html +++ b/benchmarks.html @@ -24,23 +24,22 @@

Benchmark Submission

Each Main Track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). - At least 10 of those benchmarks should be "interesting": not too easy (solvable by MiniSat in a minute) or - too hard (unsolvable by the participants own solver within one hour on a computer similar to the nodes of the - StarExec cluster). + At least 10 of those benchmarks should neither be too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour).

-

- Participants should submit benchmarks by emailing them to "organizers@satcompetition.org" with the - subject "SAT Competition Benchmark Submission" and either a URL link or attachment of a single archive containing the benchmarks. -

- -

Input and Output Format

-

- Benchmarks have to be formatted according to the - SAT Competition 2011 Benchmark Submission Guidelines. A 1-2 page benchmark description document, using the IEEE Proceedings style, - must be submitted with each submitted benchmark family, following the instructions for solver descriptions. + must be submitted with each submitted benchmark family. The benchmark descriptions will be made available similarly as the solver descriptions (see general rules). -

+ +

Input and Output Format

+ The benchmark file can start with comment lines, i.e. lines beginning with the character c. + After the comments, there is the line p cnf nbvar nbclauses that indicates that the instance is in CNF format, where nbvar is the exact number of variables appearing in the file, and nbclauses is the exact number of clauses contained in the file. + Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line. + A clause must not contain the opposite literals i and -i simultaneously. + Positive numbers denote the corresponding variables. + Negative numbers denote the negations of the corresponding variables. + +

Benchmark Selection

diff --git a/index.html b/index.html index e6b75f4..189941c 100644 --- a/index.html +++ b/index.html @@ -33,8 +33,7 @@

Objective

News