-
Notifications
You must be signed in to change notification settings - Fork 0
/
minimal-sat.html
580 lines (448 loc) · 34.8 KB
/
minimal-sat.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
<!DOCTYPE html>
<html>
<head>
<title>minimal-sat.js</title>
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<meta name="viewport" content="width=device-width, target-densitydpi=160dpi, initial-scale=1.0; maximum-scale=1.0; user-scalable=0;">
<link rel="stylesheet" media="all" href="docco.css" />
</head>
<body>
<div id="container">
<div id="background"></div>
<ul class="sections">
<li id="title">
<div class="annotation">
<h1>minimal-sat.js</h1>
</div>
</li>
<li id="section-1">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-1">¶</a>
</div>
<p>In this blog post, we write a minimal <a href="https://en.wikipedia.org/wiki/Boolean_satisfiability_problem">SAT</a> solver.
A SAT solver determines whether a boolean formula can be “satisfied” (made true) by an appropriate assignment of <code>true</code> and <code>false</code> to the variables constituting that formula.</p>
<p>For example, the boolean formula</p>
<p>(x1 ⇒ x2) ∧ (x1 ∨ ∼x3)</p>
<p>corresponds with the equation</p>
<p>true ≡ (x1 ⇒ x2) ∧ (x1 ∨ ∼x3)</p>
<p>which could be satisfied with the assignments</p>
<p>(x1 ≡ false) ∧ (x2 ≡ true) ∧ (x3 ≡ false)</p>
<p>Note that while the SAT problem concerns itself only with the existence of such an assignment, when such an assignment does exist, our solver will emit it.
This provides a way to easily validate our code, as an assignment can be verified in polynomial time.</p>
</div>
<div class="content"><div class='highlight'><pre><span class="hljs-meta">
'use strict'</span>;
<span class="hljs-keyword">const</span> fs = <span class="hljs-built_in">require</span>(<span class="hljs-string">'fs'</span>);
<span class="hljs-keyword">const</span> tape = <span class="hljs-built_in">require</span>(<span class="hljs-string">'tape'</span>);
<span class="hljs-keyword">const</span> util = <span class="hljs-built_in">require</span>(<span class="hljs-string">'util'</span>);</pre></div></div>
</li>
<li id="section-2">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-2">¶</a>
</div>
<h2 id="examples">Examples</h2>
</div>
</li>
<li id="section-3">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-3">¶</a>
</div>
<p>Let’s start by writing a test to outline what “correct” looks like.
We introduce a function that lets us embed tests in this source file, choosing to run the tests by passing a <code>--self-test</code> command line argument.
For the underlying tests, we leverage the <a href="https://github.com/substack/tape">tape</a> library, which outputs test results in the <a href="https://en.wikipedia.org/wiki/Test_Anything_Protocol">Test Anything Protocol</a> (TAP) format.</p>
</div>
<div class="content"><div class='highlight'><pre>
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">testfn</span>(<span class="hljs-params">fn, testImpl</span>) </span>{
<span class="hljs-keyword">if</span> (process.argv.includes(<span class="hljs-string">'--self-test'</span>)) {
tape(fn.name, t => testImpl(t, fn));
}
}</pre></div></div>
</li>
<li id="section-4">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-4">¶</a>
</div>
<p>Every boolean formula can be expressed as a a conjunction of disjunctions (AKA <a href="https://en.wikipedia.org/wiki/Conjunctive_normal_form">conjunctive normal form</a>, or CNF) , and by constraining our solver to input in that form, we can avoid tokenizing, parsing (which includes handling operator precedence), and writing logic for redundant operators like logical implication.</p>
<p>For example, the initial example</p>
<p>(x1 ⇒ x2) ∧ (x1 ∨ ∼x3)</p>
<p>could be converted to CNF as</p>
<p>(∼ x1 ∨ x2) ∧ (x1 ∨ ∼x3)</p>
<p>which would be encoded as</p>
<pre><code>[{<span class="hljs-attr">x1</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">x2</span>: <span class="hljs-literal">true</span>}, <span class="hljs-comment">// clause 1</span>
{<span class="hljs-attr">x1</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">x3</span>: <span class="hljs-literal">false</span>}] <span class="hljs-comment">// clause 2</span>
</code></pre><p>So our SAT solver <code>solve</code> accepts an array of clauses, where every clause must be satisfied, and to satisfy a clause at least one of the literals must match the associated value. With this in mind, we can implement our primary test.</p>
</div>
<div class="content"><div class='highlight'><pre>
testfn(solve, (t, fn) => {
<span class="hljs-keyword">const</span> unsatisfiable = [
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>}],
];
<span class="hljs-keyword">for</span> (<span class="hljs-keyword">const</span> problem <span class="hljs-keyword">of</span> unsatisfiable) {
<span class="hljs-keyword">const</span> assignment = fn(problem);
t.deepEqual(assignment, <span class="hljs-literal">null</span>);
}
<span class="hljs-keyword">const</span> satisfiable = [
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">false</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">true</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">true</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">c</span>: <span class="hljs-literal">true</span>}],
[{<span class="hljs-attr">a</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-attr">b</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">c</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">b</span>: <span class="hljs-literal">true</span>}],
];
<span class="hljs-keyword">for</span> (<span class="hljs-keyword">const</span> problem <span class="hljs-keyword">of</span> satisfiable) {
<span class="hljs-keyword">const</span> assignment = fn(problem);
t.ok(!!assignment);
<span class="hljs-keyword">const</span> isValidAssignment = problem.every(<span class="hljs-function"><span class="hljs-params">clause</span> =></span> {
<span class="hljs-keyword">const</span> isSatisfied = <span class="hljs-built_in">Object</span>.keys(clause).some(<span class="hljs-function"><span class="hljs-params">atom</span> =></span> clause[atom] === assignment[atom]);
<span class="hljs-keyword">return</span> isSatisfied;
});
t.ok(isValidAssignment);
}
t.end();
});</pre></div></div>
</li>
<li id="section-5">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-5">¶</a>
</div>
<h2 id="solver-implementation">Solver Implementation</h2>
</div>
</li>
<li id="section-6">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-6">¶</a>
</div>
<p>Many SAT algorithms exist, and one of the most fundamental is <a href="https://en.wikipedia.org/wiki/DPLL_algorithm">DPLL</a>.
We collect assignments as follows:</p>
<ol>
<li>Choose an unassigned variable, stopping if none are available.</li>
<li>For each possible truth value assignment of that variable, verify that the assignment does not contradict any clauses, backtracking if both assignments contradict.</li>
<li>Assuming an assignment does not yet contradict, recurse with a simplified problem in which the variable no longer exists, cleaning up clauses as necessary. If our recursive call succeeds, we’re done. If it fails for both <code>true</code> and <code>false</code>, we backtrack (as a different assignment of previously assigned variables might be successful).</li>
</ol>
</div>
<div class="content"><div class='highlight'><pre>
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">solve</span>(<span class="hljs-params">clauses, assignment = {}</span>) </span>{
<span class="hljs-keyword">return</span> trace(solve, <span class="hljs-built_in">arguments</span>, () => { <span class="hljs-comment">// we wrap in a helper for debugging</span>
<span class="hljs-keyword">const</span> v = nextVar(clauses);
<span class="hljs-keyword">if</span> (!v) { <span class="hljs-keyword">return</span> assignment; }
<span class="hljs-keyword">for</span> (<span class="hljs-keyword">const</span> value <span class="hljs-keyword">of</span> [<span class="hljs-literal">true</span>, <span class="hljs-literal">false</span>]) {
<span class="hljs-keyword">if</span> (canAssign(value, v, clauses)) {
<span class="hljs-keyword">const</span> result = solve(removeVar(value, v, clauses), newAssignment(assignment, v, value));
<span class="hljs-keyword">if</span> (result) { <span class="hljs-keyword">return</span> result; }
}
}
<span class="hljs-keyword">return</span> <span class="hljs-literal">null</span>;
});
}</pre></div></div>
</li>
<li id="section-7">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-7">¶</a>
</div>
<p>The above implementation relies on the following four helpers:</p>
<ol>
<li><code>nextVar</code>: choose a variable favoring “unit” clauses with only one possible assignment;</li>
<li><code>canAssign</code>: infer when an assignment of that variable violates any clause;</li>
<li><code>removeVar</code>: “clean up” satisfied clauses; and</li>
<li><code>newAssignment</code>: add a variable-to-truth-value assignment to a collection of assignments.</li>
</ol>
</div>
<div class="content"><div class='highlight'><pre>
testfn(nextVar, (t, fn) => {
t.deepEqual(fn([]), <span class="hljs-literal">null</span>);
t.deepEqual(fn([{}]), <span class="hljs-literal">null</span>);
t.deepEqual(fn([{<span class="hljs-attr">x</span>: <span class="hljs-number">0</span>}]), <span class="hljs-string">'x'</span>);
t.deepEqual(fn([{<span class="hljs-attr">x</span>: <span class="hljs-number">0</span>, <span class="hljs-attr">y</span>: <span class="hljs-number">0</span>}]), <span class="hljs-string">'x'</span>);
t.end();
});
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">nextVar</span>(<span class="hljs-params">clauses</span>) </span>{
<span class="hljs-keyword">const</span> clauseKeys = clauses.map(<span class="hljs-function"><span class="hljs-params">c</span> =></span> <span class="hljs-built_in">Object</span>.keys(c));
<span class="hljs-keyword">if</span> (clauseKeys.some(<span class="hljs-function"><span class="hljs-params">c</span> =></span> c.length == <span class="hljs-number">0</span>)) {
<span class="hljs-keyword">return</span> <span class="hljs-literal">null</span>;
}
<span class="hljs-keyword">const</span> unit = clauseKeys.find(<span class="hljs-function"><span class="hljs-params">c</span> =></span> c.length == <span class="hljs-number">1</span>);
<span class="hljs-keyword">if</span> (unit) {
<span class="hljs-keyword">return</span> unit[<span class="hljs-number">0</span>];
}
<span class="hljs-keyword">return</span> clauseKeys.reduce(<span class="hljs-function">(<span class="hljs-params">l, r</span>) =></span> l.concat(r), []).find(<span class="hljs-function"><span class="hljs-params">x</span> =></span> x) || <span class="hljs-literal">null</span>;
}
testfn(canAssign, (t, fn) => {
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, []), <span class="hljs-literal">true</span>);
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, [{}]), <span class="hljs-literal">true</span>); <span class="hljs-comment">// <span class="hljs-doctag">NOTE:</span> clause is unsat, but assignment is valid</span>
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, [{<span class="hljs-attr">y</span>: <span class="hljs-literal">true</span>}]), <span class="hljs-literal">true</span>);
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, [{<span class="hljs-attr">y</span>: <span class="hljs-literal">false</span>}]), <span class="hljs-literal">true</span>);
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, [{<span class="hljs-attr">x</span>: <span class="hljs-literal">true</span>}]), <span class="hljs-literal">true</span>);
t.deepEqual(fn(<span class="hljs-literal">true</span>, <span class="hljs-string">'x'</span>, [{<span class="hljs-attr">x</span>: <span class="hljs-literal">false</span>}]), <span class="hljs-literal">false</span>);
t.end();
});
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">canAssign</span>(<span class="hljs-params">value, variable, clauses</span>) </span>{
<span class="hljs-keyword">return</span> clauses.every(<span class="hljs-function"><span class="hljs-params">c</span> =></span> <span class="hljs-built_in">Object</span>.keys(c).length > <span class="hljs-number">1</span> || !c.hasOwnProperty(variable) || c[variable] == value);
}
testfn(removeVar, (t, fn) => {
t.deepEqual(
fn(<span class="hljs-literal">true</span>, <span class="hljs-number">1</span>, [{<span class="hljs-number">1</span>: <span class="hljs-literal">false</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">true</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">false</span>}]),
[{<span class="hljs-number">3</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">true</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">false</span>}]);
t.deepEqual(
fn(<span class="hljs-literal">false</span>, <span class="hljs-number">1</span>, [{<span class="hljs-number">1</span>: <span class="hljs-literal">false</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">true</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">true</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">false</span>}]),
[{<span class="hljs-number">2</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-number">2</span>: <span class="hljs-literal">true</span>, <span class="hljs-number">3</span>: <span class="hljs-literal">false</span>}]);
t.end();
});
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">removeVar</span>(<span class="hljs-params">value, variable, clauses</span>) </span>{
<span class="hljs-keyword">return</span> clauses.filter(<span class="hljs-function"><span class="hljs-params">c</span> =></span> c[variable] !== value).map(<span class="hljs-function"><span class="hljs-params">c</span> =></span> {
<span class="hljs-keyword">const</span> result = <span class="hljs-built_in">Object</span>.assign({}, c);
<span class="hljs-keyword">delete</span> result[variable];
<span class="hljs-keyword">return</span> result;
});
}
testfn(newAssignment, (t, fn) => {
t.deepEqual(
newAssignment({}, <span class="hljs-string">'x'</span>, <span class="hljs-literal">true</span>),
{<span class="hljs-attr">x</span>: <span class="hljs-literal">true</span>});
t.deepEqual(
newAssignment({}, <span class="hljs-string">'y'</span>, <span class="hljs-literal">false</span>),
{<span class="hljs-attr">y</span>: <span class="hljs-literal">false</span>});
t.deepEqual(
newAssignment({<span class="hljs-attr">x</span>: <span class="hljs-literal">false</span>}, <span class="hljs-string">'y'</span>, <span class="hljs-literal">true</span>),
{<span class="hljs-attr">x</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">y</span>: <span class="hljs-literal">true</span>});
t.end();
});
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">newAssignment</span>(<span class="hljs-params">original, variable, value</span>) </span>{
<span class="hljs-keyword">const</span> result = <span class="hljs-built_in">Object</span>.assign({}, original);
result[variable] = value;
<span class="hljs-keyword">return</span> result;
}</pre></div></div>
</li>
<li id="section-8">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-8">¶</a>
</div>
<h2 id="parsing">Parsing</h2>
</div>
</li>
<li id="section-9">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-9">¶</a>
</div>
<p>The <a href="http://people.sc.fsu.edu/~jburkardt%20/data/cnf/cnf.html">DIMACS CNF format</a> specifies a common encoding for CNF expressions.
By parsing this format, we can validate our implemenation against more test data and also easily compare our SAT performance with other implementations.</p>
</div>
<div class="content"><div class='highlight'><pre>
testfn(parseDimacs, (t, fn) => {
<span class="hljs-keyword">const</span> example = <span class="hljs-string">`
c simple_v3_c2.cnf
c
p cnf 3 2
1 -3 0
2 3 -1 0
`</span>;
t.deepEqual(
parseDimacs(example),
[{<span class="hljs-attr">x1</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">x3</span>: <span class="hljs-literal">false</span>}, {<span class="hljs-attr">x1</span>: <span class="hljs-literal">false</span>, <span class="hljs-attr">x2</span>: <span class="hljs-literal">true</span>, <span class="hljs-attr">x3</span>: <span class="hljs-literal">true</span>}]);
t.end();
});
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">parseDimacs</span>(<span class="hljs-params">data</span>) </span>{</pre></div></div>
</li>
<li id="section-10">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-10">¶</a>
</div>
<p>First we remove comments, which are lines starting with a “c” character.</p>
</div>
<div class="content"><div class='highlight'><pre> data = data.replace(<span class="hljs-regexp">/(^|\n)c.*/g</span>, <span class="hljs-string">''</span>);</pre></div></div>
</li>
<li id="section-11">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-11">¶</a>
</div>
<p>Next we extract the problem description, which indicates the number of symbols and clauses.
For simplicity, we just throw this away as we can infer it from the rest of the file.</p>
</div>
<div class="content"><div class='highlight'><pre> <span class="hljs-keyword">const</span> lines = data.replace(<span class="hljs-regexp">/(^|\n)c.*/g</span>, <span class="hljs-string">''</span>).split(<span class="hljs-string">'\n'</span>);
<span class="hljs-keyword">let</span> i = <span class="hljs-number">0</span>;
<span class="hljs-keyword">while</span> (lines[i].length == <span class="hljs-number">0</span> || lines[i][<span class="hljs-number">0</span>] != <span class="hljs-string">'p'</span>) { ++i; }
<span class="hljs-keyword">const</span> problem = lines[i].match(<span class="hljs-regexp">/\S+/g</span>);
debug({problem});</pre></div></div>
</li>
<li id="section-12">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-12">¶</a>
</div>
<p>Now we are ready to extract the clauses. Note that clauses are “0” delimited, not newline delimited.</p>
</div>
<div class="content"><div class='highlight'><pre> <span class="hljs-keyword">const</span> clauses = lines.splice(i+<span class="hljs-number">1</span>) <span class="hljs-comment">// start w/ lines after the problem</span>
.join(<span class="hljs-string">'\n'</span>).split(<span class="hljs-regexp">/\s+0/</span>) <span class="hljs-comment">// split on '0' character delimiter instead of newline</span>
.map(<span class="hljs-function"><span class="hljs-params">l</span> =></span> l.match(<span class="hljs-regexp">/\S+/g</span>)) <span class="hljs-comment">// extract tokens</span>
.filter(<span class="hljs-function"><span class="hljs-params">l</span> =></span> l); <span class="hljs-comment">// and filter out noise</span>
debug({clauses});</pre></div></div>
</li>
<li id="section-13">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-13">¶</a>
</div>
<p>The clauses are encoded such that <code>-num</code> indicates that x<sub>num</sub> is false while <code>num</code> indicates x<sub>num</sub> is true.</p>
</div>
<div class="content"><div class='highlight'><pre> <span class="hljs-keyword">return</span> clauses.map(<span class="hljs-function"><span class="hljs-params">encoded</span> =></span> {
<span class="hljs-keyword">const</span> decoded = {};
<span class="hljs-keyword">for</span> (<span class="hljs-keyword">const</span> sym <span class="hljs-keyword">of</span> encoded) {
<span class="hljs-keyword">if</span> (sym < <span class="hljs-number">0</span>) {
decoded[<span class="hljs-string">'x'</span> + -sym] = <span class="hljs-literal">false</span>;
} <span class="hljs-keyword">else</span> {
decoded[<span class="hljs-string">'x'</span> + sym] = <span class="hljs-literal">true</span>;
}
}
<span class="hljs-keyword">return</span> decoded;
});
}</pre></div></div>
</li>
<li id="section-14">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-14">¶</a>
</div>
<h1 id="performance">Performance</h1>
</div>
</li>
<li id="section-15">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-15">¶</a>
</div>
<p>Similar to our <code>testfn</code> helper, we introduce a <code>timefn</code> helper that only runs performance tests if the program is started with a <code>--perf</code> argument.</p>
</div>
<div class="content"><div class='highlight'><pre>
function timefn(fn, impl) {
const count = 1;
if (!process.argv.includes('--perf')) { return; }
console.log(`# ${fn.name}`);
impl(fn, (description, computation) => {
const start = new Date();
for (let i = 0; i < count; ++i) {
computation();
}
const end = new Date();
console.log(`## ${description}: ${(end - start)/count} ms`);
});
}</pre></div></div>
</li>
<li id="section-16">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-16">¶</a>
</div>
<p>To stress our solver a bit, we have three example DIMACS CNF files:</p>
<ol>
<li><a href="http://people.sc.fsu.edu/~jburkardt/data/cnf/aim-50-1_6-yes1-4.cnf">aim-50-1_6-yes1-4.cnf</a></li>
<li><a href="http://people.sc.fsu.edu/~jburkardt/data/cnf/aim-100-1_6-no-1.cnf">aim-100-1_6-no-1.cnf</a></li>
<li><a href="http://people.sc.fsu.edu/~jburkardt%20/data/cnf/zebra_v155_c1135.cnf">zebra_v155_c1135.cnf</a></li>
</ol>
</div>
<div class="content"><div class='highlight'><pre>
timefn(solve, (fn, time) => {
fs.readFile(<span class="hljs-string">'aim-50-1_6-yes1-4.cnf'</span>, <span class="hljs-string">'utf-8'</span>, (err, data) => {
<span class="hljs-keyword">const</span> constraints = parseDimacs(data);
time(<span class="hljs-string">'aim-50-1_6-yes1-4.cnf: satisfiable'</span>, () => solve(constraints));
});
fs.readFile(<span class="hljs-string">'aim-100-1_6-no-1.cnf'</span>, <span class="hljs-string">'utf-8'</span>, (err, data) => {
<span class="hljs-keyword">const</span> constraints = parseDimacs(data);
time(<span class="hljs-string">'aim-100-1_6-no-1.cnf: unsatisfiable'</span>, () => solve(constraints));
});
fs.readFile(<span class="hljs-string">'zebra_v155_c1135.cnf'</span>, <span class="hljs-string">'utf-8'</span>, (err, data) => {
<span class="hljs-keyword">const</span> constraints = parseDimacs(data);
time(<span class="hljs-string">'zebra_v155_c1135.cnf: satisfiable'</span>, () => solve(constraints));
});
});</pre></div></div>
</li>
<li id="section-17">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-17">¶</a>
</div>
<p>Two of the problems are satisfiable and take just under a second on my laptop, while one is unsatisfiable and takes just over a minute on the same hardware.
For comparison, the industrial strength <a href="https://github.com/Z3Prover/z3">Z3</a> theorem prover can solve all three in milliseconds.
It’s clear that this minimal example has lots of room for performance improvements!</p>
</div>
</li>
<li id="section-18">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-18">¶</a>
</div>
<h2 id="appendix-development-helpers">Appendix: Development Helpers</h2>
</div>
</li>
<li id="section-19">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-19">¶</a>
</div>
<p>TAP parsers expect a leading <code>#</code> for comments, and outputing debug information to the console without that leading <code>#</code> breaks parsing.
To make our debug logging slightly less verbose, we introduce another small helper, <code>debug</code>.</p>
<p>Note that while <code>#</code> indicates a comment, nodejs TAP reporters (such as <a href="https://github.com/scottcorgan/tap-spec">tap-spec</a>) typically interpret <code>#</code> as a test name, so this helper emits a <code>##</code>, which most parsers interpret as a non-test-comment.</p>
</div>
<div class="content"><div class='highlight'><pre>
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">debug</span>(<span class="hljs-params">format, ... other</span>) </span>{
<span class="hljs-keyword">if</span> (process.argv.includes(<span class="hljs-string">'--debug'</span>)) {
<span class="hljs-keyword">if</span> (<span class="hljs-keyword">typeof</span> format != <span class="hljs-string">'string'</span>) {
format = util.inspect(format);
}
<span class="hljs-built_in">console</span>.log(<span class="hljs-string">'## '</span> + format, ...other);
}
}</pre></div></div>
</li>
<li id="section-20">
<div class="annotation">
<div class="pilwrap ">
<a class="pilcrow" href="#section-20">¶</a>
</div>
<p>It’s also useful to be able to trace function calls, so we introduce a helper for that as well.
Example output:</p>
<pre><code>## solve <-- [ { a: true, b: true }, { b: true } ]
## solve <-- [ { b: true } ], { a: true }
## solve <-- [], { a: true, b: true }
## solve --> { a: true, b: true }
## solve --> { a: true, b: true }
## solve --> { a: true, b: true }
</code></pre>
</div>
<div class="content"><div class='highlight'><pre>
<span class="hljs-function"><span class="hljs-keyword">function</span> <span class="hljs-title">trace</span>(<span class="hljs-params">fn, args, impl</span>) </span>{
<span class="hljs-keyword">if</span> (!process.argv.includes(<span class="hljs-string">'--debug'</span>)) { <span class="hljs-keyword">return</span> impl.apply(<span class="hljs-keyword">this</span>, args); }
trace.depth = trace.depth || <span class="hljs-number">0</span>;
<span class="hljs-keyword">const</span> pad = <span class="hljs-string">' '</span>.repeat(trace.depth);
<span class="hljs-keyword">const</span> name = fn.name || <span class="hljs-keyword">new</span> <span class="hljs-built_in">Error</span>().stack.match(<span class="hljs-regexp">/ at ([^ ]+)/g</span>)[<span class="hljs-number">1</span>].split(<span class="hljs-string">' '</span>)[<span class="hljs-number">2</span>];
<span class="hljs-keyword">try</span> {
++trace.depth;
debug(<span class="hljs-string">`<span class="hljs-subst">${pad}</span><span class="hljs-subst">${name}</span> <--`</span>, <span class="hljs-built_in">Array</span>.from(args).map(util.inspect).join(<span class="hljs-string">', '</span>));
<span class="hljs-keyword">const</span> result = impl.apply(<span class="hljs-keyword">this</span>, args);
debug(<span class="hljs-string">`<span class="hljs-subst">${pad}</span><span class="hljs-subst">${name}</span> -->`</span>, result);
<span class="hljs-keyword">return</span> result;
} <span class="hljs-keyword">catch</span>(err) {
debug(<span class="hljs-string">`<span class="hljs-subst">${pad}</span><span class="hljs-subst">${name}</span> !!!`</span>, err);
<span class="hljs-keyword">throw</span> err;
} <span class="hljs-keyword">finally</span> {
--trace.depth;
}
}</pre></div></div>
</li>
</ul>
</div>
</body>
</html>