forked from tammet/logictools
-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathpropositional.html
More file actions
436 lines (386 loc) · 17.9 KB
/
propositional.html
File metadata and controls
436 lines (386 loc) · 17.9 KB
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
<!DOCTYPE html>
<html lang="en">
<head itemscope>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta name="description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta name="author" content="Tanel Tammet">
<meta name="keywords" content="logic, solvers, propositions, dpll, resolution, truth table">
<meta itemprop="itemtype" content="http://schema.org/SoftwareApplication">
<meta itemprop="name" content="Logictools">
<meta itemprop="description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta itemprop="url" content="http://logictools.org">
<meta itemprop="operatingSystems" content="Linux, Windows">
<meta itemprop="softwareApplicationCategory" content="WebApplication">
<meta property="og:title" content="Logictools">
<meta property="og:url" content="http://logictools.org">
<meta property="og:site_name" content="Logictools">
<meta property="og:type" content="website">
<meta property="og:description" content="Simple propositional logic solvers: easy to hack and experiment with.">
<meta property="fb:admins" content="tanel.tammet">
<link rel="shortcut icon" href="logo.png">
<title>Logictools</title>
<!-- Bootstrap core CSS -->
<link rel="stylesheet" href="https://maxcdn.bootstrapcdn.com/bootstrap/3.3.4/css/bootstrap.min.css">
<!-- Custom styles for this template -->
<link href="wdb.css" rel="stylesheet">
<script>
// google analytics
(function(i,s,o,g,r,a,m){i['GoogleAnalyticsObject']=r;i[r]=i[r]||function(){
(i[r].q=i[r].q||[]).push(arguments)},i[r].l=1*new Date();a=s.createElement(o),
m=s.getElementsByTagName(o)[0];a.async=1;a.src=g;m.parentNode.insertBefore(a,m)
})(window,document,'script','//www.google-analytics.com/analytics.js','ga');
ga('create', 'UA-61132529-1', 'auto');
ga('send', 'pageview');
</script>
</head>
<body>
<div id="fb-root"></div>
<div class="navbar navbar-inverse navbar-static-top" style="background-color: #333333;">
<div class="container">
<div class="navbar-header">
<button type="button" class="navbar-toggle" data-toggle="collapse" data-target=".navbar-collapse">
<span class="icon-bar"></span>
<span class="icon-bar"></span>
<span class="icon-bar"></span>
</button>
<a class="navbar-brand" href="index.html">Logictools</a>
</div>
<div class="navbar-collapse collapse">
<ul class="nav navbar-nav">
<li class="dummy"><a href="index.html">Solve</a></li>
<li class="active"><a href="propositional.html">Propositional logic</a></li>
<li class="dummy"><a href="predicate.html">Predicate logic</a></li>
<li class="dummy"><a href="download.html">Download</a></li>
<li class="dummy"><a href="about.html">About</a></li>
</ul>
</div><!--/.navbar-collapse -->
</div>
</div>
<!-- content after titlebar -->
<!-- Main jumbotron for a primary marketing message or call to action -->
<div class="jumbotron" >
<div class="container" style="text-align: left; padding-left: 45px;">
<h1 class="jumbotron_title">Propositional logic</h1>
<p class="jumbotron_caption">Solvers and utilities to learn and hack
</p>
<p></p>
<div style="font-family: Arial, Helvetica, sans-serif;">
<a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">Solving</a> a
<a href="http://en.wikipedia.org/wiki/Classical_logic"> classical</a>
<a href="http://en.wikipedia.org/wiki/Propositional_calculus">propositional formula</a>
means looking for such values of variables that the formula becomes true. For example,
<tt>(a -> b) & a</tt> becomes true if and only if both <tt>a</tt> and <tt>b</tt> are assigned true.
<p></p>
You can select and try out several solver algorithms:
the "<a href='http://en.wikipedia.org/wiki/DPLL_algorithm'>DPLL</a> better"
is the best solver amongst the options offered on our page.
Read the "Methods for solving formulas" section below about the differences between algorithms.
<p></p>
One single suitable set of values
is enough as a solution: our solver algorithms stop and do not try to find additional solutions. Some of the solver algorithms
output the suitable values, but some do not, or output a partial set.
<p></p>
It may also happen that the formula is false for all possible values of variables: if so, the solver algorithms report
that after exhausting the search options. For example,
<tt>(a -> b) & a & -b</tt> is always false.
<p></p>
Notice that you can check whether some formula <i>F</i> is always true by trying to solve the
<b>negated</b> formula <i>-F</i>: in case <i>-F</i> is always false, <i>F</i> must be always true.
<p></p>
Our solvers may optionally output a trace of the search process. Select "html trace" to see the search
process.
<p></p>
For formula-syntax input our solvers first convert the formula to a
<a href="http://en.wikipedia.org/wiki/Conjunctive_normal_form">clause normal form</a>: for certain kinds of formulas this
conversion step may create a huge output, but in most cases it is a sensible simplification before actual search.
<p>
</div>
</div>
</div>
<div class="container" style="margin-top: 25px; margin-bottom: 25px;">
<h1 style="text-align: center">Methods for solving formulas</h1>
</div>
<div class="container">
<!-- Example row of columns -->
<div class="row">
<div class="col-md-12 wblock wblock1">
<div class="wiblock wiblock_full">
There are three main method categories for solving classical propositional formulas:
<p><p>
<ul>
<li><b><a href="http://en.wikipedia.org/wiki/Truth_table">Truth table</a> search</b>:
generate all possible assignment combinations for all the
variables in the formula and check for each assigment whether the formula is true. Since the number
of combinations is two to the power of the number of variables, this becomes infeasible for formulas
with a large number of variables.
<p></p>
This <a href="proplog_searchtable.js">"truth-table: naive"</a> method can be improved by checking also
<i>partial</i> assigments where only some variables have
been assigned values: it may happen that a formula becomes false even after just a few variables have been
assigned. This is implemented as the <a href="proplog_searchtable.js">"truth table: better"</a>
method on our page.
<p></p>
</li>
<li><a href="http://en.wikipedia.org/wiki/Resolution_(logic)"><b>Resolution search</b></a>:
the idea of the resolution method is to use a gneralization of
<a href="http://en.wikipedia.org/wiki/Modus_ponens">modus ponens</a> to derive
new clauses from the existing clauses. Clauses are derived until all combinations are exchausted or a contradiction is
derived. The resolution method should be seen as a general framework: actual solvers implement wildly different
strategies and optimisations.
<p></p>
Our <a href="proplog_naiveres.js">"resolution: naive"</a> method generates clauses in all possible ways and implements no optimizations.
The <a href="proplog_res.js">"resolution: better"</a> is significantly optimized: preprocessing clauses,
literals in clauses are ordered like [-3-1,2,5],
ordered resolution is used (only the first literal of a clause is selected),
always selecting the shortest usable clause as given,
storing and simplification by unit clauses (assigned variables),
forward subsumption of selected clauses and partial backward-subsumption.
<p></p>
While resolution has been the basis of most state-of-art
<a href="http://en.wikipedia.org/wiki/Automated_theorem_proving">predicate logic solvers</a>, for propositional logic
it is inferior to the DPLL method described next.
<p></p>
</li>
<li><a href="http://en.wikipedia.org/wiki/DPLL_algorithm"><b>DPLL (Davis-Putnam-Logemann-Loveland) search</b></a>
is essentially a constraint solver based on the combination of the truth table search with (limited)
resolution. For each partial assigment of values in the truth table search we (a) test whether the formula is
already false (like the "truth table: better" method above) and (b) use unit clauses (single literals) to derive new
unit clauses, which is essentially a limited version of resolution.
<p></p>
The DPLL method should be also seen as a general framework: actual solvers implement wildly different
strategies and optimisations. An excellent source for reading about various methods used by the state of the
art solvers is the <a href="http://minisat.se/Papers.html">collection of papers</a> by the authors of
<a href="http://minisat.se">Minisat</a>, a popular high-end solver. An important extension to DPLL is
<a href="https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning">Conflict-Driven Clause Learning</a>,
currently not implemented by the solvers presented on our page.
<p></p>
We provide three versions of DPLL solvers for experimenting, from worst (and easiest to understand) to
better and more complicated:
<ul>
<li><a href="proplog_naivedpll.js">dpll: naive</a>
a minimal, naive implementation of dpll with no optimizations. The code is very similar to the
<a href="proplog_searchtable.js">pure table search solver</a>.</li>
<li><a href="proplog_olddpll.js">dpll: old</a>
an improved <i>old-style</i> (before the improvements developed in nineties) DPLL.
It adds the pure literal rule (used after every unit propagation step), selects literals according to weights
calculated before the start of the search, organizes clauses into buckets associated with variables.</li>
<li><a href="proplog_dpll.js">dpll: better</a> implements additional widely used optimizations on
top of the "dpll: old" version (see, for example,
<a href="http://minisat.se/Papers.html">minisat papers</a> for explanations):
<ul>
<li>simple preprocessing before search starts: limited unit propagation/subsumption,
tautology deletion and pure literal deletion</li>
<li>does not use pure literal rule during search (too time-consuming)</li>
<li>learning variable weights: the last contradiction clause adds weights to the variables it contains</li>
<li>only two literals per clause are watched</li>
</ul>
However, the important
<a href="https://en.wikipedia.org/wiki/Conflict-Driven_Clause_Learning">Conflict-Driven Clause Learning</a>
strategy is not implemented.
</li>
<p></p>
</li>
</div>
</div>
</div>
</div>
<div class="container" style="margin-top: 25px; margin-bottom: 25px;">
<h1 style="text-align: center">State of the art solvers</h1>
</div>
<div class="container">
<!-- Example row of columns -->
<div class="row">
<div class="col-md-12 wblock wblock1">
<div class="wiblock wiblock_full">
The easiest way to find top level propositional solvers is to check the
<a href="http://www.satcompetition.org/">The international SAT Competition</a>: you
will see the competition results for various problem categories, can download competition
problems, source code and descriptions of the provers.
<p></p>
A good alternative choice is to check out <a href="http://minisat.se">minisat</a>:
an easily extensible and hackable state of the art solver which is a basis for several
other state of the art solvers. You can even run
<a href="http://www.msoos.org/2013/09/minisat-in-your-browser/">minisat in your browser</a>,
compiled from C to javascript using LLVM.
</div>
</div>
</div>
</div>
<div class="container" style="margin-top: 25px; margin-bottom: 25px;">
<h1 style="text-align: center">Parsing, converting and printing</h1>
</div>
<div class="container">
<!-- Example row of columns -->
<div class="row">
<div class="col-md-12 wblock wblock1">
<div class="wiblock wiblock_full">
The three building options "truth table", "clause normal form" and a "parse tree" are simple,
useful utilities implemented in <a href="proplog_parse.js">proplog_parse.js</a> and
<a href="proplog_convert.js">proplog_convert.js</a>:
<p><p>
<ul>
<li>
The <b>truth table</b> implemented in <a href="proplog_convert.js">proplog_convert.js</a>
prints a full
<a href="http://en.wikipedia.org/wiki/Truth_table">truth table</a>
of a formula up to 1024 rows: nice for checking out
small propositional formulas.
<p>
</li><li>
The <b>clause normal form</b> implemented in <a href="proplog_convert.js">proplog_convert.js</a> is a
<a href="http://en.wikipedia.org/wiki/Conjunctive_normal_form">conjunctive normal form</a> just as used by
the solvers. The conversion algorithm used is very simple and does not perform any optimizations. In many
cases the optimized converters like the
<a href="http://en.wikipedia.org/wiki/Tseitin_transformation">Tseitin transformation</a>
would give a much smaller output much faster.
<p>
</li><li>
The <b>parse tree</b> implemented in
<a href="proplog_parse.js">proplog_parse.js</a> prints a formula as a nested list built by the simple
<a href="http://en.wikipedia.org/wiki/Recursive_descent_parser">recursive descent parser</a>.
This list is later used by the
clause normal form converter to build the form suitable for solvers. Check the parse tree in case you are
not sure how the system understands your formula.
</li>
</ul>
</div>
</div>
</div>
</div>
<div class="container" style="margin-top: 25px; margin-bottom: 25px;">
<h1 style="text-align: center">Generating problems</h1>
</div>
<div class="container">
<!-- Example row of columns -->
<div class="row">
<div class="col-md-12 wblock wblock1">
<div class="wiblock wiblock_full">
<b>Generate a problem</b> button will call generators implemented in
<a href="proplog_generate.js">proplog_generate.js</a> to generate an example problem in a simple
<a href="http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf">DIMACS format</a>
of a clause normal form, suitable for solvers.
<p><p>
The options for the type of a problem are:
<ul>
<li><b>random 3-sat</b> generates a random set of
<a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem#3-satisfiability">clauses of length 3</a>,
using the number of
variables you choose: problems containing more variables are, on the average, harder to solve.
The number of clauses is always four times the number of variables: this
is, on the average, a specially hard-to-solve ratio for solvers.
<p><p>For DPLL try out 200 variables or
more. Truth table solvers start running into trouble with more than 20 variables. The resolution
provers are a bit better than the truth table solvers, yet much worse than the DPLL solvers.</li>
<li><b>all combinations</b> generates a set of clauses representing all possible combinations
of the input variables: any such set is unsatisfiable (i.e. no values of variables can make it true).
The number of clauses is hence always two to the power of the number of variables.</li>
<li><b>small unsat</b> generates a very small unsatisfiable clause set, consisting of a single long
clause containing all the variables and N single-element clauses containing all variables negated.</li>
</ul>
The <b>clear</b> button simply clears the input field and result.
<p>
You can also <b>browse</b> and read the contents of a file into the input area: essentially copy-paste from
a file.
</div>
</div>
</div>
</div>
<div class="container" style="margin-top: 25px; margin-bottom: 25px;">
<h1 style="text-align: center">Syntax</h1>
</div>
<div class="container">
<!-- Example row of columns -->
<div class="row">
<div class="col-md-12 wblock wblock1">
<div class="wiblock wiblock_full">
Use either a conventional formula syntax like
<pre>
(a -> b) & a & -b
</pre>
or a <a href="http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf">dimacs</a>
version of the clause normal form syntax like
<pre>
-1 2
1
-2
</pre>
which is a conjunction of disjunction lines with numbers standing for variables:
the last example means simply <tt>(-x1 v x2) & x1 & -x2</tt>
<p><p>
For conventional formula syntax:
<ul>
<li>negation symbols are <b>-, ~</b></li>
<li>conjunction symbols are <b>&, and</b></li>
<li>disjunction symbols are <b>|, v, V, or</b></li>
<li>xor symbols are <b>+, xor </b></li>
<li>implication symbols are <b>->, =></b></li>
<li>equivalence symbols are <b><->, <=></b></li>
</ul>
There is no operator precedence; all operators are bound from left:<br>
<tt>a & b v c & d v e</tt> is read as <tt>((((a & b) v c) & d) v e)</tt>
<p><p>
For dimacs you may use or skip the initial comment lines starting with <b>c</b>,
the special <b>p</b> line and the final <b>0</b> symbols at the end of each disjunct.
We allow the trailing <b>0</b>-s only at the end of a line.
<p>
I.e. you may use the full dimacs version like
<pre>
c comment
p cnf 2 3
-1 2 0
1 0
-2 0
</pre>
or just
<pre>
-1 2
1
-2
</pre>
</div>
</div>
</div>
</div>
<!-- footer -->
<div class="ofooter">
<div class="col-md-12 container ifooter">
</div>
</div>
<!-- at-end-scripts -->
<script>
// instead of jquery
function gid(x) { return document.getElementById(x); }
// reading a file
/*
function handleFileSelect(evt) {
var files = evt.target.files;
for (var i = 0, f; f = files[i]; i++) {
var reader = new FileReader();
reader.onload = (function(theFile) {
return function(e) { gid('propinput').value=e.target.result; };
})(f);
reader.readAsText(f);
}
}
gid('files').addEventListener('change', handleFileSelect, false);
*/
</script>
<!-- ui with bootstrap -->
<script src="http://ajax.googleapis.com/ajax/libs/jquery/1.11.1/jquery.min.js"></script>
<script src="http://maxcdn.bootstrapcdn.com/bootstrap/3.3.4/js/bootstrap.min.js"></script>
<!-- Solver code -->
<!--
<script src="proplog_ui.js"></script>
<script src="proplog_parse.js"></script>
<script src="proplog_convert.js"></script>
<script src="proplog_generate.js"></script>
<script src="proplog_dpll.js"></script>
<script src="proplog_olddpll.js"></script>
<script src="proplog_naivedpll.js"></script>
<script src="proplog_searchtable.js"></script>
<script src="proplog_naiveres.js"></script>
<script src="proplog_res.js"></script>
-->
</body>
</html>