Satoku Matrix

Author:	Wolfgang Scherer

See http://sw-amt.ws/README-Satoku.html for an explanation of the satoku matrix.

To get started, put xemacs-fsf-compat.el somewhere in your load-path, then load satoku.el:

Press C-x C-e at end of the following expression:

(load-file "satoku.el")

or press:

`M-x load-file RET satoku.el RET'

Then execute the command satoku-insert-matrix:

`M-x satoku-insert-matrix RET'

Which will give you a Satoku matrix with a single clause sub-matrix:

// |    ||   S||  0|   0|| 1 1 1 |
// +----++----++---+----++-------+
// +-----+----++---+----++-------+
// |     |   0||   |    || 1 * * |
// |     |   1||   |    || * 1 * |
// |     |   2||   |    || * * 1 |
// +-----+----++---+----++-------+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Position point somewhere inside the matrix and execute:

`C-u M-x satoku-mode RET'

This constrains your cursor movements to the matrix and assigns special commands to certain keys. (Note: Outside the matrix, the keys work as usual).

Press ? for help.

Some commands are prefix commands (e.g. g). Press ? after the prefix command to get help.

To extend the matrix with another 3x3 clause sub-matrix, press:

`C-u 3 > >'

// |    ||   S||  0|   0|| 1 1 1 | 1 1 1 |
// +----++----++---+----++-------+-------+
// +-----+----++---+----++-------+-------+
// |     |   0||   |    || 1 * * | _ _ _ |
// |     |   1||   |    || * 1 * | _ _ _ |
// |     |   2||   |    || * * 1 | _ _ _ |
// +-----+----++---+----++-------+-------+
// |     |   3||   |    || _ _ _ | 1 * * |
// |     |   4||   |    || _ _ _ | * 1 * |
// |     |   5||   |    || _ _ _ | * * 1 |
// +-----+----++---+----++-------+-------+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Press > > to get a separator line:

// |    ||   S||  0|   0|| 1 1 1 | 1 1 1 ||
// +----++----++---+----++-------+-------++
// +-----+----++---+----++-------+-------++
// |     |   0||   |    || 1 * * | _ _ _ ||
// |     |   1||   |    || * 1 * | _ _ _ ||
// |     |   2||   |    || * * 1 | _ _ _ ||
// +-----+----++---+----++-------+-------++
// |     |   3||   |    || _ _ _ | 1 * * ||
// |     |   4||   |    || _ _ _ | * 1 * ||
// |     |   5||   |    || _ _ _ | * * 1 ||
// +-----+----++---+----++-------+-------++
// +-----+----++---+----++-------+-------++
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Press C-u 2 > > to get a 2x2 clause sub-matrix, repeat, and repeat again (hint: you can use keyboard macros).

Normal keys are disabled inside the matrix (but not the legend), use 0 to mark selection conflicts, - to clear a cell. (Mirror cells are automatically changed accordingly.)

Do not use 1 to mark required selections. Exclude all other selections with 0 instead:

// |    ||   S||  0|   0|| 1 1 1 | 1 1 1 || 1 1 | 1 1 | 1 1 |
// +----++----++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   0||   |    || 1 * * | 0 _ _ || _ 0 | _ _ | _ _ |
// |     |   1||   |    || * 1 * | _ _ 0 || _ _ | _ _ | _ _ |
// |     |   2||   |    || * * 1 | _ _ 0 || _ _ | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   3||   |    || 0 _ _ | 1 * * || 0 _ | _ _ | _ _ |
// |     |   4||   |    || _ _ _ | * 1 * || _ _ | _ _ | _ _ |
// |     |   5||   |    || _ 0 0 | * * 1 || _ _ | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   6||   |    || _ _ _ | 0 _ _ || 1 * | _ _ | _ _ |  a
// |     |   7||   |    || 0 _ _ | _ _ _ || * 1 | _ _ | _ _ | ¬a
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   8||   |    || _ _ _ | _ _ _ || _ _ | 1 * | _ _ |  b
// |     |   9||   |    || _ _ _ | _ _ _ || _ _ | * 1 | _ _ | ¬b
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |  10||   |    || _ _ _ | _ _ _ || _ _ | _ _ | 1 * |  c
// |     |  11||   |    || _ _ _ | _ _ _ || _ _ | _ _ | * 1 | ¬c
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Then press r u to run the requirements update algorithm, which detects and fills in the hard one requirements.

If you did use 1 and are no longer sure, whether the matrix conditions are proper, press r c to clear all hard one requirements. Then press r u to run the requirements update algorithm.

// |    ||   S||  0|   0|| 1 1 1 | 1 1 1 || 1 1 | 1 1 | 1 1 |
// +----++----++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   0||   |    || 1 * * | 0 _ _ || 1 0 | _ _ | _ _ |
// |     |   1||   |    || * 1 * | _ _ 0 || _ _ | _ _ | _ _ |
// |     |   2||   |    || * * 1 | _ _ 0 || _ _ | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   3||   |    || 0 _ _ | 1 * * || 0 1 | _ _ | _ _ |
// |     |   4||   |    || _ _ _ | * 1 * || _ _ | _ _ | _ _ |
// |     |   5||   |    || 1 0 0 | * * 1 || 1 0 | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   6||   |    || _ _ _ | 0 _ _ || 1 * | _ _ | _ _ |  a
// |     |   7||   |    || 0 _ _ | _ _ 0 || * 1 | _ _ | _ _ | ¬a
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |   8||   |    || _ _ _ | _ _ _ || _ _ | 1 * | _ _ |  b
// |     |   9||   |    || _ _ _ | _ _ _ || _ _ | * 1 | _ _ | ¬b
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |     |  10||   |    || _ _ _ | _ _ _ || _ _ | _ _ | 1 * |  c
// |     |  11||   |    || _ _ _ | _ _ _ || _ _ | _ _ | * 1 | ¬c
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Copyright