Implement Tseytin transformation

.github/workflows/main.yml

@@ -26,3 +26,6 @@ jobs:
 
       - name: Run tests
         run: make test
+
+      - name: Run `dub test`
+        run: dub test

dub.json

@@ -3,6 +3,9 @@
 		"public_yusuke"
 	],
 	"copyright": "Copyright © 2020, public_yusuke",
+	"dependencies": {
+		"pegged": "~>0.4.4"
+	},
 	"description": "A small SAT solver implementation",
 	"license": "MIT",
 	"name": "sat-d"

dub.selections.json

@@ -1,4 +1,6 @@
 {
 	"fileVersion": 1,
-	"versions": {}
-}
+	"versions": {
+		"pegged": "0.4.4"
+	}
+}

source/app.d

@@ -6,9 +6,11 @@ import assignment;
 import std.algorithm : each;
 import solvers.cdcl;
 import std.file : getcwd;
-import std.string : chomp;
+import std.string : chomp, join;
+import tseytin;
+import std.math : abs;
 
-void main(string[] args)
+int main(string[] args)
 {
 	// auto a = parseClauses();
 	// auto cnf = CNF(a.clauses, a.preamble);
@@ -20,9 +22,42 @@ void main(string[] args)
 	// stdout.flush();
 
 	CDCLSolver solver = new CDCLSolver();
+	CDCLSolverResult res;
 	// solver.initialize(solver.parseClauses(File("testcase/graph-ordering-5.cnf")));
-	solver.initialize(parseClauses());
 
+	if (args.length >= 2 && args[1] == "tseytin")
+	{
+		if (args.length == 2)
+		{
+			stderr.writeln("Usage: sat-d tseytin <formula>");
+			return 1;
+		}
+		auto formula = args[2 .. $].join(' ');
+		auto tseytin = tseytinTransform(formula);
+		solver.initialize(tseytin.parseResult);
+		res = solver.solve();
+		auto literals = res.peek!(Literal[]);
+		if (literals is null)
+		{
+			writeln("UNSAT");
+			return 0;
+		}
+		else
+		{
+			bool[string] assignment;
+			bool[Literal] litToTruth;
+			foreach (lit; *literals)
+			{
+				litToTruth[abs(lit)] = lit > 0;
+			}
+			foreach (var, lit; tseytin.varToLiteral)
+			{
+				assignment[var] = litToTruth[lit];
+			}
+			assignment.writeln;
+			return 0;
+		}
+	}
 	if (args.length >= 2 && args[1] == "true")
 		solver.generateGraph = true;
 	if (args.length >= 2 && args[1] == "benchmark")
@@ -31,12 +66,13 @@ void main(string[] args)
 
 		StopWatch watch;
 		watch.start;
-		auto res = solver.solve();
+		res = solver.solve();
 		watch.stop;
 		writefln("%s,%f", res.peek!(typeof(null)) ? "UNSAT" : "SAT",
 				watch.peek.total!"usecs" / 1e6);
-		return;
+		return 0;
 	}
+	solver.initialize(parseClauses());
 	// CDCLSolver solver = new CDCLSolver(parseInput());
 
 	auto result = solver.solve();
@@ -47,5 +83,5 @@ void main(string[] args)
 		writeln("s SATISFIABLE");
 		result.writeln;
 	}
-
+	return 0;
 }

source/solvers/cdcl.d

@@ -1,5 +1,5 @@
 module solvers.cdcl;
-import cnf : CNF, Clause, Literal;
+import cnf : CNF, Clause, Literal, Set;
 import dimacs : Preamble, parseResult;
 import std.container : RedBlackTree, redBlackTree;
 import std.typecons : Tuple;
@@ -14,8 +14,6 @@ import std.variant : Algebraic;
 
 import std.stdio;
 
-alias Set(T) = RedBlackTree!T;
-
 /// LAMBDA は conflict node の意。
 const Literal LAMBDA = 0;
 
@@ -30,13 +28,18 @@ struct ImplicationGraph
     /// dlevel とは、decision level のことをさす。
     alias Node = Tuple!(Literal, "literal", size_t, "dlevel");
 
-    Set!Node nodes = redBlackTree!Node;
+    Set!Node nodes;
     Set!Node[Node] successors;
     Set!Node[Node] predecessors;
     Clause.ID[Node][Node] edges;
 
     Literal[] decisionLiterals;
 
+    void initalize()
+    {
+        nodes = redBlackTree!Node;
+    }
+
     this(ImplicationGraph graph)
     {
         this.nodes = graph.nodes.dup;
@@ -281,6 +284,8 @@ struct ImplicationGraph
     }
 }
 
+alias CDCLSolverResult = Algebraic!(Literal[], typeof(null));
+
 /// CDCL を実装した Solver
 class CDCLSolver
 {
@@ -300,6 +305,7 @@ class CDCLSolver
 
     this()
     {
+        implicationGraph.initalize();
     }
 
     void initialize(parseResult res)
@@ -342,14 +348,14 @@ class CDCLSolver
         OK
     }
 
-    alias CDCLSolverResult = Algebraic!(Literal[], typeof(null));
-
     CDCLSolverResult solve()
     {
         debug stderr.writefln("given clauses: %s", this.clauses.values);
 
         if (this.clauses.values.any!(c => c.literals.length == 0))
             return CDCLSolverResult(null);
+        if (this.preamble.variables == 0 && this.preamble.clauses == 0)
+            return CDCLSolverResult(cast(Literal[])[]);
         while (true)
         {
             while (true)