index.html

<!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#index { 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">
	SAT Competition 2023 is a competitive event for solvers of the Boolean Satisfiability (SAT) problem.
	The competition is organized as a satellite event to the <a href="http://satisfiability.org/SAT23/">SAT Conference 2023</a>
	and continues the series of the annual <a href="http://www.satcompetition.org">SAT Competitions and SAT-Races / Challenges</a>.
	
	<h3><a name="Objective">Objective</a></h3>
	<p>
	The area of SAT Solving has seen tremendous progress over the last years.
	Many problems that seemed to be 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.
	To keep up the driving force in improving SAT solvers, we want to motivate implementers to present their work to a broader audience 
	and to compare it with that of others.
	Researchers from both academia and industry are invited to submit their solvers and benchmarks.
	</p>

	<h3 id="news">News</h3>
	<ul>
		<li><b>2023-08-11</b>
			The <a href="https://researchportal.helsinki.fi/en/publications/proceedings-of-sat-competition-2023-solver-benchmark-and-proof-ch">
				Proceedings of SAT Competition 2023
			</a> are published. 
		</li>
		<li><b>2023-07-19</b>
			The plots in the <a href="downloads/satcomp23slides.pdf">slides</a> are now updated to reflect the changes in the parallel tracks (cf. 2023-07-15 news). 
		</li>
		<li><b>2023-07-17</b>
			<a href="downloads/selection23.tar.xz">The script and dataset used to compile the benchmarks is now available for download.</a>
		</li>
		<li><b>2023-07-15</b>
			Due to fixing a bug in our data processing pipeline, the scores in the parallel and cloud tracks have changed. 
			Unfortunately, the fix also results in a change in the rankings in the parallel UNSAT track, where first and second place had to be swapped. 
			This caused updates in the <a href="downloads/sc2023-detailed-results.zip">detailed results</a> and the scores on the <a href="downloads/satcomp23slides.pdf">slides</a>.
		</li>
		<li><b>2023-07-07</b>
			<a href="downloads/sc2023-detailed-results.zip">Detailed results (per instance runtimes) are available for download</a>
		</li>
		<!--<li><b>2023-07-07</b> 
			<a href="downloads/sc2023-proceedings-draft.pdf">A draft of the proceedings with all solver and benchmark descriptions is available for download</a>. 
			Please contact the organizers in case you have any comments. 
			The proceedings will be finalized by the end of July. 
			Please do not link directly to this draft version, as it will be removed within the next couple of weeks.
		</li>-->
		<li><b>2023-07-07</b> 
			<a href="downloads/satcomp23slides.pdf">The slides with the presentation of results are available for download</a>
		</li>
		<li><b>2023-03-07</b> <a href="starexec.html#testing2">Read the updated submission guidelines for selecting a proof checker</a></li>
		<li><b>2023-03-01</b> <a href="checkers.html">The documentation of the proof-format used by VeriPB is now available</a></li>
		<li><b>2023-02-15</b> We are currently experiencing sporadic problems with our email-address <a href="mailto:organizers@satcompetition.org">organizers@satcompetition.org</a>
			due to shared IP-addresses being black-listed by dynamic spam-filters. 
			If you experience issues with emails bouncing off or if you just want to make sure to reach us, 
			then please send your email directly to <a href="organizers.html">all the organizers</a>
		</li>
		<li><b>2023-02-10</b> <a href="index.html#dates">We released the Timeline</a></li>
		<li><b>2022-12-06</b> We have an open <a href="call.html">Call for Verified Proof Checkers</a></li>
	</ul>

	<h3><a name="Tracks">Tracks</a></h3>
	<ul>
		<li><a href="tracks.html#main">Main Track</a>
			<ul>
				<li><a href="tracks.html#special">Opportunity to choose from several different proof checkers</a></li>
				<li><a href="tracks.html#hack">CaDiCaL Hack Track</a></li>
				<li><a href="tracks.html#nolimits">No-Limits Track</a></li>
			</ul>
		</li>
		<li><a href="tracks.html#parallel">Parallel Track</a></li>
		<li><a href="tracks.html#cloud">Cloud Track</a></li>
	</ul>

	<h3 id="dates">Important Dates</h3>
	<table>
	  <tr>
		<td>Registration Opens:</td>
		<td class="date">April 1st</td>
	  </tr>
	  <tr>
		<td>Benchmark Submission / Solver Registration Deadline:</td>
		<td class="date"><strike>April 15th</strike> April 30th</td>
	  </tr>
	  <tr>
		<td>Solver Submission Deadline:</td> 
		<td class="date"><strike>April 15th</strike> April 30th</td>
	  </tr>
	  </tr>
	  <tr>
		<td>Announcement of Results:</td> 
		<td class="date">July 8th at <a href="http://satisfiability.org/SAT23/">SAT Conference 2023</a></td>
	  </tr>
	</table>
  </div>
</div>
</body>
</html>