1 module demo.demo; 2 3 import std.stdio; 4 import satd.dimacs; 5 import satd.cnf; 6 import satd.solvers.dpll; 7 import satd.assignment; 8 import std.algorithm : each; 9 import satd.solvers.cdcl; 10 import std.file : getcwd; 11 import std.string : chomp, join; 12 import std.getopt; 13 14 int main(string[] args) 15 { 16 // auto a = parseClauses(); 17 // auto cnf = CNF(a.clauses, a.preamble); 18 // auto res = solvers.dpll.solve(cnf); 19 // solverResultToString(res).writeln; 20 // return; 21 22 // write("testcase file: "); 23 // stdout.flush(); 24 bool renderGraph, renderAnotherGraph, isTseytin, benchmark, restart; 25 string filepath; 26 long restartThreshold = -1; 27 double restartMult = 1.5; 28 auto helpInfo = getopt(args, "graph|G", "output .dot files", &renderGraph, 29 "graph-another", "output .dot files", &renderAnotherGraph, 30 "benchmark|B", "run benchmark", &benchmark, 31 "file", &filepath, "tseytin|tseitin|T", 32 "enable tseytin transformation", &isTseytin, 33 "restart|R", "enable restart", &restart, "restart-threshold", 34 "Threshold for restart", 35 &restartThreshold, "restart-scale", "multiplication ratio for restart", &restartMult); 36 37 if (helpInfo.helpWanted) 38 { 39 defaultGetoptPrinter("sat-d is a small SAT solver implementation written in D.", 40 helpInfo.options); 41 return 0; 42 } 43 44 CDCLSolver solver = new CDCLSolver(); 45 CDCLSolverResult res; 46 if (restartThreshold > 0) 47 solver.restartThreshold = restartThreshold; 48 if (restartMult > 0) 49 solver.restartMult = restartMult; 50 51 solver.restart = restart; 52 53 if (isTseytin) 54 { 55 import satd.tseytin; 56 57 auto formula = args[$ - 1]; 58 auto tseytin = tseytinTransform(formula); 59 solver.initialize(tseytin.parseResult); 60 res = solver.solve(); 61 auto literals = res.peek!(Literal[]); 62 if (literals is null) 63 { 64 writeln("UNSAT"); 65 return 0; 66 } 67 else 68 { 69 bool[string] assignment = resultToOriginalVarsAssignment(tseytin, *literals); 70 assignment.writeln; 71 return 0; 72 } 73 } 74 auto cls = filepath ? parseClauses(File(filepath)) : parseClauses(); 75 solver.initialize(cls); 76 solver.generateGraph = renderGraph; 77 solver.generateAnotherGraph = renderAnotherGraph; 78 if (benchmark) 79 { 80 import std.datetime.stopwatch : StopWatch; 81 82 StopWatch watch; 83 watch.start; 84 res = solver.solve(); 85 watch.stop; 86 writefln("%s,%f", res.peek!(typeof(null)) ? "UNSAT" : "SAT", 87 watch.peek.total!"usecs" / 1e6); 88 return 0; 89 } 90 91 immutable auto result = solver.solve(); 92 if (result.peek!(typeof(null))) 93 writeln("s UNSATISFIABLE"); 94 else 95 { 96 auto assignment = result.peek!(Literal[]); 97 writefln("v %(%d %)", *assignment ~ 0); 98 writeln("s SATISFIABLE"); 99 } 100 return 0; 101 }