tamura70/taocp-sat

TAOCP Satisfiability

Introduction

This repository provides Linux binaries and PDF files produced from the CWEB programs written by Donald E. Knuth for “Satisfiability”, Volume 4 Fascicle 6 of The Art of Computer Programming (TAOCP). The original CWEB programs were obtained on March 19, 2019 from:

• https://www-cs-faculty.stanford.edu/~knuth/programs.html

They were compiled on Ubuntu 18.04 with TeX Live 2018 by using the following Perl script.

• http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/knuth/install.pl

There were some errors during the compilation (see the following log file). Therefore, it is not guaranteed the compiled programs and PDFs are correct.

• http://bach.istc.kobe-u.ac.jp/lect/taocp-sat/knuth/install.log

These programs can be executed in Jupyter notebooks on Binder with Almond Scala kernel.

• https://mybinder.org/v2/gh/tamura70/taocp-sat/master?urlpath=lab/tree/notebooks/index.ipynb (in Japanese)

See the following web page for more details of how to run Knuth’s programs.

• Knuth先生の『TAOCP 7.2.2.2 Satisfiability』を読む (in Japanese)

Credits/Links

Binder setup scripts are obtained from Almond Examples.

• Almond
• Jupyter
• Binder