generated from satcompetition/template
-
Notifications
You must be signed in to change notification settings - Fork 0
/
rules.html
168 lines (152 loc) · 8.7 KB
/
rules.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
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
<!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#rules { 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">
<p>
<h2>Mandatory participation requirements for SAT solvers</h2>
<ol>
<li>The source code of submitted SAT solvers must be made available (licensed for research purposes) except for the solvers participating only in the No-Limits Track.
</li>
<li>A 1-2 page system description document (see below for details).
</li>
<li>The co-authors of a solver in the solver description must match the co-authors listed in the submission system.
</li>
<li>SAT solvers must conform to DIMACS input/output requirements
(see <A href="http://www.satcompetition.org/2009/format-benchmarks2009.html">SAT Competition 2009</A> for details).
Printing models in case of a satisfiable instance is required for all tracks expect for "no-limits". Additionally, UNSAT certificates (proofs) are required for the main tracks.
</li>
<li>SAT solvers that are planning to participate in the Main track must be able to produce certificates for UNSAT instances in
tracecheck or DRAT (Delete Resolution Asymmetric Tautologies) format which is backwards compatible with
the <A href="http://www.cs.utexas.edu/~marijn/drup/">DRUP</A> format of SAT Competition 2013.
</li>
<li>
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
<a href="https://www.starexec.org/starexec/public/machine-specs.txt">StarExec cluster</a>).
See the <a href="benchmarks.html">benchmarks page</a> for more information.
</li>
</ol>
</p>
<h2>System Description Document</h2>
<p>
Each entrant to the SAT Competition <b>must include</b> a short (at least 1, at most 2 pages) description of the system.
This should include a list of all authors of the system and their present institutional
affiliations.
It should also provide details of any non-standard algorithmic techniques (e.g., heuristics, simplification/learning techniques, etc.)
and data structures, as well as references to relevant literature (be they by the authors themselves or by others).
The system description must be formatted in <a href="http://www.ieee.org/conferences_events/conferences/publishing/templates.html">IEEE Proceedings style</a>, and submitted as PDF.
The system descriptions will be posted on the SAT Competition website.
Furthermore, given that the quality and number of system descriptions is
high enough, the organizers are considering publishing the collection of
system description as a report under the report series of Department of
Computer Science, University of Helsinki (with ISSN and ISBN numbers).
</p>
<h2>Your E-mail to the Organizers</h2>
<p>
In your registration e-mail to the organizers, please include the following information:
<ol>
<li>the name of the solver</li>
<li>the name(s) of the solver author(s)</li>
<li>the tracks in which the solver is to participate</li>
<li>the benchmarks or a link to the benchmarks (if applicable)</li>
<li>the <b>proof checker</b> to be used for checking unsat proofs (if applicable)</li>
<li>attach the solver description document</li>
<li>attach the benchmark description document (if applicable)</li>
</ol>
</p>
<div>
<h2>Composition of Solvers</h2>
<p>
SAT Competitions stimulate progress in development and implementation of core SAT solving methods.
<b>Pure Portfolio</b> SAT solvers which are a combination of two or more (core) SAT solvers
developed by different groups of authors are <b>not allowed</b> to participate in the competition.
</p>
<p>
Otherwise, composed solvers must have <b>different solving methodologies</b>,
e.g., CDCL, SLS, Lookahead, Groebner Basis, etc., not just different solving strategies.
Exempted from this rule are solvers which are singularly, and completely, written by the author(s).
</p>
<p>
There is no need to acquire permission to use the code or to add the original author(s)
of the composed solvers to the published paper, if the copyright allows for this.
However, doing it as a courtesy is encouraged,
when this does not interfere with the <b>maximal permitted solvers by the authors</b>.
</p>
<p>
<b>The limitations for compositions of solvers do not hold for solvers in the Cloud Track.</b>
</p>
</div>
<!--
<h2>Mandatory participation requirements for benchmarks</h2>
<p>
Submitted benchmarks <b>must</b> be accompanied by a 1-2 page description
(IEEE format, SAT Competition 2014 specific template with instructions on contents
<a href="sc2014-description-template.tgz">is available here</a>).
This should include a list of all authors of the system and their present institutional affiliations. It should also provide details of any non-standard algorithmic techniques (e.g., heuristics, simplification/learning techniques, etc.) and data structures. The system description must be formatted in IEEE Proceedings style, and submitted as PDF. The system descriptions will be posted on the SAT Challenge 2012 website. Following <a href="http://hdl.handle.net/10138/34218">SAT Challenge 2012</a>, the organizers are considering publishing the collection of system description as a report under the report series of Department of Computer Science, University of Helsinki (with ISSN and ISBN numbers).
</p>
-->
<h2>Qualification</h2>
<p>
There will be no qualification round, but only a testing round to ensure that solvers are running properly
on the evaluation system. The test set of instances will consist in a random selection of instances from
the last SAT Competitions. The organizers reserve the right to disqualify poorly performing solvers.
</p>
<h2>Disqualification</h2>
<p>
A SAT solver will be disqualified if the solver produces a wrong answer. Specifically, if a solver
reports UNSAT on an instance that was proven to be SAT by some other solver, or SAT and provides a
wrong certificate. A solver disqualified from the competition is not eligible to win any award.
Disqualified solvers will be marked as such on the competition results page.
</p>
<p>
Note that there is a dedicated period when the participants can check their results to ensure
that no problems are caused by the competition framework.
</p>
<!--
<h2>Certified UNSAT tracks</h2>
<p>
The sequential UNSAT tracks for core solvers are certified, similar to SAT Competition 2013.
In order to participate in these tracks, solvers are required to emit an unsatisfiability proof.
The proofs format of the certified UNSAT tracks is DRAT (Delete Resolution Asymmetric Tautologies)
which is backward compatible with <A href="http://www.cs.utexas.edu/~marijn/drup/">DRUP</A>
(Delete Reverse Unit Propagation) and RUP (Reverse Unit Propagation).
In the certified UNSAT tracks, only benchmarks are counted for which the solver emitted a DRAT proof
that can be verified by a <A href="http://www.cs.utexas.edu/~marijn/drat-trim/">DRAT-trim</A> checker
provided by the organization. A proof that is discarded by the checker will not result in disqualification of the solver.
</p>
-->
<h2>Withdrawal</h2>
<p>
A solver can be withdrawn from the SAT Competition only before the deadline for the submission
of the final versions. After this deadline no further changes or withdrawals of the solvers are possible.
</p>
<h2>Participation of the organizers</h2>
<p>
The organizers of this SAT Competition are not allowed to compete.
</p>
<h2 id="num">Number of submissions</h2>
<p>
Each participant is restricted to be a co-author of at most four different sequential solvers in the Main track, one CaDiCaL hack-track submission,
two different parallel solvers in the Parallel track, and one solver in the Cloud track.
Two solvers are different as soon as their sources differ or the compilation options are different.
Solvers are also different if they use different command line options.
However, we make an exception for a command line option that enables emitting UNSAT proofs for the certified UNSAT tracks.
Authors can select per solver whether to participate in a track or not.
</p>
</div>
</div>
</body>
</html>