dkh.twosat source code

1 module dkh.twosat;
2 
3 import dkh.graph.scc;
4 import dkh.container.stackpayload;
5 
6 /// 2-SAT Solver
7 struct TwoSat {
8     bool[] vars; /// assigned variable
9 
10     static struct Edge {uint to;}
11     private StackPayload!Edge[] g;
12 
13     /// Clause $(D (vars[a] == expectedA) || (vars[b] == expectedB))
14     void addClause(size_t a, bool expectedA, size_t b, bool expectedB) {
15         import std.conv : to;
16         g[2*a+(expectedA?0:1)] ~= Edge((2*b+(expectedB?1:0)).to!uint);
17         g[2*b+(expectedB?0:1)] ~= Edge((2*a+(expectedA?1:0)).to!uint);
18     }
19 
20     /**
21     Solve 2-SAT
22 
23     Returns:
24         satisfiable or not
25      */
26     bool solve() {
27         import std.array : array;
28         import std.algorithm : map;
29         auto sccInfo = scc(g.map!(v => v.data).array);
30         foreach (i; 0..vars.length) {
31             if (sccInfo.id[2*i] == sccInfo.id[2*i+1]) return false;
32             vars[i] = sccInfo.id[2*i] < sccInfo.id[2*i+1];
33         }
34         return true;
35     }
36 
37     /**
38     Params:
39         n = # of variables
40      */
41     this(size_t n) {
42         vars = new bool[n];
43         g = new StackPayload!Edge[](2*n);
44     }
45 }
46 
47 ///
48 unittest {
49     // Solve (x0 v x1) ^ (~x0 v x2) ^ (~x1 v ~x2)
50     auto sat = TwoSat(3);
51     sat.addClause(0, true,  1, true);  // (vars[0] == true  || vars[1] == true)
52     sat.addClause(0, false, 2, true);  // (vars[0] == false || vars[2] == true)
53     sat.addClause(1, false, 2, false); // (vars[1] == false || vars[2] == false)
54     assert(sat.solve() == true);
55     auto vars = sat.vars;
56     assert(vars[0] == true  || vars[1] == true);
57     assert(vars[0] == false || vars[2] == true);
58     assert(vars[1] == false || vars[2] == false);
59 }
60 
61 unittest {
62     import std.algorithm, std.conv, std.stdio, std.range;
63     import std.random;
64     import std.typecons;
65 
66     struct E {int to;}
67 
68     void f() {
69         int n = uniform(1, 50);
70         int m = uniform(1, 100);
71         auto ans = new bool[n];
72         auto sat = TwoSat(n);
73         ans.each!((ref x) => x = uniform(0, 2) == 1);
74         struct N {int i; bool expect;}
75         N[2][] conds;
76         foreach (i; 0..m) {
77             int x = uniform(0, n);
78             int y = uniform(0, n);
79             while (true) {
80                 bool f = uniform(0, 2) == 1;
81                 bool g = uniform(0, 2) == 1;
82                 if (ans[x] != f && ans[y] != g) continue;
83                 sat.addClause(x, f, y, g);
84                 conds ~= [N(x, f), N(y, g)];
85                 break;
86             }
87         }
88         assert(sat.solve());
89         auto vars = sat.vars;
90         foreach (cond; conds) {
91             int x = cond[0].i;
92             bool f = cond[0].expect;
93             int y = cond[1].i;
94             bool g = cond[1].expect;
95             assert(vars[x] == f || vars[y] == g);
96         }
97     }
98 
99     import dkh.stopwatch;
100     auto ti = benchmark!(f)(1000);
101     writeln("TwoSat Random1000: ", ti[0].toMsecs);
102 }