2017/welcome.html at main · satcompetition/2017 · GitHub

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
<h3>
Affiliated with the
  <a href="http://sat2017.gitlab.io/">20th International Conference on Theory and Applications of Satisfiability Testing</a><br/>
taking place on the 28th August - 1st of September in Melbourne, Australia.
</h3>

<p>
The 2017 SAT Competition is a competitive event for solvers of the Boolean Satisfiability (SAT) problem.
It is organized as a satellite event to the
<a href="http://sat2017.gitlab.io/">20th International Conference on Theory and Applications of Satisfiability Testing</a>
and stands in the tradition of the yearly <a href="http://www.satcompetition.org">SAT Competitions</a> and <a href="previous.html">SAT-Races / Challenges</a>.
</p>

<h3><a style="color:red" name="News">News</a></h3>
<p>
<ul>
<li>BYOB - Bring your own <strike>Beer</strike> Benchmarks: 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 <a href="https://www.starexec.org/starexec/public/machine-specs.txt">nodes of the StarExec cluster</a>).
See <a href="http://baldur.iti.kit.edu/sat-competition-2017/benchmarks.html">the benchmarks page</a> for more information.
</li>
<li>The solvers will ranked using the PAR-2 scheme: The score of a solver is defined as the sum of all runtimes for solved instances + 2*timeout for unsolved instances, lowest score wins.</li>
<li>The IPASIR interface for the Incremental Track is updated, click <a href="http://baldur.iti.kit.edu/sat-competition-2017/incremental.html">here</a> for details. </li>
</ul>
</p>

<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>
SAT Competition 2017 will consist of the following tracks*:
</p>
<ul>
  <li>Main Track (with a Glucose-Hack award)</li>
  <li>Parallel Track</li>
  <li>Incremental Library Track</li>
  <li>Agile Track</li>
  <li>Random Satisfiable Track</li>
  <li>No-Limits 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">1st May, 2017</td>
  </tr>
  <tr>
    <td>Benchmark Submission Deadline</td>
    <td class="date"><del>May 15</del> <del>June 1</del> <font color="red">June 10, 2017</font></td>
  </tr>
  <tr>
    <td>Solver Submission Deadline:</td>
    <td class="date"><del>May 15</del> <del>June 1</del> <font color="red">June 10, 2017</font></td>
  </tr>
  <tr>
    <td>Announcement of Results:</td>
    <td>At the <a href="http://sat2017.gitlab.io/">SAT'17 Conference</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 SAT Competition 2017.
</p>