-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathtracks.html
69 lines (61 loc) · 3.52 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
<!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 2020</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:#c20114; }</style>
</head>
<body>
<div class="main">
<div class="navigation" w3-include-html="navigation.html"></div>
<script>w3.includeHTML();</script>
<div class="content">
<h1>SAT Competition 2020</h1>
<h2>Description of Tracks</h2>
The following tracks will be featured in 2020 SAT Competition.
<ul>
<li><a href='track_main.html' style='font-weight:bold'>Main Track</a> is the track of sequential SAT solvers. 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>.
<ul>
<li>We encourage <a href='track_hack.html' style='font-weight:bold'>Glucose Hack</a> authors to participate in the main track. A prize will be awarded to the best Glucose hack.</li>
<li><span style='color:#c20114'>New this year</span> is the <a href='track_planning.html' style='font-weight:bold'>Planning Track</a>, which is the track for SAT solvers good on instances encoding AI planning problems.</li>
<li>If your solver can not produce UNSAT certificates you can still participate in the <a href='track_nolimits.html' style='font-weight:bold'>No Limits Track</a>.</li>
</ul>
</li>
<li><a href='track_incremental.html' style='font-weight:bold'>Incremental Library Track</a> is for incremental SAT solvers and will be revived this year.</li>
<li>We will also have the <a href='track_parallel.html' style='font-weight:bold'>Parallel Track</a> again.</li>
<li>Another <span style='color:#c20114'>new track</span> is in this competition is the <a href='track_cloud.html' style='font-weight:bold'>Cloud Track</a> for massively parallel SAT solvers using up to 1024 cores.</li>
</ul>
<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>
<h2>Execution Environment</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 <s>24GB</s> <span style="color:#c20114">128GB</span> of RAM.
</p>
<p>
The Incremental Library Track will be run on computers with 2 x Intel Xeon E5430 2.66 GHz (4-Core) processors and 24GB of RAM.
</p>
<!--<p>The Parallel Track will be run on computers with Dual Socket
Xeon E5-2690 v3 (Haswell) : 12 cores per socket (24 cores/node), 2.6 GHz processors and
64 GB DDR4-2133 (8 x 8GB dual rank x8 DIMMS) main memory.
Hyperthreading is Enabled - 48 threads (logical CPUs) per node.
Compute nodes lack a local disk, but users have access to a 32 GB /tmp
RAM disk to accelerate IO operations. Note that any space taken in
/tmp will decrease the total amount of memory available on the node.
If 8 GB of data are written to /tmp the maximum memory available for
applications and OS on the node will then be 64 GB - 8 GB = 56GB.
</p>
<h2>Awards</h2>
tba.-->
</div>
</div>
</body>
</html>