generated from satcompetition/template
-
Notifications
You must be signed in to change notification settings - Fork 1
/
index.html
105 lines (95 loc) · 4.3 KB
/
index.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
105
<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
<title class='tpl-name'></title>
<link rel="stylesheet" href="main.css" type="text/css">
<link rel="stylesheet" href="template.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#index { 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 class='tpl-name'></h1>
<h3>
Affiliated with the
<a href="https://www.iiia.csic.es/sat2021/"><span class='tpl-afil'></span></a>
taking place on the <span class='tpl-afil-place'></span>.
</h3>
<p>
<span class='tpl-name'></span> is a competitive event for solvers of the Boolean Satisfiability (SAT) problem.
It is organized as a satellite event to the
<a href="https://sat2020.idea-researchlab.org/"><span class='tpl-afil'></span></a>
and stands in the tradition of the yearly <a href="http://www.satcompetition.org">SAT Competitions and SAT-Races / Challenges</a>.
</p>
<h3><a name="Objective">News</a></h3>
<ul>
<li>[21.04.2022] Parallel and Cloud track solvers sources are now archived and available in the <a href='downloads.html' id='downloads'>downloads section</a> (unfortunatly not all submissions repositories were still online)</li>
<li>[27.08.2021] The <a href='http://hdl.handle.net/10138/333647'>Proceedings of SAT Competition 2021</a> are now available</li>
<li>[12.07.2021] Reuploaded results CSV
<ul>
<li>Replaced all magic numbers >10000 by strings carrying their semantics: "memout", "timeout"</li>
<li>Removed data for disqualified solvers</li>
<li>Fixed scores of VBSs</li>
</ul>
</li>
<li>[12.07.2021] The Cloud track results presented were incorrectly evaluated with respect to a 5000 seconds timeout (instead of 1000 seconds as announced).
This has now been corrected in the <a href='results.html' id='results'>results section</a>
and a corrected set of slides is available in the <a href='downloads.html' id='downloads'>downloads section</a>.
Unfortunately, this has led to a change in the third-placed cloud solver.
</li>
<li>[10.07.2021] The benchmarks and sequential solvers are now available in the <a href='downloads.html' id='downloads'>downloads section</a></li>
<li>[10.07.2021] The detailed results per track are now available in the <a href='results.html' id='results'>results section</a></li>
</ul>
<h3><a name="Objective">Objective</a></h3>
<p>
The area of SAT Solving has seen tremendous progress over the last years.
Many problems (e.g. in hardware and software verification) that seemed to be completely out of reach a decade ago can now be handled routinely.
Besides new algorithms and better heuristics, refined implementation techniques turned out to be vital for this success.
</p>
<p>
To keep up the driving force in improving SAT solvers, we want to motivate implementors to present their work to a broader audience and to compare it with that of others.
</p>
<h3><a name="Tracks">Tracks</a></h3>
<p>
<span class='tpl-name'></span> will consist of the following tracks*:
</p>
<ul>
<li>Main Track (with No-Limits and CaDiCaL-Hack sub-tracks)</li>
<li>Application Track: Cryptography</li>
<li>Incremental Library Track</li>
<li>Parallel Track</li>
<li>Cloud Track</li>
</ul>
<p>* Tracks with less than 3 participants will be canceled.</p>
<h3>Important Dates</h3>
<table>
<tr>
<td>Registration Opens:</td>
<td class="date">March 1</td>
</tr>
<tr>
<td>Benchmark Submission Deadline</td>
<td class="date"><strike>March 31</strike> April 27</td>
</tr>
<tr>
<td>Solver Submission Deadline:</td>
<td class="date"><strike>March 31</strike> April 27</td>
</tr>
<tr>
<td>Announcement of Results:</td>
<td>At the <a href="https://www.iiia.csic.es/sat2021/"><span class='tpl-afil-short'></span></a></td>
</tr>
</table>
<h3><a name="Organization">Organization</a></h3>
<p>
Researchers from both academia and industry are invited to submit their solvers and benchmarks to <span class='tpl-name'></span>.
</p>
</div>
</div>
</body>
</html>