From 5dc254203546e75891f217db0c073d8a7aafb21e Mon Sep 17 00:00:00 2001 From: public_yusuke <30387586+private-yusuke@users.noreply.github.com> Date: Mon, 14 Sep 2020 02:24:20 +0900 Subject: [PATCH] Implement Tseytin transformation --- .github/workflows/main.yml | 3 + dub.json | 3 + dub.selections.json | 6 +- source/app.d | 48 ++++++- source/solvers/cdcl.d | 18 ++- source/tseytin.d | 270 +++++++++++++++++++++++++++++++++++++ 6 files changed, 334 insertions(+), 14 deletions(-) create mode 100644 source/tseytin.d diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index dc228a3..521a730 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -26,3 +26,6 @@ jobs: - name: Run tests run: make test + + - name: Run `dub test` + run: dub test diff --git a/dub.json b/dub.json index 2fe0496..cf844ca 100644 --- a/dub.json +++ b/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" diff --git a/dub.selections.json b/dub.selections.json index 22b6c56..455d9a1 100644 --- a/dub.selections.json +++ b/dub.selections.json @@ -1,4 +1,6 @@ { "fileVersion": 1, - "versions": {} -} \ No newline at end of file + "versions": { + "pegged": "0.4.4" + } +} diff --git a/source/app.d b/source/app.d index 648da03..65be82a 100644 --- a/source/app.d +++ b/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 "); + 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; } diff --git a/source/solvers/cdcl.d b/source/solvers/cdcl.d index 1c9abc5..f2cd44b 100644 --- a/source/solvers/cdcl.d +++ b/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) diff --git a/source/tseytin.d b/source/tseytin.d new file mode 100644 index 0000000..4f34447 --- /dev/null +++ b/source/tseytin.d @@ -0,0 +1,270 @@ +module tseytin; +import pegged.grammar; +import pegged.tohtml; +import dimacs; +import cnf; +import std.stdio; +import std.string : strip; +import std.container : redBlackTree; +import std.array : array; +import std.range : enumerate; +import std.typecons : Tuple; + +mixin(grammar(` +Expression: + Expr < Imp (OrOperator Imp)* + Imp < Conj (ImpOperator Conj / EquivOperator Conj)* + Conj < Unary (ConjOperator Unary)* + Unary < (UnaryOperator)? Primary + Primary < "(" Expr ")" / Ident + + OrOperator < "or" / "∨" / "v" / "\\/" + ImpOperator < "implies" / "then" / "→" / "⇒" / "->" / "=>" + EquivOperator < "equiv" / "⇔" / "↔" / "<=>" + + ConjOperator < "and" / "∧" / "^" / "/\\" + UnaryOperator < "not" / "-" / "￢" / "!" + Keyword < OrOperator / ImpOperator / EquivOperator / ConjOperator / UnaryOperator / "__VAR" ~[0-9]+ + Ident <- !Keyword ~[0-9A-Za-z_]+ +`)); + +debug +{ + import solvers.cdcl; + + enum bool[string] answers = [ + "not (a or not (b and c))" : true, + "not (a -> (b and c)) -> (b or not d equiv a)" : true, + "a and not a" : false, "not (a and not a)" : true + ]; + bool isSAT(string formula) + { + CDCLSolver solver = new CDCLSolver(); + solver.initialize(tseytinTransform(formula).parseResult); + return solver.solve().peek!(Literal[]) !is null; + } + + unittest + { + assert(isSAT("")); + assert(isSAT(" ")); + assert(isSAT("a")); + assert(isSAT("A or B and A or not B or not A or not B")); + assert(isSAT("A or B and not A or B and A or not B and not A or not B")); + assert(isSAT("a or not a")); + assert(!isSAT("a and not a")); + assert(!isSAT("A /\\ !A")); + + // check whether all the symbols can be interpreted correctly... + assert(isSAT("A or A ∨ A v A \\/ A implies B then B → B ⇒ B -> B equiv C ⇔ C ↔ C <=> D and D ∧ D ^ D /\\ D or not E or -D or ￢ D or ! D")); + import std.exception : collectException; + + // check that exceptions should be thrown if the input is invalid + assert(collectException(isSAT("a or v"))); + assert(collectException(isSAT("not"))); + assert(isSAT("A -> A")); + assert(isSAT("A implies A")); + assert(isSAT("not (a or not (b and c))")); + assert(isSAT("not (a -> (b and c)) -> (b or not d equiv a)")); + } +} + +enum ExprType +{ + NOT, + OR, + AND, + IMP, + EQUIV, +} + +struct Expr +{ + string left; + ExprType type; + string right; +} + +ExprType toExprType(string name) +{ + with (ExprType) + { + enum ExprType[string] exprMap = [ + "Expression.OrOperator" : OR, "Expression.ImpOperator" : IMP, + "Expression.EquivOperator" : EQUIV, + "Expression.ConjOperator" : AND, "Expression.UnaryOperator" : NOT + ]; + return exprMap[name]; + } +} + +alias tseytinTransformResult = Tuple!(parseResult, "parseResult", Literal[string], "varToLiteral"); + +tseytinTransformResult tseytinTransform(string input) +{ + input = input.strip; + // if the input is just blanks + if (input == "") + return tseytinTransformResult(parseResult([], Preamble(0, 0)), null); + + auto inputExpr = Expression(input); + // if (inputExpr.end != input.length) + // error("invalid input"); + + Expr[] expressions; + Set!string originalVars = redBlackTree!string; + string getPreviousVariable() + { + assert(expressions.length != 0); + return format("__VAR%d", expressions.length - 1); + } + + PT visit(PT)(PT p) + { + switch (p.name) + { + case "Expression": + return visit(p.children[0]); + case "Expression.Expr", "Expression.Imp", + "Expression.Conj": + if (p.children.length == 1) return visit(p.children[0]); + Expr lastExpr = Expr(visit(p.children[0]).input, + p.children[1].name.toExprType, visit(p.children[2]).input); + expressions ~= lastExpr; + + ulong k = 3; + while (k < p.children.length) + { + ExprType type = p.children[k].name.toExprType; + lastExpr = Expr(getPreviousVariable(), type, visit(p.children[k + 1]).input); + expressions ~= lastExpr; + k += 2; + } + p.input = getPreviousVariable(); + return p; + + case "Expression.Unary": + if (p.children.length == 1) + return visit(p.children[0]); + + auto res = visit(p.children[1]); + expressions ~= Expr(res.input, ExprType.NOT); + res.input = getPreviousVariable(); + return res; + + case "Expression.Primary": + if (p.children.length == 1) + return visit(p.children[0]); + else + return visit(p.children[1]); + + case "Expression.Ident": + p.input = p.input[p.begin .. p.end].strip; + originalVars.insert(p.input); + return p; + + default: + error("invalid formula"); + assert(0); + } + + } + + visit(inputExpr); + import std.algorithm; + + // if the input is like "a", meaning that there's only one variable left there and no operations found + if (expressions.length == 0) + return tseytinTransformResult(parseResult([Clause(1, [1])], Preamble(1, 1)), [ +input: 1 + ]); + + auto vars = redBlackTree!string; + foreach (ind, expr; expressions) + { + vars.insert(expr.left); + vars.insert(expr.right); + vars.insert(format("__VAR%d", ind)); + } + vars.removeKey(""); + long[string] m; + foreach (i, v; vars.array.enumerate) + m[v] = i + 1; + m[""] = 0; + + size_t clauseVarNum = 1; + Clause newClause(T...)(T literals) + { + return Clause(clauseVarNum++, [literals]); + } + + Clause[] clauses; + + Clause[] exprToClauses(size_t ind, Expr expr) + { + auto tseytinLit = m[format("__VAR%d", ind)]; + auto left = m[expr.left], right = m[expr.right]; + with (ExprType) switch (expr.type) + { + case NOT: + return [ + newClause(tseytinLit, left), newClause(-tseytinLit, -left) + ]; + case OR: + return [ + newClause(tseytinLit, -left), newClause(tseytinLit, -right), + newClause(-tseytinLit, left, right) + ]; + case AND: + return [ + newClause(-tseytinLit, left), newClause(-tseytinLit, right), + newClause(tseytinLit, -left, -right) + ]; + case IMP: + return [ + newClause(tseytinLit, left), newClause(tseytinLit, -right), + newClause(-tseytinLit, -left, right) + ]; + case EQUIV: + return [ + newClause(tseytinLit, left), newClause(tseytinLit, -right), + newClause(-tseytinLit, -left, right), newClause(tseytinLit, + right), newClause(tseytinLit, -left), + newClause(-tseytinLit, -right, left) + ]; + default: + assert(0); + } + } + + foreach (ind, expr; expressions) + { + clauses ~= exprToClauses(ind, expr); + } + clauses ~= newClause(m[format("__VAR%d", expressions.length - 1)]); + + Literal[string] varToLiteral; + foreach (var; originalVars) + { + varToLiteral[var] = m[var]; + } + + return tseytinTransformResult(parseResult(clauses, Preamble(vars.length, + clauseVarNum - 1)), varToLiteral); +} + +private: +import std.string : format; + +void error(A...)(string msg, A args) +{ + class ExpressionReadException : Exception + { + this(string msg) + { + super(msg); + } + } + + throw new ExpressionReadException(format(msg, args)); +}