update more self-contained regarding io formats

README.md

@@ -16,17 +16,16 @@ The 2024 SAT Competition will consist of the following tracks:
 
 ## New This Year
 
-**New SAT Checker**
+**Partial satisfying assignments allowed**
 
-We will replace the satisfying assignments checker that has traditionally been used in SAT competitions with a new checker that is part of the verified GRAT checker. 
-This will allow partial models to be accepted as long as every clause of the original SAT instance is satisfied.
+We will replace the satisfying assignments checker that has traditionally been used in SAT competitions. This will allow partial models to be accepted as long as every clause of the original SAT instance is satisfied. See also https://satcompetition.github.io/2024/output.html#satassign
 
 
 ## Aspects to Highlight
 
 **Bring Your Own Benchmarks (BYOB)**
 
-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 (i.e., not solved by MiniSat within one minute on modern hardware) or not too hard (unsolvable by the participant's own solver within one hour on a computer similar to the nodes of the StarExec cluster).
+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 neither be too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour).
 
 **PAR-2 Scoring Scheme**
 

benchmarks.html

@@ -24,23 +24,22 @@ <h4>Benchmark Submission</h4>
 	</p>
 	<p>
 	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>).
+	At least 10 of those benchmarks should neither be too easy (solvable by MiniSat in a minute) or too hard (unsolvable by the participants own solver within one hour).
 	</p>
-	<p>
-	Participants should submit benchmarks by emailing them to "[email protected]" with the 
-	subject "SAT Competition Benchmark Submission" and either a URL link or attachment of a single archive containing the benchmarks.
-	</p>
-
-	<h4>Input and Output Format</h4>
-	<p>
-	Benchmarks have to be formatted according to the
-	<a href="http://www.satcompetition.org/2011/format-benchmarks2011.html">SAT Competition 2011 Benchmark Submission Guidelines</a>.
 	A 1-2 page benchmark description document, using the <a href="http://www.ieee.org/conferences_events/conferences/publishing/templates.html">IEEE Proceedings style</a>,
-	must be submitted with each submitted benchmark family, following the instructions for solver descriptions.
+	must be submitted with each submitted benchmark family.
 	The benchmark descriptions will be made available similarly as the solver descriptions (see <a href="rules.html">general rules</a>).
-	</p>
+
+	<h4>Input and Output Format</h4>
+ 	The benchmark file can start with <i>comment lines</i>, i.e. lines beginning with the character <i>c</i>. 
+	After the comments, there is the line <i>p cnf nbvar nbclauses</i> that indicates that the instance is in CNF format, where <i>nbvar</i> is the exact number of variables appearing in the file, and <i>nbclauses</i> is the exact number of clauses contained in the file. 
+	Then the clauses follow. Each clause is a sequence of distinct non-null numbers between -nbvar and nbvar ending with 0 on the same line. 
+	A clause must not contain the opposite literals i and -i simultaneously. 
+	Positive numbers denote the corresponding variables. 
+	Negative numbers denote the negations of the corresponding variables.
+
+	<!-- Benchmarks have to be formatted according to the
+	<a href="http://www.satcompetition.org/2011/format-benchmarks2011.html">SAT Competition 2011 Benchmark Submission Guidelines</a>. -->
 
 	<h4>Benchmark Selection</h4>
 	<p>

index.html

@@ -33,19 +33,18 @@ <h3><a name="Objective">Objective</a></h3>
 	<h3 id="news">News</h3>
 	<ul>
 		<li><b>2024-01-26</b>
-			We will replace the satisfying assignments checker that has traditionally been used in SAT competitions with a new checker that is part of the verified GRAT checker. 
-This will allow partial models to be accepted as long as every clause of the original SAT instance is satisfied.
+			We will replace the satisfying assignments checker that has traditionally been used in SAT competitions. This will allow <a href="output.html#satassign">partial models to be accepted</a> as long as every clause of the original SAT instance is satisfied.
 		<li><b>2024-01-22</b>
 			The competition website is online.
 		</li>
 	</ul>
 
 	<h3><a name="Tracks">Tracks</a></h3>
 	<ul>
-		<li><a href="tracks.html#main">Main Track</a>
+		<li><a href="tracks.html#main">Main Track</a>, including subtracks:
 			<ul>
 				<li><a href="tracks.html#hack">CaDiCaL Hack Track</a></li>
-				<li><a href="tracks.html#nolimits">No-Limits 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>

navigation.html

@@ -4,7 +4,7 @@
 <a href='tracks.html' id='tracks'>Competition Tracks</a><br>
 <a href='rules.html' id='rules'>Solver Submission</a><br>
 <ul>
-    <li><a href='certificates.html' id='certificates'>UNSAT Certificates</a></li>
+    <li><a href='output.html' id='output'>Output Format</a></li>
     <li><a href='starexec.html' id='starexec'>StarExec Cluster</a></li>
     <li><a href='aws.html' id='aws'>AWS Cloud</a></li>
 </ul>

certificates.html → output.html

@@ -6,7 +6,7 @@
 <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#certificates { color:var(--link-color-2); }</style>
+<style>a#output { color:var(--link-color-2); }</style>
 </head>
 
 <body>
@@ -16,12 +16,38 @@
   <script>w3.includeHTML();</script> 
 
   <div class="content">
-	<h2>Certified UNSAT</h2>
-	All participants in the Main track of this competition are required to output certificates of unsatisfiablity. 
-	Certificates of unsatisfiability have been required for the UNSAT tracks since SAT Competition 2013. 
-	As of SAT Competition 2023, participants can select from several proof systems and formats. 
-	<br>
-	The following proof checkers are provided and described in the respective documents. 
+	<h2 id="output">Output Format</h2>
+	All solver output on stdout must either be a <b>comment line</b>, a <b>solution line</b>, or a <b>value line</b>. 
+	Comment lines start with a lower case "c" followed by a space. 
+	Comments are optional and may appear anywhere in the solver output.
+	The solution line is mandatory and must appear exactly once. 
+	The solution line starts with a lower case "s" followed by a space.
+	It must be one of the following answers:
+	<ul>
+	<li><tt>s SATISFIABLE</tt><br>
+		This indicates that the solver has found a model of the formula. 
+		In such a case, if the track requires <a href="output.html#satassign">satisfying assignments</a>, one or multiple value lines are mandatory.
+	</li>
+	<li><tt>s UNSATISFIABLE</tt><br> 
+		This indicates that the solver has proof that the formula has no model. 
+		In such a case, if the track requires <a href="output.html#unsatcert">UNSAT certificates</a>, the proof must be written to a file called "proof.out", which is then passed to the verifier.
+	</li>
+	<li><tt>s UNKNOWN</tt><br>
+		This line must be output in any other case, i.e. when the solver is not able to tell anything about the formula.
+	</li>
+	</ul>
+
+	<h2 id="satassign">Satisfying Assignment</h2>
+	Value lines start with a lower case "v" followed by a space and must be ended by a "0" zero. 
+	Values are given as a space-separated list of non-contradictory literals. 
+	The negation of a literal is denoted by a minus sign immediately followed by the identifier of the variable. 
+	Value lines provide a model (or an implicant) of the instance, and it is NOT necessary to list the literals corresponding to all variables if a smaller amount of literals suffices to satisfy all clauses. 
+	The order of the literals does not matter. 
+	More than one value line is allowed and even necessary if the output would otherwise exceed the maximum line length of 4096 characters. 
+
+	<h2 id="unsatcert">Certificates of Unsatisfiablity</h2>
+	All participants in the Main track of this competition are required to output certificates of unsatisfiablity which must be written to a file called "proof.out". 
+	Participants can select from the following proof checkers, which are described in the respective documents. 
 	<ul>
 	<li>
 		<a href="downloads/checkers/cakelpr.pdf">Verified LRAT and LPR Proof Checking with cake_lpr</a></br>

rules.html

@@ -18,20 +18,13 @@
   <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.
+	<ul>
+	<li>The source code of submitted SAT solvers must be made available (licensed for research purposes) except for the solvers participating only in the <a href="tracks.html#nolimits">No-limits Track</a>.
 	</li>
-	<li>A 1-2 page system description document (see below for details).
+	<li>A <a href="rules.html#systemdecription">system description document</a> must be submitted with your <a href="rules.html#registration">registration e-mail</a>. The co-authors of a solver in the system description document must match the co-authors listed in your registration e-mail. 
 	</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>
+	Printing a <a href="output.html#satassign">model in case of a satisfiable instance</a> is required for all tracks expect for "No-limits". Additionally, <a href="output.html#unsatcert">UNSAT certificates (proofs)</a> are required for the Main track.
 	</li>
 	<li>
 	Each Main Track participant (team) is required to submit 20 new benchmark instances (not seen in previous competitions). 
@@ -40,10 +33,10 @@ <h2>Mandatory participation requirements for SAT solvers</h2>
 	<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>
+	</ul>
 	</p>
 
-	<h2>System Description Document</h2>
+	<h2 id="systemdecription">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
@@ -58,42 +51,43 @@ <h2>System Description Document</h2>
 	Computer Science, University of Helsinki (with ISSN and ISBN numbers).
 	</p>
 
-	<h2>Your E-mail to the Organizers</h2>
+	<h2 id="registration">Solver Registration</h2>
 	<p>
-	In your registration e-mail to the organizers, please include the following information:
-	<ol>
+	Your registration e-mail to the organizers should include the following:
+	<ul>
 	<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>	
+	<li>the solver description document</li>
+	<li>if applicable, the benchmarks or a link to the benchmarks, and the benchmark description document</li>
+	<li>if applicable, the proof checker to be used for checking unsat proofs</li>
+	</ul>	
 	</p>
 
-<div>
-	<h2>Composition of Solvers</h2>
+
+	<h2 id="composition">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>, 
+	Pure Portfolios which are a combination of two or more (core) SAT solvers 
+	developed by different groups of authors are not allowed to participate in the competition.
+	Otherwise, solver compositions must have different solving methodologies, 
 	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. 
+	Exempted from this rule are solvers which are singularly and completely written by the author(s).
+	If the copyright allows for this, 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. 
     However, doing it as a courtesy is encouraged, 
-    when this does not interfere with the <b>maximal permitted solvers by the authors</b>.
+    when this does not interfere with the maximal permitted solvers by the authors.
+	<b>The limitations for compositions of solvers do not hold for solvers in the Cloud Track.</b>
 	</p>
+
+	<h2 id="num">Number of submissions</h2>
 	<p>
-		<b>The limitations for compositions of solvers do not hold for solvers in the Cloud Track.</b>
+	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.
+	Authors can select per solver whether to participate in a track or not.
 	</p>
-</div>
 
 	<!--
 	<h2>Mandatory participation requirements for benchmarks</h2>
@@ -114,54 +108,23 @@ <h2>Qualification</h2>
 	</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>

tracks.html

@@ -28,7 +28,7 @@ <h3 id="main">Main Track</h3>
 		The solvers will be allowed to use up to 128GB of RAM.
 		All solvers participating in the Main track are required to provide certificates in both SAT and UNSAT cases. 
 		Like last year, we will offer to choose from different proof checkers.
-		For more information about the UNSAT certificates see <a href="certificates.html">this page</a>.
+		For more information about the UNSAT certificates see <a href="output.html#unsatcert">this page</a>.
 
 	<h4 id="hack">CaDiCaL 1.9.4 Hacks</h4>
 		We encourage CaDiCaL Hack authors to participate in the Main track. 
@@ -48,11 +48,9 @@ <h4 id="hack">CaDiCaL 1.9.4 Hacks</h4>
 		You can use our <a href="downloads/editdistance.zip">edit distance tool</a> on all modified files to count the number of modifications.
 		</p>
 
-	<h4 id="nolimits">No-Limits Track</h4>
-		If your solver does not generate SAT or UNSAT certificates or if you do not want to publish your source code, 
-		you can still submit your solver to the No-Limits track. 
-		<p>Each solver submitted to the Main track will automatically participate in the No-Limits track. </p>
-		<p>The No-Limits track will only be evaluated with respect to the <i>new</i> benchmarks instances which are submitted to this SAT Competition.</p>
+	<h4 id="nolimits">No-limits Track</h4>
+		If your solver does not generate result certificates or if the source code of your solver can not be public, you can submit your solver to the No-limits track. 
+		Submissions to the No-limits track will only be evaluated on the <i>new</i> benchmark instances submitted to this SAT competition and must outperform the top three solvers of the Main track on those instances to receive an award.
 
 	<h3 id="parallel">Parallel Track</h3>
 		The Parallel track will be run on Amazon Web Services (AWS).