satd.solvers.dpll source code

1 module satd.solvers.dpll;
2 
3 import satd.cnf, satd.assignment;
4 import std.variant : Algebraic;
5 import std.typecons : Tuple;
6 
7 alias Null = typeof(null);
8 alias SolverResult = Algebraic!(Assignment, Null);
9 
10 alias unitPropagateResult = Tuple!(CNF, "F", Assignment, "assignment");
11 
12 SolverResult solve(CNF F)
13 {
14     auto res = dpll(F, Assignment(F.variableNum));
15     if (res.peek!Assignment)
16     {
17         auto tmp = res.get!0;
18         tmp.fillUnassignedLiterals();
19         res = tmp;
20     }
21     return res;
22 }
23 
24 ulong k;
25 SolverResult dpll(CNF F, Assignment assignment)
26 {
27     k++;
28     auto uPRes = unitPropagate(F, assignment);
29     F = uPRes.F, assignment = uPRes.assignment;
30 
31     // if there exists an empty clause
32     if (F.emptyClauses.length > 0)
33         return SolverResult(null);
34     // if there's no clauses left
35     if (F.allClauses.length == 0)
36         return SolverResult(assignment);
37 
38     Literal l = assignment.getUnassignedLiteral();
39 
40     CNF F_l = CNF(F);
41     Assignment asgn1 = Assignment(assignment);
42     F_l.simplify(l);
43     asgn1.assign(l);
44 
45     auto res1 = dpll(F_l, asgn1);
46     if (res1.peek!Assignment)
47         return SolverResult(res1);
48 
49     CNF F_lnotl = CNF(F);
50     Assignment asgn2 = Assignment(assignment);
51     F_lnotl.simplify(-l);
52     asgn2.assign(-l);
53 
54     return dpll(F_lnotl, asgn2);
55 }
56 
57 unitPropagateResult unitPropagate(CNF F, Assignment assignment)
58 {
59     while (F.emptyClauses.length == 0 && F.unitClauses.length > 0)
60     {
61         auto k = F.unitClauses.keys[0], v = F.unitClauses[k];
62         Literal x = v.unitLiteral;
63 
64         F.simplify(x);
65         assignment.assign(x);
66     }
67     return unitPropagateResult(F, assignment);
68 }