Don Knuth releases Volume 4, Pre-fascicle 6A [gzipped ps]
www-cs-faculty.stanford.edu
www-cs-faculty.stanford.edu
Seeing Knuth talk about tweets feels weird.
On another note, anyone actually run into a random k-SAT problem in "real life"?
Does it make you feel better that he released the book as a .ps?
All of the fonts in that postscript file are bitmaps. Knuth started with metafont, but the file he distributed only contains bitmaps.
If you look inside the file, you'll find the comment "DVIPSBitmapFont". And if you convert it to PDF and zoom in, you'll see that the fonts are bitmaps. This is typical for TeX files generated by dvips prior to the widespread adoption of the Type1 equivalents for the computer modern fonts.
Fortunately, the file was generated by a recent version of dvips, so the "pkfix" script can be used to rewrite it with Type1 fonts substituted for the bitmapped fonts. I'd recommend doing this before converting it to PDF.
It's a bit harder to fix this after PDF conversion. A few years ago, I wrote some Java code to do it (inspired by "pkfix-helper"), but it worked off of font metric signatures so it's not very accurate for small font subsets (e.g. exponents). To fix this, I need to actually look at bitmaps (or ask the user), and I never got around to implementing that.
I suppose it's a minor issue, but it is a pet peeve of mine. I've come across a lot of papers on the net in PDF or PS format that look unnecessarily bad when viewed on a computer screen.
Because there's a lot of research into solving SAT "pretty quickly", one of the half-reasonable ways to approach an NP-complete problem is to find an efficient reduction and use a premade SAT solver/heuristic. I don't think nearly as much work has gone into that sort of thing as, say, integer programming (http://en.wikipedia.org/wiki/Integer_programming), but I remember reading something about it a couple of years ago.
Of course, when people realise their problem is NP-complete they tend to go a different way with things. The usual answers are:
1. Problems in practice are small enough for brute-force (or a simple backtracking search)
2. We probably don't need optimality, just use some kind of heuristic or metaheuristic.
3. Too hard, let's do something else.
From what I've heard, researchers are actually rejoicing, once they are proven a problem is in NP (instead of something worse or unknown status): because that's means it's quite likely that most of it's instances are tractable and we know lots about how to solve NP problems.
I believe SatPlan (1992) initiated that trend, by showing that compiling classical planning problems to SAT can get significant speedups over traditional planning algorithms in some cases. This ties into another, mostly informal hallway debate so far, over whether AI needs a replacement idea of "AI-completeness" to specify the problems that are really hard from an AI perspective. I wrote a short opinion piece on that a few years ago: http://www.kmjn.org/notes/nphard_not_always_hard.html
A more common problem than SAT not being fast enough is the reduction being intractable. It's ok if it's "big" (SAT solvers can solve for millions of variables), but it's easy for naive encodings to generate truly absurd blowups, gigabytes or more, which can make it intractable to even state the SAT problem, i.e. write it to disk or send it over a pipe. If you avoid that problem, the actual SAT-solving step is usually fast. I believe that's where some of the interest in alternatives to SAT comes from, as compilation targets, so to speak, that are easier to generate non-blown-up code for.
SAT-heritage grounding targets are still common in logic programming, though, e.g. http://potassco.sourceforge.net/ uses a SAT-like approach, though one specialized for answer-set programming rather than directly targeting SAT.
My impression is that there's a little bit of tool-choice segregation by community, with OR people, AI people, software-verification people, and PLs people each having their own favorite tools, and not as much overlap as there could be.
Granted, I haven't mustered the courage to begin reading TAOCP, but my impression is it's a timelessly relevant masterwork for the man.
First example from this new section about satisfiability, the epigraphs:
> “He reaps no satisfaction but from low and sensual objects, or from the indulgence of malignant passions.” – David Hume, The Skeptic (1742)
> “I can’t get no ...” — Mick Jagger & Keith Richards, “Satisfaction” (1965)
Or an example from the text, from a few pages later on:
> “Start with any truth assignment. While there are unsatisfied clauses, pick any one, and flip a random literal in it.”
> Some programmers are known to debug their code in a haphazard manner, somewhat like this approach, and we know that such “blind” changes are foolish because they usually introduce new bugs....
I don't think Knuth is under any illusions about staying relevant: The original editions had code examples for a machine having 6-bit bytes and used self-modifying code to store the return address of subroutines rather than a stack.
In later editions he updated the examples, but even with respect to algorithms the new fascicles make references to quite recent papers and results. The books as timeless as they are, are products of their time more so than most books on mathematical topics.
I'm betting "social" and "network" will still be recognizable words in 50 years too.
It might just give the whole work a nice and quaint touch.
[1] https://twitter.com/pervognsen/status/230892091188846592
I would have to google pretty much all of that, which is inconvenient. It should have linked to a page describing what it is, even if OP had to make it himself. Its only blogspam if you put ads on your blog... which I'd hope anyone here doesn't.
For your assertion that it should link to a page describing what it is, I think you're wrong and I don't think you addressed my point about that being less efficient. Even in your case, I think it's more efficient this way. I don't think you would understand much in the submission without a lot of googling, and that's if you're even interested in understanding (which I doubt given your resistance to merely typing "define:fascicle" into Google) in the first place. A blog post describing the work would tell you as much, but since you didn't even understand the title, you already knew that you likely wouldn't understand the work. (Gods help you if you're on Windows and can't read PS files without downloading stuff from websites you've never visited.) An incomprehensible (to you) title saved you time. It's better for you this way. You did ruin your potential efficiency gains by spending time complaining about the submission type in the comments, much more time than it would take to google the parts of the title you didn't understand, but you knew that already when you ventured to the comments (which people seem to do regardless of the format of the content--I know I often get more out of the comments than the submission itself and sometimes will skip the submission entirely).
Edit: I will grant that there is an additional improvement to the title. Adding to the end "on Satisfiability". Which wouldn't help anyone not inclined to google but does at least say more specifically what it's about.
Reading the TeX source online?
I'd make it public, but that would be a copyright violation.
I wonder if Google hashes and caches the result. If they do the next upload should be much faster for anyone.
$ curl -s http://www-cs-faculty.stanford.edu/~knuth/fasc6a.ps.gz | dd bs=16 count=1 | xxd
0000000: 1f8b 0808 689e 1150 0203 6661 7363 3661 ....h..P..fasc6aNot only prevalent, but also the right thing to do. PDF was an attempt to (among other aims) achieve smaller filesizes than PS. But that was premature optimization: While a PS file is usually bigger than a PDF, gzipped PS beats PDF.