generated from satcompetition/template
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathtracks.html
104 lines (94 loc) · 6.35 KB
/
tracks.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title>SAT Competition</title>
<link rel="stylesheet" href="main.css" type="text/css">
<link rel="icon" type="image/x-icon" href="doge2.ico">
<script src="https://www.w3schools.com/lib/w3.js"></script>
<style>a#tracks { color:var(--link-color-2); }</style>
</head>
<body>
<div class="main">
<div class="navigation" w3-include-html="navigation.html"></div>
<div class="heading" w3-include-html="heading.html"></div>
<script>w3.includeHTML();</script>
<div class="content">
<h2>Competition Tracks</h2>
<p>
The Main track as well as its subtracks will be run on the <a href="https://www.starexec.org/starexec/public/about.jsp">StarExec cluster</a>.
The time limit for solving an instance will be 5000 seconds (in each track).
The solvers will be allowed to use up to 128GB of RAM.
</p>
<p>
Printing a model in case of a satisfiable instance is required for all tracks.
UNSAT certificates (proofs) are required only in the main tracks.
</p>
<h3 id="anniversary">Anniversary Track</h3>
<p>
International competitions for SAT solvers have a long tradition.
The first sporadic events took place in the 1990s (Paderborn 1992, DIMACS 1993, and Beijing 1996).
In 2002, Edward A. Hirsch, Daniel Le Berre, and Laurent Simon initiated a series of regularly scheduled competitions: the SAT Competition as we know it.
Today, we can look back on 20 years of exciting public evaluations and award ceremonies; 20 years of SAT competitions that testify to the tremendous scientific progress made in SAT solving.
</p>
<p>
We celebrate the 20th anniversary of this event series in the form of a special Anniversary track.
The benchmarks for this track will be comprised of <i>all benchmark instances</i> which have been used in Application, Crafted, and Main Tracks of previous SAT competitions.
</p>
<p>
There will be three categories of this track, one each for Main track, Parallel track and Cloud track solvers.
Participants can submit a maximum of two solvers to the Main category of this track, and one solver for each of the Parallel and Cloud categories.
We particularly welcome you to also submit solvers or configurations which are tailored to specific instance types.
</p>
<p>
All submissions to the Anniversary track have to be open source.
Solvers which contain code which could be perceived as instance-specific branching or a result-lookup table will be disqualified.
If you are unsure whether your solver meets these requirements, please feel free to contact us.
</p>
<h3 id="main">Main Track</h3>
Main track is the track for sequential SAT solvers.
This track will be run on the StarExec Cluster.
Consider the <a href="rules.html">general submission guidelines</a> and the <a href="starexec.html">StarExec submission instructions</a>.
We will use 300-600 benchmark problems, the time limit will be 5000 seconds.
All solvers participating in the Main track are required to provide certificates in both SAT and UNSAT cases.
For more information about the UNSAT certificates see <a href="certificates.html">this page</a>.
<h4 id="hack">CaDiCaL 1.4.1 Hacks</h4>
We encourage CaDiCaL Hack authors to participate in the Main track.
A prize will be awarded to the best CaDiCaL hack.
<p>
Hack tracks have been part of many SAT Competition since 2009.
The motivation of hack tracks is two-fold.
On the one hand, we want to lower the threshold for Master and PhD students to enter the SAT Competition with new and innovative ideas.
On the other hand, the aim is to see how far the performance of CaDiCaL can be improved by making only minor changes to its source code.
Competing with minor hacks helps the community to isolate the actual causes of improvements.
Thus, we strongly encourage all participants of the Main track (including non-students) to participate with a "hacked" CaDiCaL solver.
</p>
<p>
Participants in the CaDiCaL Hack track should use the source of the newly released <a href="https://github.com/arminbiere/cadical/tree/rel-1.4.1">CaDiCaL 1.4.1</a>.
These sources include a comfortable <a href="https://github.com/arminbiere/cadical/blob/rel-1.4.1/scripts/prepare-sc2021-submission.sh">script for preparing the submission for StarExec</a>.
In order to qualify as a CaDiCaL Hack, the diff between the patched and modified sources of CaDiCaL 1.4.1 has to be less than 1000 non-space characters.
You can use our <a href="downloads/editdistance.zip">edit distance tool</a> on all modified files to count the number of modifications.
</p>
<h4 id="nolimits">No-Limits Track</h4>
If your solver does not generate UNSAT proofs or if you do not want to publish your source code,
you can still submit your solver to the No-Limits track.
<p>Each solver submitted to the Main track will automatically participate in the No-Limits track. </p>
<p>The No-Limits track will only be evaluated with respect to the new benchmarks instances which are submitted to this SAT Competition.</p>
<h3 id="parallel">Parallel Track</h3>
The Parallel track will be run on Amazon Web Services (AWS).
Consider the <a href="rules.html">general submission guidelines</a> and the <a href="aws.html">AWS submission instructions</a>.
The solvers participating in this track will be executed with a wall-clock time limit of 5000 seconds.
Each solver will be run an a single AWS machine of the type m4.16xlarge, which has 64 virtual cores and 256GB of memory.
More details about m4.16xlarge nodes can be found
<a href="https://aws.amazon.com/about-aws/whats-new/2016/09/introducing-new-m4-instance-size-m4-16xlarge-and-new-region-availability-of-m4-instances/">here</a>.
<h3 id="cloud">Cloud Track</h3>
The Cloud track will evaluate the effectiveness of parallel SAT solvers to run in a distributed manner.
This track will be run on Amazon Web Services(AWS).
Consider the <a href="rules.html">general submission guidelines</a> and the <a href="aws.html">AWS submission instructions</a>.
The solvers participating in this track will be executed with a wall-clock time limit of 1000 seconds running on 100 m4.4xlarge machines in parallel.
Each m4.4xlarge machine has 16 virtual CPUs and 64 GB memory.
Communication between the machines is possible using MPI and SSH.
</div>
</div>
</body>
</html>