Add support for "knf" format.

potassco · Feb 19, 2025 · f922152 · f922152
1 parent cf8ecfd
commit f922152
Show file tree

Hide file tree

Showing 4 changed files with 38 additions and 8 deletions.
diff --git a/CHANGES b/CHANGES
@@ -9,6 +9,7 @@ clasp 3.4.0:
   * added number of blocked restarts to stats
   * reworked dynamic/blocked restarts and added support for different moving averages
   * added support for pb-constraints in [w]cnf+ format
+  * added support for "knf" format (see https://github.com/jreeves3/LiteralSorting?tab=readme-ov-file#knf-format)
   * addressed issue https://github.com/potassco/clasp/issues/107
   * added additional timing info to output (see https://github.com/potassco/clasp/issues/108)
   * "tweety" asp options are now applied when using config "many"

diff --git a/clasp/parser.h b/clasp/parser.h
@@ -153,6 +153,7 @@ class DimacsReader : public SatReader {
 private:
 	void parsePbConstraint(WeightLitVec& scratch, int64_t maxV);
 	void parseConstraintRhs(WeightLitVec& lhs);
+	void parseAtLeastK(WeightLitVec& scratch, int64_t maxV);
 	SatBuilder* program_;
 	Var         numVar_;
 	bool        wcnf_;

diff --git a/src/parser.cpp b/src/parser.cpp
@@ -294,16 +294,17 @@ bool DimacsReader::doAttach(bool& inc) {
 	if (!accept(peek(false))) { return false; }
 	skipLines('c');
 	require(match("p "), "missing problem line");
-	wcnf_ = match("w");
-	require(match("cnf", false), "unrecognized format, [w]cnf expected");
-	plus_ = match("+", false);
+	bool knf = match("knf");
+	wcnf_ = !knf && match("w");
+	require(knf || match("cnf", false), "unrecognized format, [w]cnf expected");
+	plus_ = !knf && match("+", false);
 	require(stream()->get() == ' ', "invalid problem line: expected ' ' after format");
 	numVar_     = matchPos(ProgramParser::VAR_MAX, "#vars expected");
 	uint32 numC = matchPos("#clauses expected");
 	wsum_t cw   = 0;
-	while (stream()->peek() == ' ')  { stream()->get(); };
+	while (stream()->peek() == ' ')  { stream()->get(); }
 	if (wcnf_ && peek(false) != '\n'){ stream()->match(cw); }
-	while (stream()->peek() == ' ')  { stream()->get(); };
+	while (stream()->peek() == ' ')  { stream()->get(); }
 	require(stream()->get() == '\n', "invalid extra characters in problem line");
 	program_->prepareProblem(numVar_, cw, numC);
 	if (options.anyOf(ParserOptions::parse_full)) {
@@ -323,15 +324,18 @@ bool DimacsReader::doParse() {
 				require(lit >= -maxV && lit <= maxV, "invalid variable in clause");
 				cc.push_back(toLit(static_cast<int32>(lit)));
 			}
-			if (lit == 0) { program_->addClause(cc, cw); }
-			else {
-				require(plus_, "invalid character in clause - '0' expected");
+			if      (lit == 0) { program_->addClause(cc, cw); }
+			else if (card)     {
 				wlc.clear();
 				for (LitVec::const_iterator it = cc.begin(), end = cc.end(); it != end; ++it) {
 					wlc.push_back(WeightLiteral(*it, 1));
 				}
 				parseConstraintRhs(wlc);
 			}
+			else {
+				require(cc.empty() && !wcnf_ && match("k "), "invalid character in clause - '0' expected");
+				parseAtLeastK(wlc, maxV);
+			}
 		}
 		else {
 			parsePbConstraint(wlc, maxV);
@@ -371,6 +375,19 @@ void DimacsReader::parsePbConstraint(WeightLitVec& constraint, int64_t maxV) {
 	}
 	parseConstraintRhs(constraint);
 }
+void DimacsReader::parseAtLeastK(WeightLitVec& scratch, int64_t maxV) {
+	scratch.clear();
+	int64 k;
+	require(stream()->match(k) && k >= 0 && k <= CLASP_WEIGHT_T_MAX, "invalid at-least-k constraint");
+	for (int64 lit;;) {
+		require(stream()->match(lit) && lit >= -maxV && lit <= maxV, "invalid variable in at-least-k constraint");
+		if (lit == 0) {
+			program_->addConstraint(scratch, static_cast<weight_t>(k));
+			return;
+		}
+		scratch.push_back(WeightLiteral(toLit(static_cast<int32>(lit)), 1));
+	}
+}
 /////////////////////////////////////////////////////////////////////////////////////////
 // OpbReader
 /////////////////////////////////////////////////////////////////////////////////////////

diff --git a/tests/parser_test.cpp b/tests/parser_test.cpp
@@ -826,6 +826,17 @@ TEST_CASE("Dimacs parser", "[parser][sat]") {
 		REQUIRE(ctx.numConstraints() == 2);
 	}
 
+	SECTION("testKnf") {
+		prg << "p knf 4 2\n"
+		       "1 2 0\n"
+		       "3 4 0\n"
+		       "k 2 1 2 3 4 0\n";
+		REQUIRE((parse(api, prg) && api.endProgram()));
+		REQUIRE(ctx.numVars() == 4);
+		REQUIRE(ctx.output.size() == 4);
+		REQUIRE(ctx.numConstraints() == 3);
+	}
+
 	SECTION("testDimacsExtSupportsGraph") {
 		prg
 			<< "p cnf 4 3\n"