Unary Logic Functions

Let's have a look at unary logic functions. There are exactly four of them (this is a very useful application of combinatorics):

These functions can be described as follows:

• X1 stands for single selection (exactly one selection must be made, i.e. exactly one of the variables must be true).
• MS stands for multiple selection (one ore more selections must be made, i.e. one ore more of the variables must be true).

Lemma: The correct representation of unary logic function F0 would be F0,1 -- but DOGgy style allows to have faith in the ability of the reader to understand the concept of context.

In this case, there is no need within a section about unary functions to redundantly identify all functions as unary. (It's implicit, dummy.)

Binary Logic Functions

Let's have a look at binary logic functions. There are exactly 16 of them (another useful application of combinatorics):

These functions can be described as follows:

Hmm, besides the selection thingies, not much new.

Ternary Logic Functions

Ternary logical functions are defined by subsequent application of the binary function to the result of the binary function and the next logical value, e.g.:

OR(p, q, r) = ((p OR q) OR r)

F127,3(p, q, r) = F7,2((F7,2(p, q), r)

Generally, any n-ary logic function can be recursively broken down to repeated applications of the binary version:

f[n] ( v0, .., v[n-1] ) = f[2] ( f[n-1] ( v0, .., v[n-2] ), v[n-1] )

Now, isn't that nice! All those theorems and lemmas and transitivities and distributivities and symmetries, you name it! And then there is no need to examine all those n-ary functions in a truth table, it's just great! Logic seems very mathematical indeed.

I should not have been surprised, when I discovered that I was using antivalence (XOR) and single selection (X1) interchangeably (which is correct in binary contexts only).

Lemma: DOGgy style predicts, that you will keep confusing similar but not identical concepts for quite some time before realizing that there is a difference.

The difference is that n-ary single selection cannot be broken down to a binary single selection applied to the result of an (n-1)-ary single selection and a truth value:

F105,3(p, q, r) == F6,2(F6,2(p, q), r) # XOR
F104,3(p, q, r) != F6,2(F6,2(p, q), r) # X1

It is possible to define a quasi-ternary logic, to be used for intermediate results, which allows to process n-ary single selections in the usual manner. Here 1 stands for true and 0, -1 both stand for false. But I am not sure whether that helps :).

F104,3(p, q, r) = FX2(FX2(p, q), r) > 0

If you present someting like this, you will immediately arouse heated excitement (and not of the good kind). You are mixing boolean operators with arithmetical operators. It does not matter, that your programming language allows you to do so and that it is therefore a correct model of what your program does. It is still forbidden, since you have not explicitely stated, that you are talking Programmese. And it is also forbidden to take other people's hard work and deface in such an apalling way. You are hereby expelled from the calculus. Nothing you say makes any sense at all!

Lemma: In DOGgy style programming it is always a good idea to mention very early on, that you are using Programmese to describe the features of your program. If need be, contact me and I will set up a Bitbucket project about the promising ongoing research in Programmese, which will state that a formalized theory will be presented real soon. This will not only protect you from attacks, but it will elicit the impression that you are on the bleeding edge of the next best hype in computer science.

So, the interesting ternary functions regarding selection are these:

The functions can be described as follows:

Historic Context

Before talking about SAT-problems, I would like to limit the expectations in regard to that matter (beware of DOG!).

At the time when I started fiddling with SAT problems (around 2004), the available material still cited the worst case for a brute-force attack:

"It takes worst case exponential time (2^n) over the variables, if there is only a single solution (or no solution at all), and if that solution (contradiction) is found last[5]."

// clauses:  1105
// max literal count: 17

// clauses: 319
// 2-SAT clauses: 140
// k-SAT clauses: 179

I was under the impression, that it must be a lot harder to find all solutions. And since I was looking for a hobby to last me a lifetime, I thought that it would make no difference just how unsolvable the problem is. In order to understand the structure of a problem, I decided it was best to acquire as much information as possible and went with trying to find all possible solutions instead of just a single one.

I did not set out to prove P vs. NP or be the fastest kid on the block. I was just curious, whether I could get a clue as to why that problem was so hard.

Since my goal was different from the standard research in this field (and since I cannot understand mathematical texts so well), I did not do a lot of research. Instead I wrote programs to visualize the problem structure and explore various algorithms.

The purpose of the programs I wrote is to facilitate analysis of logical k-SAT problems. The exponentiality is still there, I just have a much better idea why that is so. And I have a tool to perform logical reasoning in a geometrically structured environment without the symbolic clutter of algebraic symbols.

The satoku matrix scales well from 1-SAT to k-SAT and back, and it delivers a polynomial time 2-SAT solver without the need to search for a solution. That is aesthetically especially nice. (I.e., I like my program better, but who wouldn't :)).

I find it funny, that it turns out to be actually slightly more efficient to find a single solution when searching for all possible solutions simultaneously, than it is when searching for a single solution only.

The current state of affairs allows me to get a good upper bound on the worst-case running time per individual problem, so that I can display the message "No need to get up" or "You can go on a nice trip to Hawaii". This is good, since you are supposed to always give progress feedback to the user.

Lemma: If you feel the need to explain yourself -- as most DOGgy style programmers do as a pastime -- you should consider bringing that up at your next PA (Programmers Anonymous) meeting. If you cannot suppress the urge to do it right there and then, at least consider putting the stuff in a footnote or an appendix. It's just boring for everybody else and does not change the facts. But thanks for sharing.

Course of Events

Satisfiability problems are sometimes defined in a manner as in the following citation from 2-satisfiability on Wikipedia (emphasis added by me):

The 2-satisfiability problem is to find a truth assignment to these variables that makes a formula of this type true: we must choose whether to make each of the variables true or false, so that every clause has at least one term that becomes true.

I had read that "each SAT problem gives rise to a similar selection problem, which is again NP-complete"[someone]. I misunderstood this as a selection problem being the same problem and the at least to stand for multiple selection[6]:

Select (multiple) literals from clauses so that at least one of them is true.

The proper form is to demand that exactly one literal must be selected from each clause (single selection), so that no two selected literals represent a variable and its negation.

Although the assignment of a truth value may seem implicit, there is no necessity to do so. (It will later become obvious, why it is a good thing, that actual assignment can be deferred indefinitely).

It is obvious, that the condition for proving satisfiability for a selection problem can be met without actually making any truth value assignment. Even, if the implict assignment of True to a selected variable:

literal = variable → variable = T

or False to a selected negated variable:

literal = ¬variable → variable = F

is accepted, that still leaves cases where it is it not necessary to select all of the variables.

In the trivial case, where all variables only appear once in a formula, it is even impossible to make a satisfying selection which contains all variables. E.g.:

(a ∨ ¬b ∨ c) ∧ (d ∨ e ∨ ¬f)

Fun fact: in this case, it is not even necessary to make any selection or assignment. Since there are no conflicts, all assignments satisfy the problem.

However, once such a partial core-assignment is found, all fully assigned solutions that statisfy the multiple selection property can be trivially derived through permutations[7] of the possible truth values over the remaining unassigned variables.

The statement "Formula X is satisfiable" becomes true, as soon as the single selection condition is met. The assignment of thus far unassigned variables does no longer have an influence on that truth value[8].

In other words: It is possible, that a fully assigned solution cannot be presented by single selection. Nonetheless, it is certain, that a fully assigned solution can eventually be constructed and that it will take at most linear time over the set of unassigned variables to do so.

The fact that it is necessary to assign all variables for a complete assignment of truth values is completely off-topic. Even for the decision problem variant, a partial assignment is already sufficient to check the validity of the prospective fully assigned solutions: If there is any true assignment present in a clause, the condition at least is already satisfied. No reason to demand more[9].

What is the reason behind the demand, that all variables must be assigned? The principle of excluded middle? Logicians can only count to 1? My computer ran out of numbers? I could not find a class in Java? Too much effort, maybe?

If 1 represents true, 0 represents false and -1 represents unassigned, then the following algorithm correctly checks the validity of a partially assigned solution (it also works, if all variables are assigned):

good = False # I cannot remember whether an empty clause set
good = True  # signifies True or False \|:todo:|
             # So I go with: `Is a non-existent problem satisfiable`? A: yes
for i in range(len(clauses)):
    clause = clauses[i]
    good = False
    for j in range(len(clause)):
        if clause[j] == 1:
            good = True
            break
    if not good:
        break
if good:
    print("SAT")
else:
    print("UNSAT")

This algorithm does exactly, what the definition of the problem demands for verifying a solution. I have to admit I'm stumped.

Lemma: In DOGgy style programming it is true, that Thou shalt not rant!. Remember principle 3 of DOGgy style programming. As RMS once pointed out:

Criticizing the flaws of other people's thinking about the problem does not help me understand the problem or your solution. So it is best to leave that out.

Or bring it up at your PA meeting.

Corollary: Ranting usually means, that you have not fully understood a mechanism. Wait a while until it becomes clear. If ranting helps you to bide your time, feel free to do so. However, you should not publish the rant, but rather replace it with the enlightenment you have found. In this special case, you can keep the rant to demonstrate the principle.

Corollary: Try to find out, why you don't understand it. What is the context of the statement[10]? Maybe ask somebody else.

Lemma: However, this example is still useful to show why in DOGgy style programming you must not fall prey to decision-making-OCD. All decisions must be procrastinated until they are absolutely necessary. And even then, you should rather spend your time with making excuses for not yet deciding, than acting against that gut-feeling that still tells you that the decision is potentially dangerous. Good half-truths are always: "The code needs to be cleaned up", "An important part of the program needs attention, because it can still turn the whole project into a failure".

Experience shows, that right after you irrevocably made the decision and cleaned up your program in many places, you will all of a sudden realize in clairvoyant brilliance why it was dumb to make the decision the way you made it. You will blush and your gut-feeling will smirk (again): "told you so!"

Corollary: This leads directly to the rule, that in DOGgy style programming you must never ever work without version control. No matter how much other people insist on it not being necessary when you work on your own. This is their own varition of delusions of grandeur, that you must never deal with.

Lemma: Gut-feeling (or intuition) is a central part of DOGgy style programming. It is the part of yourself that eludes conscious control and the driving force behind DOGgy style programming. Therefore, DOGgy style programming can never be a conscious process and no rigid model can ever be constructed. But you must never stop to try, since the journey is the destination.

As multiple selection turns out to be just another name for a disjunction (OR), I will refer to single selection (X1) as simply selection from here on out (and maybe above, if I forget, that plain selection is not supposed to appear before this point, or as I'm sure to forget, that I must move this paragraph to the beginning.) (|:todo:| don't! This TODO serves as a perfect example for a bad TODO. The requested action should have happened immediately).

Satoku - The Game

Although a game of Satoku can be played entirely with pencil and paper, it is best played in Emacs with satoku-mode. (Get satoku.el, see Satoku README for basic instructions).

The examples from this article are included in the package to make it easier to follow the argument.

Design Principle

The design principle for this algorithm is based on the concept of strong decisions and weak decisions, where

• a strong decisions is a decision that never has to be reversed
• a weak decision is a decision that possibly needs to be reversed (backtracking).

The goal of the algorithm developed here is to avoid weak decisions as long as possible and still provide a useful tool for structural analysis of boolean satisfiability problems.

Independent Set Problem and Adjacency Matrix

As shown in David M. Mount, CMSC 451 Lecture Notes, Fall 2012[13], pp. 92, a 3-SAT problem can be mapped to an independent set problem in polynomial time.

Before I found this proof, I illustrated the principle with a game called Pick-A-Puck (I should have used an undirected graph, but I did not know too much about graph theory).

Lemma: If you do proper research and talk to the right people, you can save a lot of time and effort. You will also find out, what the rest of the world accepts as proof and what not. DOGgy style programming ist not about sloppiness! It is about efficiency!

The mapping to an independent set problem ensures, that only one literal can be selected from each clause. (Not so) coincidentally that is excatly what the single selection function requires.

Independent set problems can further be mapped to an adjacency matrix, which can be inverted directly during mapping by exchanging 0 and 1.

Mapping the following CNF 3-SAT formula:

(¬a ∨ ¬b ∨  c) ∧
(¬a ∨  b ∨ ¬c) ∧
(¬a ∨  b ∨  c) ∧
( a ∨ ¬b ∨ ¬c) ∧
( a ∨ ¬b ∨  c) ∧
( a ∨  b ∨ ¬c) ∧
( a ∨  b ∨  c)

to an inverted adjacency matrix looks like this:

You could now go ahead and use algebraic methods on this construct, or whatever it is, that is available for this structure (I should do some research one of these days). Or you can choose to go another route.

Lemma: DOGgy style programming is all about choice and pleasing someone (if not the customer, than at least yourself). If you can support different possiblities at minimal cost, you should always do so, no matter whether it is currently needed or not.

Satoku Matrix

The inverted adjacency matrix of the independent set graph does not show the clause restrictions, which were explicitly introduced during the mapping (and are therefore implicit in the final inverted adjacency matrix). However, the information is readily available during mapping and allows to subdivide the matrix into regions, which clearly indicate the relation of the matrix to the mapped clauses:

This augmented inverted adjacency matrix is called satoku matrix (SM) to clearly indicate, that the algorithm is unrelated to graph theory. Whether graph theory does or does not apply beyond the basic property of mapping a SAT problem correctly to an (inverted) adjacency matrix is outside the scope of this discussion.

Lemma: In DOGgy style programming, when something acquires different properties (be they substantial or merely oranmental), it must get a new name to avoid ambiguities. You can always call it XXX or use the placeholder system of your choice, if you cannot think of a name right now.

In the context of selection rows, a matrix cell is denoted as c[[i, j], [f,g]] corresponding to selection rows s[i,j] and s[f,g].

The truth value instances of 1 in the SM{} are classified based on the number of occurrences in a clause segment of a selection row.

• If a clause segment in a selection row contains more than one matrix cell with the value 1, the values are replaced by a dash (-) and called soft one. Note that the truth value of a soft one is still 1, the substitution is merely ornamental.
• If a clause segment cs[[i,j], f] in a selection row s[i,j] contains exactly one matrix cell c[[i,j], [f,g]] with the value 1, the value is unchanged and called a hard one. The corresponding selection row s[f,g] becomes a required (or necessary) selection for selection row s[i,j].

After these rules are applied, the satoku matrix looks like this:

For a better overview, a status row, representing the selection status of the entire problem is introduced. It is labeled P and behaves essentially like a matrix row. If an entire column of the satoku matrix becomes 0, the corresponding cell in the status line also becomes 0:

Finally, the original SAT problem is augmented with some tautologies to represent the (possible) selection of either a variable or its negation[14]:

(¬a ∨ ¬b ∨  c) ∧
(¬a ∨  b ∨ ¬c) ∧
(¬a ∨  b ∨  c) ∧
( a ∨ ¬b ∨ ¬c) ∧
( a ∨ ¬b ∨  c) ∧
( a ∨  b ∨ ¬c) ∧
( a ∨  b ∨  c) ∧
( a ∨ ¬a) ∧
( b ∨ ¬b) ∧
( c ∨ ¬c)

Proof: For all propositional formulas F the following statement is true:

Lemma: In DOGgy style programming proofs are way cool! Give them, if you can. But don't worry too much about them. If your program works, there is no need to prove it.

Since these tautologies are entirely optional, they are separated from the original core problem (upper left matrix region) by a double line.

So the final satoku matrix looks like this:

• A dash (-) is merely a substitution for the truth value 1, if there is more than one matrix cell containing the value 1 present in a clause segment of a selection row.

• A selection row is an entire satoku matrix row, which represents a selection from a clause of the mapped SAT problem including the dependencies on all other selections.

  The selection row indexing refers to literal j from clause i of the mapped SAT problem.

• satoku matrix subdivisions limited by horizontal lines represent clause sub-matrixes S[i], containing one or more selection rows.

  Clause sub-matrixes are further divided by vertical lines into clause conflict sub-matrixes S[i, f], where f has the same range of values as i.

  A clause conflict sub-matrix S[i, f] represents the dependencies between all selections from two SAT problem clauses S[i] and S[f].

  The special clause conflict sub-matrix S[i, i] is called clause identity sub-matrix.

• A clause segment cs[[i,j], f] is the intersection of selection row s[i,j] and clause conflict sub-matrix S[i,f].

• The row labeled P is not part of the matrix, it shows the status of globally possible (- or +), required (1) and impossible (0) selections.

• The double lines are just visual aids to separate semantically different groups (e.g., core problem clauses and variables). They have the same meaning as a single line.

• The right margin is used for comments which can be completely ignored.

Do you remember, that the clauses are mapped to single selection clauses and that single selection is equivalent to XOR in a binary context? So the additional variable clauses can also be read (sel(p) XOR sel(¬p)) in the context of the satoku matrix.

Lemma: If you are suffering from instant-cleanup-OCD or everything-must-have-a-purpose-OCD, unnecessary things are thrown away. However, in DOGgy style we never throw anything away, even if we do not (yet) know, whether it is useful or not (it does at least visualize a concept in this case). If we do not know all facets of the problem yet, it may come in useful later on.

Satoku Matrix Properties

For general matrix cell properties, the standard index scheme for row f and column g is used (f, g ∈ (0,1, ..)) . Rows are denoted by r[f], matrix cells are denoted by c[f,g].

• An inverted adjacency matrix is necessarily symmetrical (mirrored at the matrix diagonal). This property follows from mapping an undirected graph to an inverted adjacency matrix. This property also holds for the satoku matrix.

• The row and column indexes of a matrix cell are equivalent to the row indexes of the related rows. E.g., cell c[3, 5] refers to row r[3] and row r[5].

• If the value of the matrix cell c[f,g] is zero (0), it is said that the selection of row r[f] depends on (conflicts with) the selection of row r[g], or that selection of row r[f] makes selection of row r[g] impossible.

  Due to symmetry, it can also be said, that selection of row r[g] depends on (conflicts with) the selection of row r[f].

• If the value of the matrix cell c[f,g] is one (1), it is said that the selection of row r[f] is independent from the selection of row r[g].

  Due to symmetry, it can also be said, that the selection of row r[g] is independent from the selection of row r[f].

Fun fact (just to see, whether TeX conversion works): Given a set of clauses C and a set of variables V, the matrix cell count MC is:

Therefore the space requirements of the mapping algorithm are O(m^2).

Requirements Update Algorithm

The satoku matrix is used as a dynamic data structure. It is therefore necessary to define the operations in a manner as to preserve the properties of an inverted adjacency matrix.

Requirement Update Example

Here is an example to illustrate the requirement update.

Transition 1 -> 0:

Mark requirement updates:

First requirement update leads to 1 -> 0 transition and more requirement updates:

This continues:

until the last requirement update does not cause any changes:

Other Operations

In the context of this discussion, a satoku matrix is also manipulated in the following ways:

• Selection rows (and corresponding columns) are removed.
  • Requirements update algorithm is not necessary if the selection row was already unselectable.
  • Requirements update algorithm is necessary after each removal of a selectable row (rows must be removed sequentially).
• Entire clause sub-matrixes (including their vertical counterparts) are removed. There is no action necessary after removal.
• Entire empty clause sub-matrixes (including their vertical counterparts) are added. There is no action necessary after addition.
• Selection row conflicts are added manually. Requirements update algorithm is necessary after any change to a selection row.

Conflict Maximization

It becomes obvious, that zeroes and hard ones are a good thing. Soft ones eventually require a decision to be made, which is known to be prone to inefficienct backtracking.

So, let's extend the original formula a little. The following extension:

is applied to the previous SAT instance:

(¬a ∨ ( a ∧ ¬b) ∨ ( a ∧  b ∧  c)) ∧
(¬a ∨ ( a ∧  b) ∨ ( a ∧ ¬b ∧ ¬c)) ∧
(¬a ∨ ( a ∧  b) ∨ ( a ∧ ¬b ∧  c)) ∧
( a ∨ (¬a ∧ ¬b) ∨ (¬a ∧  b ∧ ¬c)) ∧
( a ∨ (¬a ∧ ¬b) ∨ (¬a ∧  b ∧  c)) ∧
( a ∨ (¬a ∧  b) ∨ (¬a ∧ ¬b ∧ ¬c)) ∧
( a ∨ (¬a ∧  b) ∨ (¬a ∧ ¬b ∧  c)) ∧
( a ∨ ¬a) ∧
( b ∨ ¬b) ∧
( c ∨ ¬c)

Proof: With:

A = ¬p ∧ q
B = ¬p ∧ ¬q ∧ r

induction over the full truth table:

p	q	r	¬p	¬q	A	B	p ∨ q ∨ r	p ∨ A ∨ B
0	0	0	1	1	0	0	0	0
0	0	1	1	1	0	1	1	1
0	1	0	1	0	1	0	1	1
0	1	1	1	0	1	0	1	1
1	0	0	0	1	0	0	1	1
1	0	1	0	1	0	0	1	1
1	1	0	0	0	0	0	1	1
1	1	1	0	0	0	0	1	1

shows that (p ∨ q ∨ r) and (p ∨ A ∨ B) are logically equivalent.

For the mapping of a SAT problem to a satoku matrix it is necessary to decide, whether a literal and a conjunction can be selected independently or not. This is formalized in the following statements.

A literal l and a conjunctive clause C can be selected independently, if the literal l can be selected independently from all literals l[c] of C:

Proof: is trivial: p ∧ (q ∧ r) = (p ∧ q) ∧ (p ∧ r).

Two conjunctive clauses C0, C1 can be selected independently, if all literals l[i] of C0 can be selected independently from all literals l[j] of C1:

RT: O(k^2), k = |C|

The extended SAT formula is now mapped into the satoku matrix and the requirements update algorithm is applied:

Surprised much? Probably not. The CNF formula was just an encoded conjunction (a ∧ b ∧ c) to begin with. (I chose it for the high density instant solution effect).

Here are some more properties that can be observed:

• Rows that require each other become identical (this can be used to optimize the requirements update algorithm).
• If a clause has only one selectable row, that row is required by all other clauses (1-SAT property).
• Unselectable rows and their corresponding columns can be removed from the matrix. (Note, that this may break the relation between selection row indexes and clause literal indexes).
• If two clauses consist of only identical rows (each row of one clause requires exactly one row in the other clause) (redundant clauses), one of the clauses (rows and corresponding columns) can be removed from the matrix. (Note, that this will break row/clause index relations).
• A redundant clause can also be removed, if each row of a clause presents the same conflict structure as a row in the other clause (except for the clause segments at the matrix diagonal). (Note, that this also breaks row/clause index relations).

Here is the result, after cleaning up the satoku matrix:

For obvious reasons, the variable selection clauses have been left intact. However, the selection indices have been removed because they do no longer represent the selection row/SAT clause relation correctly.

Lemma: Once a problem is solved, it is good to clean up. Since all disambiguities have been resolved. It is also good to remove information that is no longer applicable!

Merging Clause Sub-Matrixes

Iff a single selection must be made from one clause and a single selection must be made from another clause, then a single selection must be made from the possible combinations of exactly one literal from one clause and exactly one literal from the other clause:

X1(p, q) ∧ X1(r, s) ↔ X1(p ∧ r, p ∧ s, q ∧ r, q ∧ s)

Proof:

Let statements A and B be:

A = X1(p, q) ∧ X1(r, s)
B = X1(p ∧ r, p ∧ s, q ∧ r, q ∧ s)

Induction over the full truth table shows, that statement A and statement B are logically equivalent:

p	q	r	s	X1(p, q)	X1(r, s)	A	p ∧ r	p ∧ s	q ∧ r	q ∧ s	B	A
0	0	0	0	0	0	0	0	0	0	0	0	0
0	0	0	1	0	1	0	0	0	0	0	0	0
0	0	1	0	0	1	0	0	0	0	0	0	0
0	0	1	1	0	0	0	0	0	0	0	0	0
0	1	0	0	1	0	0	0	0	0	0	0	0
0	1	0	1	1	1	1	0	0	0	1	1	1
0	1	1	0	1	1	1	0	0	1	0	1	1
0	1	1	1	1	0	0	0	0	1	1	0	0
1	0	0	0	1	0	0	0	0	0	0	0	0
1	0	0	1	1	1	1	0	1	0	0	1	1
1	0	1	0	1	1	1	1	0	0	0	1	1
1	0	1	1	1	0	0	1	1	0	0	0	0
1	1	0	0	0	0	0	0	0	0	0	0	0
1	1	0	1	0	1	0	0	1	0	1	0	0
1	1	1	0	0	1	0	1	0	1	0	0	0
1	1	1	1	0	0	0	1	1	1	1	0	0

Note, that p, q, r, s stand for the truth value of a selection being made, they do not refer to any boolean values of variables in the underlying SAT problem. (I hope that is enough).

The problem with this proof is, that n-ary single selection X1 cannot be defined recursively like other logical functions. So it could be argued, that it should be proved for all possible cases of n-ary single selection, which of course is not possible. If anybody has a better idea, please, let me know (combinatorics maybe?).

From what I understand, that principle is somehow related to the DPLL algorithm and possibly does not need to be proved. That would be nice.

Lemma: DOGgy style programming encourages you to prove things to yourself. Choose the method best suited for your purpose and don't worry about other people so much. You can find out later, what the correct way is.

I think I have a better idea! Based on De Morgan's laws and the distributive property, P ∧ (Q ∨ R) = (P ∧ Q) ∨ (P ∧ R), a different proof would be as follows. The equivalence

(p ∨ q) ∧ (r ∨ s) = ((p ∧ r) ∨ (p ∧ s) ∨ (q ∧ r) ∨ (q ∧ s))

allows to transform the conjunction of two disjunctive clauses into a single disjunctive clause with 4 conjunctive sub-clauses. According to the principle of conflict maximization, this constitutes a single clause SAT problem which can be mapped into a single clause satoku matrix.

Back on topic, let's start with the example conjunction from above. The goal is to merge clause sub-matrixes S0 and S5.

When counting the possible and impossible selections in the clause conflict sub-matrix S[0, 5] at the intersection of row S0 and column S5, the number of possible selections is the predicted number of selection rows, which the merge result will have (in this case: 6).

Both clause sub-matrixes S0 and S5 have 3 selection rows each. The number of possible combinations is therefore 3 * 3 = 9.

Start merging by adding an empty clause sub-matrix with 9 rows and columns (press `C-u 9 > >' in satoku-mode), and fill out clause conflict sub-matrix S[7, 0] with requests for all selection rows of clause sub-matrix S0. Each request must be repeated twice for a total of 3 requests per selection row:

Now clause conflict sub-matrix S[7, 5] is also filled with 3 requests each per selection row of S5. However, the order of the requests must be chosen such as to produce all possible combinations of selection rows:

When the requirements update algorithm has finished (press `r u' in satoku-mode), the satoku matrix looks pretty torn up:

After removing the impossible selections (rows/columns with all zeroes) (press `d l' in satoku-mode on a row with all zeroes to delete it[sm-single]), a conflict free satoku matrix is revealed, which still has some single row clauses (aka. 1-SAT clauses) and two identical clause sub-matrixes (they require each other):

The final result, after removing the trivial single row clause sub-matrixes and the redundant clause sub-matrix (press `d L' in satoku-mode to remove a clause sub-matrix):

All selection rows can be mapped to truth assignments of the SAT problem variables, since no conflicts (zeroes) are present.

It appears as if there are many solutions to the problem, but when the variables are also mapped, it can be seen, that the truth value assignment for all selection rows is identical. The effective assignment is the single solution for the conjunction (a ∧ b ∧ c):

Conflict Comparison

The special clause identity segment cs[[i,j], i] is ignored in each selection row, when comparing the conflicts of selection rows. The difference in the clause identity segments trivially states, that the selection rows represent different selections. But clearly the effects of different selections can still be the same.

E.g., given two selection rows s[0, 0], s[0, 1]:

for the purpose of conflict comparison, the clause identity segments cs[[0, 0], 0] and cs[[0, 1], 0] are assumed to be set to 1:

The comparison shows, that the effect of either selection is identical in the core problem sub-matrix and that the effect is different in the variable section.

Whether selection rows conflict with each other or not is immaterial for conflict comparison. It follows for selection rows in different clauses, that both clause identity segments are ignored in both selection rows.

E.g., given two selection rows s[0, 0], s[1, 0]:

for the purpose of conflict comparison, the clause identity segments cs[[0, 0], 0], cs[[0, 0], 1], cs[[1, 0], 0] and cs[[1, 0], 1] are assumed to be set to 1:

Clause Reduction By Redundancy Removal

1. If there are two selection rows in the same clause sub-matrix, where one selection row is a superset of of the other selection row, the superset can be removed (obfuscation).
2. From 1. follows: If two selection rows in the same clause sub-matrix present the same conflicts, one of them can be deleted.

Proof:

Given selection s[i,j] and selection s[i, h], a common conflicting selection q, and a conflicting selection r which is unique to selection s[i, h]:

selection s[i,j] -> ¬q
selection s[i, h] -> ¬q ∧ ¬r

p = selection s[i,j] ∨ selection s[i, h]

it follows, that making any of the selections will make selection q impossible or it will make both selections q and r impossible:

p -> ¬q ∨ (¬q ∧ ¬r)

Full induction based on the truth table:

p	q	r	¬r	¬q	¬q ∧ ¬r	p -> ¬q ∧ ¬r	p -> ¬q	p -> ¬q ∨ (¬q ∧ ¬r)
0	0	0	1	1	1	1	1	1
0	0	1	0	1	0	1	1	1
0	1	0	1	0	0	1	1	1
0	1	1	0	0	0	1	1	1
1	0	0	1	1	1	1	1	1
1	0	1	0	1	0	0	1	1
1	1	0	1	0	0	0	0	0
1	1	1	0	0	0	0	0	0

shows that there is no difference in the result if the term (¬q ∧ ¬r) is dropped. Therefore, it is sufficient to consider selection s[i,j] only.

Note: if only the core part of the selection rows is considered, the total number of solutions will be incorrect, if the variable requirements differ. However, satisfiability cannot be affected, since the core problem is sufficient to determine satisfiability. The variable part is entirely optional.

Note: Do not forget to run the requirements update algorithm after removing a selection row, especially if there is a differing variable part and only the core problem part was considered matching. Also run the requirements update algorithm before removing an entire clause.

Example:

After first round of redundancy elimination:

Note: If a selection row does not have any conflicts, this corresponds to the statement:

"If a variable appears only unnegated or only negated in a forumula, it can be set to T or F respectively and all clauses containing the literal can be removed from the formula."

After second round of redundancy elimination:

Final result:

Cross Clause Requirements

1. If there are two lines in different clause sub-matrixes, where one line is a subset of of the other line, the subset can be made a requirement of the superset, if they do not conflict with each other.
2. From 1. follows: If two lines in different clause sub-matrixes present the same conflicts, they can be made identical, if they do not conflict with each other.

Note: requirement requests must be issued sequentially. I.e., after a request, the requirements update algorithm must be run, before the next request can be issued.

The following example shows how a requirement request is added to the clause segment cs[[0, 2], 2] of selection row s[0, 2]:

That request is enough to let the requirements update algorithm detect the underlying conjunction:

Alternate Clause Representations

If several lines in different clause sub-matrixes present the same conflicts, but cannot be made identical, they represent a single selection of lines distributed across clause sub-matrixes. They can be placed into a clause sub-matrix of their own. An additional line is added to allow for none of the lines to be selected. (See Strange Thing for an alternate approach to that type of conflict).

The regular clause sub-matrixes are implictely based on such a construct. In this example the selection rows s[2, 0], s[3, 0], s[4, 0] are mutually exclusive:

The requirements update algorithm normalizes this as shown in the following satoku matrix. Note, that the alternative "none selected" is invalid:

Reverse Mapping of a Satoku Matrix

Based on the equivalence:

p → q = ¬p ∨ q

If a selection s[i,j] is made, it follows that another selection s[k, l] cannot be made.

E.g., encoding this satoku matrix:

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

renders (redundant clauses removed):

// S0 weak selection (allow one or more selections)
s[0,0] ∨ s[0,1] ∨ s[0,2]

// S0 intra-clause conflicts (require single selection)
¬s[0,0] ∨ ¬s[0,1]
¬s[0,0] ∨ ¬s[0,2]
¬s[0,1] ∨ ¬s[0,2]

// S1 weak selection (allow one or more selections)
s[1,0] ∨ s[1,1] ∨ s[1,2]

// S1 intra-clause conflicts (require single selection)
¬s[1,0] ∨ ¬s[1,1]
¬s[1,0] ∨ ¬s[1,2]
¬s[1,1] ∨ ¬s[1,2]

// S[0, 1] inter-clause conflicts
¬s[0,0] ∨ ¬s[1,0]
¬s[0,1] ∨ ¬s[1,1]
¬s[0,2] ∨ ¬s[1,2]

In order to produce a SAT problem with CNF clauses, the disjunctions (OR) are mapped to a set of disjunctive clause vectors.

Since the SAT problem to satoku matrix mapping function explicitely adds the intra-clause conflicts, they can be dropped in the reverse mapping:

[ 1 1 1 - - - ]
[ - - - 1 1 1 ]
[ 0 - - 0 - - ]
[ - 0 - - 0 - ]
[ - - 0 - - 0 ]
  s s s s s s
  0 0 0 1 1 1
  0 1 2 0 1 2

The clause vectors can then be translated to a SAT problem in conjunctive normal form[15]:

( s00 ∨  s01 ∨  s02) ∧
( s10 ∨  s11 ∨  s12) ∧
(¬s00 ∨ ¬s10 ) ∧
(¬s01 ∨ ¬s11 ) ∧
(¬s02 ∨ ¬s12 )

If you map this problem back to a satoku matrix (without mapping the variables!), this is what you get:

// |     || S ||  0|   0|| 1 1 1 | 1 1 1 || 1 1 | 1 1 | 1 1 |
// +-----++---++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |  0 H|   0||  2|   2|| 1 * * | 0 _ _ || _ _ | _ _ | 1 0 |
// |     |   1||  2|   2|| * 1 * | _ 0 _ || _ _ | 1 0 | _ _ |
// |     |   2||  2|   2|| * * 1 | _ _ 0 || 1 0 | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |  1 H|   3||  2|   2|| 0 _ _ | 1 * * || _ _ | _ _ | 0 1 |
// |     |   4||  2|   2|| _ 0 _ | * 1 * || _ _ | 0 1 | _ _ |
// |     |   5||  2|   2|| _ _ 0 | * * 1 || 0 1 | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |  2 H|   6||  1|   1|| _ _ _ | _ _ 0 || 1 * | _ _ | _ _ |
// |     |   7||  1|   1|| _ _ 0 | _ _ _ || * 1 | _ _ | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |  3 H|   8||  1|   1|| _ _ _ | _ 0 _ || _ _ | 1 * | _ _ |
// |     |   9||  1|   1|| _ 0 _ | _ _ _ || _ _ | * 1 | _ _ |
// +-----+----++---+----++-------+-------++-----+-----+-----+
// |  4 H|  10||  1|   1|| _ _ _ | 0 _ _ || _ _ | _ _ | 1 * |
// |     |  11||  1|   1|| 0 _ _ | _ _ _ || _ _ | _ _ | * 1 |
// +-----+----++---+----++-------+-------++-----+-----+-----+

Interesting, isn't it? Obviously each 2-literal clause vector maps nicely to a variable.

So the satoku matrix can also be mapped to a SAT problem in this manner:

with s[2,0] = a, s[2,1] = !a, s[3,0] = b, s[3,1] = !b, s[4,0] = c, s[4,1] = !c:

(a | b | c ) & (!a | !b | !c)

This shows unambiguously, that in the context of the satoku matrix it is completely irrelevant to make any distinction between variables and 2-SAT clauses. Their effects are identical.

1,2,k-SAT, soft, hard, weak and strong

Now, that we have come full circle mapping SAT problems to satoku matrixes and satoku matrixes back to (possibly different, but isomorphic) SAT problems, it is a good time to consolidate the theory.

In the context of satoku matrixes (and CNF formulas for that matter), there is nothing special about 1-SAT, 2-SAT, k-SAT with k >=3. The only difference is the effect of conflicts. But the conditions remain the same:

1. If a clause segment in a selection row has no possible selections (ones), the entire selection row becomes impossible and the selection row and corresponding column are filled with zeroes.
2. If all selection rows of a clause sub-matrix become impossible, the entire problem is unsatisfiable. (My crude version of the requirements update algorithm actually follows the propagation rules and fills the entire satoku matrix with zeroes for no deeper purpose at all.)

2-SAT Problems

With 2-SAT problems, there can be at most one conflict in any clause segment of a selection row. A conflict in a 2-SAT clause segment is immediately propagated throughout the entire satoku matrix by the requirements update algorithm. Soft ones only appear completely unrestricted, i.e., they cannot be combined with a conflict and still remain soft ones.

When a selection row becomes impossible, a 2-SAT clause sub-matrix degrades to a 1-SAT clause sub-matrix.

It follows, that the effects of a conflict in a 2-SAT problem are immediately known. There are no conflicts, that can be detected "later". Making Weak decisions based on soft ones remains possible. But since there is no need, it seems pretty clumsy. And the propagation of the consequences will immediately show, whether it was a good or bad decision.

The following example demonstrates that it is impossible to construct an indirect contradiction in a 2-SAT satoku matrix.

For an indirect contradiction, we need 2 selection rows s[0, 0], s[1, 0] that result in a contradiction (s[2, 0] cannot be selected) when both are actually selected:

Add two more selections s[3, 0], s[4, 0], which - when actually selected together - will require both s[0, 0] and s[1, 0]:

Selection row s[5, 0] requires both s[3, 0] and s[4, 0], which will indirectly lead to a contradiction:

The resulting satoku matrix looks perfectly fine, as long as the consequences of conflicts are ignored. But, running the requirements update algorithm detects the contradiction immediately:

This example also shows, that mapping a SAT problem to an inverted adjacency matrix and ignoring the clause constraints as negligible (since they are implicit) is a fallacy. It further shows, that mapping a 2-SAT problem to a DFS (depth-first search) graph is clumsy, since the representation of all possible solutions is unstructured and an additional search operation is needed to determine satisfiability.

Note

It may be interesting to check, whether mapping the DFS graph to an inverted adjacency matrix is equivalent to mapping the 2-SAT problem directly. But anyhow, the required DFS is definitely not equivalent to the requirements update algorithm.

Extracting Solutions from 2-SAT Satoku Matrixes

The set of unique solutions for a 2-SAT problem can be determined in the following manner.

The following 2-SAT problem:

( ¬p ∨ ¬r ) ∧
( ¬p ∨  s ) ∧
( ¬p ∨  t ) ∧
( ¬p ∨ ¬u ) ∧
(  p ∨  q ) ∧
(  q ∨ ¬r ) ∧
(  q ∨  s ) ∧
(  q ∨  t ) ∧
(  q ∨ ¬u ) ∧
(  r ∨  s ) ∧
(  r ∨  t ) ∧
(  r ∨ ¬u ) ∧
( ¬s ∨  t ) ∧
( ¬s ∨ ¬u ) ∧
(  t ∨  u )

maps to:

After removing redundant clauses, find a variable selection row with the maximum number of conflicts:

Use the (possibly partial) selection row as solution, disable the selection and continue with the next selection row, that has the maximum number of conflicts:

Repeat, until all solutions are extracted:

The set of solutions for this problem is:

[ 1 0 0 1 1 0 ]
[ 1 1 0 1 1 0 ]
[ 0 1 0 1 1 0 ]
[ 0 1 1 1 1 0 ]
[ 0 1 1 0 0 1 ]
[ 0 1 1 0 1 1 ]
[ 0 1 1 0 1 0 ]
  p q r s t u

This algorithm also works trivially for solution sets without conflicts:

The next partial solution:

The entire set of partial solutions is:

[ 1 _ _ _ ] //   2^3 =  8
[ 0 1 _ _ ] // + 2^2 =  4
[ 0 0 1 _ ] // + 2^1 =  2
[ 0 0 0 1 ] // +        1
[ 0 0 0 0 ] // +        1
  a b c d   // ----------
            //         16

Q       | * * 1 | .. | 0 - - |
        ..
R       | 0 - - | ..
        ..
S       | - 0 - | .. | - - 0 |
        ..
T       | - - 0 | .. | * 1 * |

=>
R&S     | 0 0 1 | .. | - - 0 | -> requires Q

=>
R&S&Q   | 0 0 1 | .. | 0 - 0 | -> requires T

=>
R&S&T&Q | 0 0 0 | ..

k^m, k = |C|, m = |P|,

⌈ k/2 ⌉ ^ m

Making Decisions

While it is possible to make variable based decisions in a satoku matrix, that type of algorithm is already thoroughly researched.

Therefore, this discussion only explores clause based strategies to reduce a k-SAT problem to one or more 2-SAT problems.

|:todo:| 2-SAT backtracking: find the right words ...

There are no provisions for backtracking in the scope of the satoku matrix. The following method can be employed to make it possible:

1. Make a copy of the satoku matrix to get 2 sub-problems SM0 and SM1.
2. In SM0 enforce the 2-SAT decision.
3. In SM1 enforce the complement of the 2-SAT decision (which does not necessarily result in a 2-SAT clause sub-matrix, depending on the size of the original clause sub-matrix).

.
                       Ci
                       /\
                    2 /  \ k-2
                     /    \
                   Ci,0  Ci,1
                          /\
                       2 /  \ k -4
                        /    \

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

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

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

Logical Reasoning

It is perfectly possible to use the satoku matrix without programmatically mapping an initial SAT formula.

Let's start with an empty satoku matrix. It is a sea of endless possibilities, since the selection rows in the clause sub-matrixes are not affected by the variables:

Since each selection row corresponds to the selection of a literal from a SAT problem clause, the first step is to map a clause, e.g., (¬a, ¬b, c) into the satoku matrix. This is real simple, since there are no other dependencies yet:

If you are using satoku-mode, the task becomes a lot simpler, because the requirements update algorithm can do most of the work. Since the algorithm looks for the required transition of a soft one to a hard one, a required selection is determined indirectly, by marking all other selections as impossible (this is called filling in a selection request). So let's map the clause (a, b, ¬c):

In satoku-mode press `r u' to run the requirements update algorithm. When it has finished, all impossible selections (selection conflicts) for each selection row are properly indicated:

Let's check what happens, when a request is prepared to make selection row s[0, 0] a superset row of selection row s[3, 1], by setting the matrix cell at (s[0, 0], s[3, 0]) to zero. This is logically equivalent to the statement (¬a ∧ ¬b):

Run requirements update algorithm (press `r u' in satoku-mode) to obtain the final result:

Conflict Maximization Revisited

Conflict maximization was not discoverd the way it is presented, instead it was found by reasoning in a satoku matrix. The figure below shows how (in a partial satoku matrix). (And the description shows, why a logical proof is much clearer than a proof using the satoku matrix).

The SAT clause mapping of (a, b, ¬c) in variable column range

R0 = (S0, S1, S2)

is copied into the variable column ranges

R1 = (S3, S4, S5),

R2 = (S6, S7, S8),

R3 = (S9, S10, S11),

R4 = (S12, S13, S14),

R5 = (S15, S16, S17),

R6 = (S18, S19, S20)

to show the progression of the reasoning. The ranges have been separated from each other by double rules for better visual distinction.

The initial argument concentrates on the region (Ri[0,0], Ri[1,3]), i ∈ (0, 1, .., 4). Row and column indices of ranges Ri[row, column] are relative to the range origin.

In Range R0, the regions (R0[0,2], R0[0,3]) and (R0[1,0], R0[1,1]) contain soft ones, i.e. possible selections.

Ranges R1, R2 show all possible required selections (hard ones) for the region (R0[0,2], R0[0,3]).

Ranges R3, R4 show all possible required selections (hard ones) for the region (R0[1,0], R0[1,1]).

Note, that the effective truth value assignments in ranges R2 and R3 are equivalent. It is therefore allowed to restrict the unrestricted selections of range R0 to the settings of either R1 or R4 without affecting the set of solutions of the corresponding SAT Problem.

By analogy, all possible assignments of range R0 have been prepared for restriction in range R5. Range R6 shows the actual restrictions after running the requirements update algorithm.

It is really important to verify conclusions from logical reasoning in a satoku matrix (as it is for any conclusions :)).

While this looks similar to conflict maximization:

it really is not, since the mirror property demands, that it be corrected to:

However, this is logically not equivalent to the original satoku matrix.

Conflict maximization can therefore only be applied within a clause conflict sub-matrix, not between clause conflict sub-matrixes.

Extending the original clauses shows what happens logically, when extending variable clauses:

(a ∨ ¬a) ∧ (b ∨ ¬b) ∧ (c ∨ ¬c) = (a ∨ (¬a ∧ ¬a)) ∧ (b ∨ (¬b ∧ ¬b)) ∧ (c ∨ (¬c ∧ ¬c))

(a ∨ (¬a ∧ ¬a)) = (a ∨ ¬a)

The conflicts of tautological variable clauses are already maximized. This agrees with the fact, that single selection is an operation which maximizes the direct conflicts between selections. It is not possible to add any more conflicts without making selections impossible. That is just another way to look at the clause identity sub-matrix.

Clause Construction

Here is a method to construct arbitrary disjunctive clauses from the given variable clause sub-matrixes which was inspired by the reasoning for conflict maximization:

Note the extra line at the bottom, which makes it a tautology. As proved above (proof for adding tautologies), tautologies can be added to a SAT problem without affecting the set of solutions.

The satoku matrix is completed with the requirements update algorithm:

Without any conflicts over the variables, this is not so interesting, but I found, that if the disjunctive requests over all variables are filled out and resolved subsequentially per column (not all at once), it provides a good intuitive estimate for the hardness of a SAT problem.

It will eventually lead to a situation, where no further columns can be added. Considering the number of variables after which that happens is a good indicator, whether the conflict situation is dense or flexible. E.g., XOR-SAT problems are very flexible and you can go very long without running into impossible selections.

Note

Doing this is equivalent to the brute force method of arbitrarily assigning truth values to variables.

|:todo:| prepare example

XOR Structure

Unobfuscated XOR-SAT problems encoded as 3-SAT can be easily detected and the necessary information for generating a system of linear equations can be directly extracted.

XOR encoded as 3-SAT:

(¬a ∨ ¬b ∨  c) ∧
(¬a ∨  b ∨ ¬c) ∧
( a ∨ ¬b ∨ ¬c) ∧
( a ∨  b ∨  c)

Observe redundant clause sub-matrixes S0, S1 and S2, S3.

Redundant clause sub-matrixes removed:

Clause sub-matrixes S0, S1 can be merged into a 4-SAT clause sub-matrix:

s[0, 0] ∧ s[1, 1], s[0, 0] ∧ s[1, 2], s[1, 0] ∧ s[0, 1], s[1, 0] ∧ s[0, 2]

Start by adding a 9-SAT clause sub-matrix, fill the first clause conflict sub-matrix with 3 requests per selection row (3 * 3 = 9), run requirements update algorithm:

Add a different row request for a row from the second clause sub-matrix for each row request in the first clause sub-matrix. Don't worry, if the request cell is already set to zero, just dont blank out the zero:

Remove all unselectable rows:

Run requirements update algorithm:

Remove original merge clause sub-matrixes, since they are no longer necessary:

The variable section of clause sub-matrix S0 shows the 4 possible solutions, and how an XOR can be extracted for a linear equation:

The clause section of the variables shows the typical XOR structure.

|:todo:| more images, explain

Bigger XOR-SAT problems necessarily show the same properties.

• initial redundant clause reduction m: -> m/2
• 3/3 -> 4 merge: m -> m/2

Which leaves a 4-SAT problem with 1/4 of the clauses of the original 3-SAT problem.

Since clause-based worst case for 3-SAT and 4-SAT is the same (2^m) this is a complexity reduction from 2^m to 2^(m/4)

Interleaved XOR reduces the problem by 2 clauses per decision, so effective complexity is 2^(m/8)

E.g. mod2-3cage-unsat-9-10, 232 3-SAT clauses, 87 variables:

raw n-complexity: 2^87

raw m-complexity: 2^232

analyzed n-complexity: 2^29

reduced m-complexity: 2^29

(which is exactly 87/3 and equivalent to observed n-complexity!)

observed n/m-complexity: 2^26 (contradiction)

DPLL-Like Resolution

Note: This algorithm is unresearched (it is based on my naive idea, how DPLL works). It is only listed for completeness.

If there is a conflict beteeen two clauses, it follows, that no matter which of the alternatives is selected, one of the remaining 4 selection rows must also be selected:

X1(p, l1, l2) ∧ X1(¬p, l3, l4) → X1(l1, l2, l3, l4)

Clause sub-matrix S10 is set up for the conflict in cell (s[0, 0], s[5, 0]). It consists of selection rows s[0, 1], s[0, 2], s[5, 1], s[5, 2]:

Even, if all conflicts are resolved (clause sub-matrixes S10, S11, S12), it does not help much. It is also possible that redundant selection rows appear in the resolution clause sub-matrix, see S13 and reordered copy S14:

When the common parts (S11) of the redundant selection rows (S12) are extracted,

the redundancies can be removed (S11):

The requirements update algorithm then reveals the single solution for the encoded conjunction:

Strange Thing

Here is an example, where conflict maximization gives no further clues. It was constructed after the structure of a Sat-2004 Competition instance handmade/set-85/sat04-838.cnf, (original name hirsch03/hgen8-n260-01-S1597732451.shuffled-as.sat03-885.cnf)

The odd thing about it is that conflicts appear to be transitive, i.e.:

cfl(a, b) ∧ cfl(b, c) → cfl(a, c)

This is different from the common behavior of single variable conflicts:

cfl(a, b) ∧ cfl(b, c) → b = ¬a ∧ c = ¬b → c = ¬¬a = a

However, it is not uncommon with nested conjunction/disjunction/conjunction clauses:

((a ∧ b) ∨ (c ∧ d)) ∧ ((a ∧ ¬b) ∨ (c ∧ ¬d)) ∧ ((¬a ∧ b) ∨ (c ∧ ¬d))
|:check:| bad example (all generated variables from a clause are mutually exclusive)

SAT Problem:

(  a0 ∨  a1 ∨  a2 ) ∧ (  b0 ∨  b1 ∨  b2 ) ∧
(  c0 ∨  c1 ∨  c2 ) ∧ (  d0 ∨  d1 ∨  d2 ) ∧
(  e0 ∨  e1 ∨  e2 ) ∧ (  f0 ∨  f1 ∨  f2 ) ∧
(  g0 ∨  g1 ∨  g2 ) ∧ (  h0 ∨  h1 ∨  h2 ) ∧
( ¬a0 ∨ ¬b0 ) ∧ ( ¬a0 ∨ ¬c0 ) ∧ ( ¬a1 ∨ ¬d0 ) ∧
( ¬a1 ∨ ¬e0 ) ∧ ( ¬a2 ∨ ¬g0 ) ∧ ( ¬a2 ∨ ¬h0 ) ∧
( ¬b0 ∨ ¬c0 ) ∧ ( ¬b1 ∨ ¬d1 ) ∧ ( ¬b1 ∨ ¬e1 ) ∧
( ¬b2 ∨ ¬c2 ) ∧ ( ¬b2 ∨ ¬e2 ) ∧ ( ¬b2 ∨ ¬f0 ) ∧
( ¬b2 ∨ ¬h2 ) ∧ ( ¬c1 ∨ ¬f2 ) ∧ ( ¬c1 ∨ ¬g2 ) ∧
( ¬c2 ∨ ¬e2 ) ∧ ( ¬c2 ∨ ¬f0 ) ∧ ( ¬c2 ∨ ¬h2 ) ∧
( ¬d0 ∨ ¬e0 ) ∧ ( ¬d1 ∨ ¬e1 ) ∧ ( ¬d2 ∨ ¬f1 ) ∧
( ¬d2 ∨ ¬g1 ) ∧ ( ¬d2 ∨ ¬h1 ) ∧ ( ¬e2 ∨ ¬f0 ) ∧
( ¬e2 ∨ ¬h2 ) ∧ ( ¬f0 ∨ ¬h2 ) ∧ ( ¬f1 ∨ ¬g1 ) ∧
( ¬f1 ∨ ¬h1 ) ∧ ( ¬f2 ∨ ¬g2 ) ∧ ( ¬g0 ∨ ¬h0 ) ∧
( ¬g1 ∨ ¬h1 )

The restrictions between clauses are fully mutually exclusive. E.g:

A = ( ¬a0 ∨ ¬b0 )
B = ( ¬a0 ∨ ¬c0 )
C = ( ¬b0 ∨ ¬c0 )

a0	b0	c0	A	B	C	A ∧ B ∧ C
0	0	0	1	1	1	1
0	0	1	1	1	1	1
0	1	0	1	1	1	1
0	1	1	1	1	0	0
1	0	0	1	1	1	1
1	0	1	1	0	1	0
1	1	0	0	1	1	0
1	1	1	0	0	0	0

The truth table shows, that this can be interpreted as:

X1(a0, b0, c0) ∨ (¬a0 ∧ ¬b0 ∧ ¬c0)

I.e., exactly one of a0, b0, c0 must be selected, or none of them.

The core problem of the plain conversion to a satoku matrix (selection variables not shown):

is excatly the same as that of the conversion to a satoku matrix with conflict maximization (variables not shown):

Let's try conflict resolution with a plain satoku matrix.

If 2 variables a, b are members of a SAT problem, it follows, that exactly one pair of the 4 possible variations of unnegated and negated variables must be selected:

a, b ∈ SAT → X1((a ^ b), (¬a ∧ b), (a ∧ ¬b), (¬a ∧ ¬b)) = T

It is therefore allowed to add a clause sub-matrix to the satoku matrix with all variations of a set of variables (only relevant variables shown):

The result, after the requirements update algorithm, is 3 clause sub-matrixes with 3 selection rows each:

The full conflict resolution presents as follows:

During the next step the new selection row identities are filled in:

The clause conflict sub-matrixes S[0, 8] and S[1, 8] show, that if clause sub-matrixes S0 and S1 are merged, a dense clause sub-matrix for S8 is produced, where all selection rows of S8 are fully bound (predicted size is 4 selection rows):

An even better merge choice are clause sub-matrixes S5 and S6, which have two dense conflict clause conflict sub-matrixes in common S(5, 13), S(6, 13) and S(5, 14), S(6, 14):

And the contradiction is detected by the requirements update algorithm:

Note: If that combination had been chosen first, it would have lead to the detection of the contradiction by itself.

With alternative reasoning emphasizing standard combinations for complexity reduction:

Removing merged clause sub-matrixes:

This is as far as you get:

Running the requirements update algorithm leads to a contradiction.

Undriven Clause Learning

The reverse mapping of a solution matrix offers another possibility to go about the problem from Strange Thing.

The 17 different 2-literal restriction clauses of the Strange Thing matrix can be viewed as a set of variables for the SAT core problem. In an unmaximized satoku matrix, the core problem clauses (k>=3) are fully defined by this new set of variables.

A SAT problem can be derived, which has the following structure (|:todo:| make this mathematical):

((l0,0,0 & l0,0,1 & ..) v (l0,1,0 & l0,1,1 & ..) v .. ) &
((l1,0,0 & l1,0,1 & ..) v (l1,1,0 & l1,1,1 & ..) v .. ) &
...

Each segment of a selection row spanning the clause conflict sub-matrixes of the variable section can be translated into a conjunctive clause vector. The resulting set of clause vectors represents a disjunctive set of clauses. The clause vector mapping of the above clause sub-matrixes looks like this:

// C0: DNF: (l06 & l13) v (l05 & l12) v (l01 & l11)
[ - - - - - - 0 - - - - - - 1 - - - ]
[ - - - - - 0 - - - - - - 1 - - - - ]
[ - 0 - - - - - - - - - 1 - - - - - ]
  l l l l l l l l l l l l l l l l l
  0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1
  0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6

// C1:
[ - - - - - - 1 - - - - - - 0 - - - ]
[ - - - - 0 - - - - - 1 - - - - - - ]
[ - - - 0 - - - - 0 - - - - - - 0 1 ]

// C2:
[ - - - - - - 0 - - - - - - 0 - - - ]
[ - - 0 - - - - - - 1 - - - - - - - ]
[ - - - 0 - - - - 0 - - - - - - 1 0 ]

// C3:
[ - - - - - 1 - - - - - - 0 - - - - ]
[ - - - - 1 - - - - - 0 - - - - - - ]
[ 0 - - - - - - 0 - - - - - - 1 - - ]

// C4:
[ - - - - - 0 - - - - - - 0 - - - - ]
[ - - - - 0 - - - - - 0 - - - - - - ]
[ - - - 0 - - - - 1 - - - - - - 0 0 ]

// C5:
[ - - - 1 - - - - 0 - - - - - - 0 0 ]
[ 0 - - - - - - 1 - - - - - - 0 - - ]
[ - - 1 - - - - - - 0 - - - - - - - ]

// C6:
[ - 1 - - - - - - - - - 0 - - - - - ]
[ 1 - - - - - - 0 - - - - - - 0 - - ]
[ - - 0 - - - - - - 0 - - - - - - - ]

// C7:
[ - 0 - - - - - - - - - 0 - - - - - ]
[ 0 - - - - - - 0 - - - - - - 0 - - ]
[ - - - 0 - - - - 0 - - - - - - 0 0 ]

The clause vector complement algorithm converts clause vectors from CNF to DNF and vice versa. For the conjunctive clause vectors of the first clause (DNF):

[ - - - - - - 0 - - - - - - 1 - - - ]
[ - - - - - 0 - - - - - - 1 - - - - ]
[ - 0 - - - - - - - - - 1 - - - - - ]

it delivers a set of disjunctive clause vectors (CNF):

[ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ ]
[ _ _ _ _ _ _ 0 _ _ _ _ 1 1 _ _ _ _ ]
[ _ _ _ _ _ 0 _ _ _ _ _ 1 _ 1 _ _ _ ]
[ _ _ _ _ _ 0 0 _ _ _ _ 1 _ _ _ _ _ ]
[ _ 0 _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ ]
[ _ 0 _ _ _ _ 0 _ _ _ _ _ 1 _ _ _ _ ]
[ _ 0 _ _ _ 0 _ _ _ _ _ _ _ 1 _ _ _ ]
[ _ 0 _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ ]

Repeating this procedure for all clauses produces this set of 128 CNF clause vectors (blank lines inserted to visualize clause boundaries):

[ _ _ _ _ _ _ _ _ _ _ _ 1 1 1 _ _ _ ]
[ _ _ _ _ _ _ 0 _ _ _ _ 1 1 _ _ _ _ ]
[ _ _ _ _ _ 0 _ _ _ _ _ 1 _ 1 _ _ _ ]
[ _ _ _ _ _ 0 0 _ _ _ _ 1 _ _ _ _ _ ]
[ _ 0 _ _ _ _ _ _ _ _ _ _ 1 1 _ _ _ ]
[ _ 0 _ _ _ _ 0 _ _ _ _ _ 1 _ _ _ _ ]
[ _ 0 _ _ _ 0 _ _ _ _ _ _ _ 1 _ _ _ ]
[ _ 0 _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ _ 1 _ _ 0 _ _ 1 ]
[ _ _ _ _ _ _ _ _ _ _ 1 _ _ 0 _ 0 _ ]
[ _ _ _ _ _ _ _ _ 0 _ 1 _ _ 0 _ _ _ ]
[ _ _ _ _ _ _ 1 _ _ _ 1 _ _ _ _ _ 1 ]
[ _ _ _ _ _ _ 1 _ _ _ 1 _ _ _ _ 0 _ ]
[ _ _ _ _ _ _ 1 _ 0 _ 1 _ _ _ _ _ _ ]
[ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ 1 ]
[ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 _ 0 _ ]
[ _ _ _ _ 0 _ _ _ 0 _ _ _ _ 0 _ _ _ ]
[ _ _ _ _ 0 _ 1 _ _ _ _ _ _ _ _ _ 1 ]
[ _ _ _ _ 0 _ 1 _ _ _ _ _ _ _ _ 0 _ ]
[ _ _ _ _ 0 _ 1 _ 0 _ _ _ _ _ _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ _ 1 _ _ 0 _ _ _ ]
[ _ _ _ 0 _ _ 1 _ _ _ 1 _ _ _ _ _ _ ]
[ _ _ _ 0 0 _ _ _ _ _ _ _ _ 0 _ _ _ ]
[ _ _ _ 0 0 _ 1 _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ 1 _ _ _ 0 _ _ 0 ]
[ _ _ _ _ _ _ _ _ _ 1 _ _ _ 0 _ 1 _ ]
[ _ _ _ _ _ _ _ _ 0 1 _ _ _ 0 _ _ _ ]
[ _ _ _ _ _ _ 0 _ _ 1 _ _ _ _ _ _ 0 ]
[ _ _ _ _ _ _ 0 _ _ 1 _ _ _ _ _ 1 _ ]
[ _ _ _ _ _ _ 0 _ 0 1 _ _ _ _ _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ 1 _ _ _ 0 _ _ _ ]
[ _ _ _ 0 _ _ 0 _ _ 1 _ _ _ _ _ _ _ ]
[ _ _ 0 _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 ]
[ _ _ 0 _ _ _ _ _ _ _ _ _ _ 0 _ 1 _ ]
[ _ _ 0 _ _ _ _ _ 0 _ _ _ _ 0 _ _ _ ]
[ _ _ 0 _ _ _ 0 _ _ _ _ _ _ _ _ _ 0 ]
[ _ _ 0 _ _ _ 0 _ _ _ _ _ _ _ _ 1 _ ]
[ _ _ 0 _ _ _ 0 _ 0 _ _ _ _ _ _ _ _ ]
[ _ _ 0 0 _ _ _ _ _ _ _ _ _ 0 _ _ _ ]
[ _ _ 0 0 _ _ 0 _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ _ 0 _ 0 _ 1 _ _ ]
[ _ _ _ _ _ _ _ 0 _ _ 0 _ 0 _ _ _ _ ]
[ _ _ _ _ _ 1 _ _ _ _ 0 _ _ _ 1 _ _ ]
[ _ _ _ _ _ 1 _ 0 _ _ 0 _ _ _ _ _ _ ]
[ _ _ _ _ 1 _ _ _ _ _ _ _ 0 _ 1 _ _ ]
[ _ _ _ _ 1 _ _ 0 _ _ _ _ 0 _ _ _ _ ]
[ _ _ _ _ 1 1 _ _ _ _ _ _ _ _ 1 _ _ ]
[ _ _ _ _ 1 1 _ 0 _ _ _ _ _ _ _ _ _ ]
[ 0 _ _ _ _ _ _ _ _ _ 0 _ 0 _ _ _ _ ]
[ 0 _ _ _ _ 1 _ _ _ _ 0 _ _ _ _ _ _ ]
[ 0 _ _ _ 1 _ _ _ _ _ _ _ 0 _ _ _ _ ]
[ 0 _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ _ 0 _ 0 _ _ _ 0 ]
[ _ _ _ _ _ _ _ _ _ _ 0 _ 0 _ _ 0 _ ]
[ _ _ _ _ _ _ _ _ 1 _ 0 _ 0 _ _ _ _ ]
[ _ _ _ _ _ 0 _ _ _ _ 0 _ _ _ _ _ 0 ]
[ _ _ _ _ _ 0 _ _ _ _ 0 _ _ _ _ 0 _ ]
[ _ _ _ _ _ 0 _ _ 1 _ 0 _ _ _ _ _ _ ]
[ _ _ _ _ 0 _ _ _ _ _ _ _ 0 _ _ _ 0 ]
[ _ _ _ _ 0 _ _ _ _ _ _ _ 0 _ _ 0 _ ]
[ _ _ _ _ 0 _ _ _ 1 _ _ _ 0 _ _ _ _ ]
[ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ 0 ]
[ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ 0 _ ]
[ _ _ _ _ 0 0 _ _ 1 _ _ _ _ _ _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ _ 0 _ 0 _ _ _ _ ]
[ _ _ _ 0 _ 0 _ _ _ _ 0 _ _ _ _ _ _ ]
[ _ _ _ 0 0 _ _ _ _ _ _ _ 0 _ _ _ _ ]
[ _ _ _ 0 0 0 _ _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ 0 _ 0 ]
[ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ 0 0 _ ]
[ _ _ _ _ _ _ _ _ 0 0 _ _ _ _ 0 _ _ ]
[ _ _ _ _ _ _ _ 1 _ 0 _ _ _ _ _ _ 0 ]
[ _ _ _ _ _ _ _ 1 _ 0 _ _ _ _ _ 0 _ ]
[ _ _ _ _ _ _ _ 1 0 0 _ _ _ _ _ _ _ ]
[ _ _ _ 1 _ _ _ _ _ 0 _ _ _ _ 0 _ _ ]
[ _ _ _ 1 _ _ _ 1 _ 0 _ _ _ _ _ _ _ ]
[ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ 0 _ 0 ]
[ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ 0 0 _ ]
[ _ _ 1 _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ ]
[ _ _ 1 _ _ _ _ 1 _ _ _ _ _ _ _ _ 0 ]
[ _ _ 1 _ _ _ _ 1 _ _ _ _ _ _ _ 0 _ ]
[ _ _ 1 _ _ _ _ 1 0 _ _ _ _ _ _ _ _ ]
[ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ 0 _ _ ]
[ _ _ 1 1 _ _ _ 1 _ _ _ _ _ _ _ _ _ ]
[ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ 0 ]
[ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ ]
[ 0 _ _ _ _ _ _ _ 0 0 _ _ _ _ _ _ _ ]
[ 0 _ _ 1 _ _ _ _ _ 0 _ _ _ _ _ _ _ ]
[ 0 _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ 0 ]
[ 0 _ 1 _ _ _ _ _ _ _ _ _ _ _ _ 0 _ ]
[ 0 _ 1 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ ]
[ 0 _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ 0 _ 0 _ _ 0 _ _ ]
[ _ _ _ _ _ _ _ 0 _ 0 _ 0 _ _ _ _ _ ]
[ _ _ 0 _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ ]
[ _ _ 0 _ _ _ _ 0 _ _ _ 0 _ _ _ _ _ ]
[ _ 1 _ _ _ _ _ _ _ 0 _ _ _ _ 0 _ _ ]
[ _ 1 _ _ _ _ _ 0 _ 0 _ _ _ _ _ _ _ ]
[ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ 0 _ _ ]
[ _ 1 0 _ _ _ _ 0 _ _ _ _ _ _ _ _ _ ]
[ 1 _ _ _ _ _ _ _ _ 0 _ 0 _ _ _ _ _ ]
[ 1 _ 0 _ _ _ _ _ _ _ _ 0 _ _ _ _ _ ]
[ 1 1 _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ ]
[ 1 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ]

[ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 _ 0 ]
[ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ 0 0 _ ]
[ _ _ _ _ _ _ _ _ 0 _ _ 0 _ _ 0 _ _ ]
[ _ _ _ _ _ _ _ 0 _ _ _ 0 _ _ _ _ 0 ]
[ _ _ _ _ _ _ _ 0 _ _ _ 0 _ _ _ 0 _ ]
[ _ _ _ _ _ _ _ 0 0 _ _ 0 _ _ _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ _ _ 0 _ _ 0 _ _ ]
[ _ _ _ 0 _ _ _ 0 _ _ _ 0 _ _ _ _ _ ]
[ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ 0 _ 0 ]
[ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ 0 0 _ ]
[ _ 0 _ _ _ _ _ _ 0 _ _ _ _ _ 0 _ _ ]
[ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ 0 ]
[ _ 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ 0 _ ]
[ _ 0 _ _ _ _ _ 0 0 _ _ _ _ _ _ _ _ ]
[ _ 0 _ 0 _ _ _ _ _ _ _ _ _ _ 0 _ _ ]
[ _ 0 _ 0 _ _ _ 0 _ _ _ _ _ _ _ _ _ ]
[ 0 _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ 0 ]
[ 0 _ _ _ _ _ _ _ _ _ _ 0 _ _ _ 0 _ ]
[ 0 _ _ _ _ _ _ _ 0 _ _ 0 _ _ _ _ _ ]
[ 0 _ _ 0 _ _ _ _ _ _ _ 0 _ _ _ _ _ ]
[ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 ]
[ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ ]
[ 0 0 _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ ]
[ 0 0 _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ ]

When this set of clause vectors is mapped to a satoku matrix with conflict maximization, the contradiction is detected immediately.

RT:

For a SAT problem P with core problem clauses C and 2-literal restrictions V the upper bound for the worst case running time of this algorithm is:

|P| * n^k, n = |V|, k = |C|

For k=3 it is < O(n^4). (|:check:| or whatever the correct definition is.)

3,4-SAT Splitting

The undriven clause learning algorithm is a strong argument for the reduction of clause sizes. Otherwise the algorithm would have some kind of exponential behavior in regard to the clause size. (|:check:| not sure how to calculate this?)

The arbitrary polynomial reduction is well known, so I will introduce another method called 3,4-SAT splitting here. It differs slightly from the standard method and is not yet fully researched.

// |    ||   S||  0|   0|| 1 1 1 1 1 1 1 1 | 1 1 1 1 1 1 1 1 |
// +----++----++---+----++-----------------+-----------------+
// +-----+----++---+----++-----------------+-----------------+
// |  0 H|   0||   |    || 1 * * * * * * * | 0 0 _ 0 0 _ _ 0 |
// |     |   1||   |    || * 1 * * * * * * | _ 0 0 _ 0 0 0 0 |
// |     |   2||   |    || * * 1 * * * * * | 0 _ 0 0 _ 0 0 _ |
// |     |   3||   |    || * * * 1 * * * * | 0 0 _ 0 0 _ _ 0 |
// |     |   4||   |    || * * * * 1 * * * | 0 0 0 _ 0 0 0 0 |
// |     |   5||   |    || * * * * * 1 * * | _ 0 _ 0 _ 0 0 _ |
// |     |   6||   |    || * * * * * * 1 * | 0 0 0 0 0 _ _ 0 |
// |     |   7||   |    || * * * * * * * 1 | 0 _ 0 _ 0 _ 0 _ |
// +-----+----++---+----++-----------------+-----------------+
// |  1 H|   8||   |    || 0 _ 0 0 0 _ 0 0 | 1 * * * * * * * |
// |     |   9||   |    || 0 0 _ 0 0 0 0 _ | * 1 * * * * * * |
// |     |  10||   |    || _ 0 0 _ 0 _ 0 0 | * * 1 * * * * * |
// |     |  11||   |    || 0 _ 0 0 _ 0 0 _ | * * * 1 * * * * |
// |     |  12||   |    || 0 0 _ 0 0 _ 0 0 | * * * * 1 * * * |
// |     |  13||   |    || _ 0 0 _ 0 0 _ _ | * * * * * 1 * * |
// |     |  14||   |    || _ 0 0 _ 0 0 _ 0 | * * * * * * 1 * |
// |     |  15||   |    || 0 0 _ 0 0 _ 0 _ | * * * * * * * 1 |
// +-----+----++---+----++-----------------+-----------------+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

// |    ||   S||  0|   0|| 1 1 1 1 1 1 1 1 | 1 1 1 1 1 1 1 1 || 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 || 1 1 1 1 | 1 1 1 1 | 1 1 1 1 | 1 1 1 1 ||
// +----++----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |  0 H|   0||   |    || 1 * * * * * * * | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   1||   |    || * 1 * * * * * * | _ 0 0 _ 0 0 0 0 || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   2||   |    || * * 1 * * * * * | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   3||   |    || * * * 1 * * * * | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   4||   |    || * * * * 1 * * * | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   5||   |    || * * * * * 1 * * | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   6||   |    || * * * * * * 1 * | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   7||   |    || * * * * * * * 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |  1 H|   8||   |    || 0 _ 0 0 0 _ 0 0 | 1 * * * * * * * || 0 1 | _ _ | 0 1 | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |   9||   |    || 0 0 _ 0 0 0 0 _ | * 1 * * * * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  10||   |    || _ 0 0 _ 0 _ 0 0 | * * 1 * * * * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  11||   |    || 0 _ 0 0 _ 0 0 _ | * * * 1 * * * * || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  12||   |    || 0 0 _ 0 0 _ 0 0 | * * * * 1 * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  13||   |    || _ 0 0 _ 0 0 _ _ | * * * * * 1 * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  14||   |    || _ 0 0 _ 0 0 _ 0 | * * * * * * 1 * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  15||   |    || 0 0 _ 0 0 _ 0 _ | * * * * * * * 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  16||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ 0 0 | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  17||   |    || 0 _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 0 0 _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  18||   |    || 0 1 0 0 0 0 0 0 | _ 0 0 _ 0 0 0 0 || 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  19||   |    || _ 0 _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  20||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ 0 0 | _ _ _ _ | _ _ _ _ ||
// |     |  21||   |    || _ _ 0 _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | 0 0 _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  22||   |    || 0 0 0 1 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  23||   |    || _ _ _ 0 _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  24||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ 0 0 | _ _ _ _ ||
// |     |  25||   |    || _ _ _ _ 0 _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | 0 0 _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  26||   |    || 0 0 0 0 0 1 0 0 | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  27||   |    || _ _ _ _ _ 0 _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  28||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ 0 0 ||
// |     |  29||   |    || _ _ _ _ _ _ 0 _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | 0 0 _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  30||   |    || 0 0 0 0 0 0 0 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  31||   |    || _ _ _ _ _ _ _ 0 | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  32||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ 0 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 1 * * * | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  33||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ 0 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * 1 * * | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  34||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || 0 _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * * 1 * | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  35||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || 0 _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * * * 1 | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  36||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ 0 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | 1 * * * | _ _ _ _ | _ _ _ _ ||
// |     |  37||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ 0 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | * 1 * * | _ _ _ _ | _ _ _ _ ||
// |     |  38||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | 0 _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | * * 1 * | _ _ _ _ | _ _ _ _ ||
// |     |  39||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | 0 _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | * * * 1 | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  40||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ 0 | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | 1 * * * | _ _ _ _ ||
// |     |  41||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ 0 | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | * 1 * * | _ _ _ _ ||
// |     |  42||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 _ | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | * * 1 * | _ _ _ _ ||
// |     |  43||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 _ | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | * * * 1 | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  44||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ 0 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | 1 * * * ||
// |     |  45||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ 0 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * 1 * * ||
// |     |  46||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * 1 * ||
// |     |  47||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 _ | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * * 1 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

// |    ||   S||  0|   0|| 1 1 1 1 1 1 1 1 | 1 1 1 1 1 1 1 1 || 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 || 1 1 1 1 | 1 1 1 1 | 1 1 1 1 | 1 1 1 1 ||
// +----++----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |  0 H|   0||   |    || 1 * * * * * * * | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ 0 0 | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |   1||   |    || * 1 * * * * * * | _ 0 0 _ 0 0 0 0 || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |   2||   |    || * * 1 * * * * * | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | _ _ 0 0 | 0 0 _ _ | 0 0 _ _ ||
// |     |   3||   |    || * * * 1 * * * * | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |   4||   |    || * * * * 1 * * * | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | _ _ 0 0 | 0 0 _ _ ||
// |     |   5||   |    || * * * * * 1 * * | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |   6||   |    || * * * * * * 1 * | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | _ _ 0 0 ||
// |     |   7||   |    || * * * * * * * 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |  1 H|   8||   |    || 0 _ 0 0 0 _ 0 0 | 1 * * * * * * * || 0 1 | _ _ | 0 1 | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |   9||   |    || 0 0 _ 0 0 0 0 _ | * 1 * * * * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | _ _ || 0 0 _ _ | _ _ _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  10||   |    || _ 0 0 _ 0 _ 0 0 | * * 1 * * * * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 || _ _ _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  11||   |    || 0 _ 0 0 _ 0 0 _ | * * * 1 * * * * || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 _ _ | 0 0 _ _ | _ _ _ _ | 0 0 _ _ ||
// |     |  12||   |    || 0 0 _ 0 0 _ 0 0 | * * * * 1 * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 0 0 _ _ | _ _ _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  13||   |    || _ 0 0 _ 0 0 _ _ | * * * * * 1 * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ || _ _ _ _ | 0 0 _ _ | 0 0 _ _ | _ _ _ _ ||
// |     |  14||   |    || _ 0 0 _ 0 0 _ 0 | * * * * * * 1 * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 || _ _ _ _ | 0 0 _ _ | 0 0 _ _ | _ _ _ _ ||
// |     |  15||   |    || 0 0 _ 0 0 _ 0 _ | * * * * * * * 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || 0 0 _ _ | _ _ _ _ | 0 0 _ _ | 0 0 _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  16||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ 0 0 | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  17||   |    || 0 _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 0 0 _ _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  18||   |    || 0 1 0 0 0 0 0 0 | _ 0 0 _ 0 0 0 0 || 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ 0 | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  19||   |    || _ 0 _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 0 _ 0 _ | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  20||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | _ _ 0 0 | 0 0 _ _ | 0 0 _ _ ||
// |     |  21||   |    || _ _ 0 _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | 0 0 _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  22||   |    || 0 0 0 1 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ 0 | 0 0 _ _ | 0 0 _ _ ||
// |     |  23||   |    || _ _ _ 0 _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | 0 _ 0 _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  24||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | _ _ 0 0 | 0 0 _ _ ||
// |     |  25||   |    || _ _ _ _ 0 _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | 0 0 _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  26||   |    || 0 0 0 0 0 1 0 0 | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ 0 | 0 0 _ _ ||
// |     |  27||   |    || _ _ _ _ _ 0 _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ || _ _ _ _ | _ _ _ _ | 0 _ 0 _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  28||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | _ _ 0 0 ||
// |     |  29||   |    || _ _ _ _ _ _ 0 _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | 0 0 _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  30||   |    || 0 0 0 0 0 0 0 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 0 0 _ 0 ||
// |     |  31||   |    || _ _ _ _ _ _ _ 0 | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 || _ _ _ _ | _ _ _ _ | _ _ _ _ | 0 _ 0 _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  32||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 1 * * * | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  33||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || * 1 * * | 0 0 _ _ | 0 0 _ _ | 0 0 _ _ ||
// |     |  34||   |    || 0 _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || 0 1 | _ 0 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * * 1 * | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// |     |  35||   |    || 0 _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || 0 1 | 0 _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * * * 1 | _ _ _ _ | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  36||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 1 * * * | 0 0 _ _ | 0 0 _ _ ||
// |     |  37||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | * 1 * * | 0 0 _ _ | 0 0 _ _ ||
// |     |  38||   |    || _ _ 0 _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | 0 1 | _ 0 | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | * * 1 * | _ _ _ _ | _ _ _ _ ||
// |     |  39||   |    || _ _ 0 _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | 0 1 | 0 _ | _ _ | _ _ | _ _ | _ _ || _ _ _ _ | * * * 1 | _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  40||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 0 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | 1 * * * | 0 0 _ _ ||
// |     |  41||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 0 _ _ | 0 0 _ _ | * 1 * * | 0 0 _ _ ||
// |     |  42||   |    || _ _ _ _ 0 _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | _ 0 | _ _ | _ _ || _ _ _ _ | _ _ _ _ | * * 1 * | _ _ _ _ ||
// |     |  43||   |    || _ _ _ _ 0 _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | 0 _ | _ _ | _ _ || _ _ _ _ | _ _ _ _ | * * * 1 | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |     |  44||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 0 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | 1 * * * ||
// |     |  45||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || 0 0 _ _ | 0 0 _ _ | 0 0 _ _ | * 1 * * ||
// |     |  46||   |    || _ _ _ _ _ _ 0 _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 1 | _ 0 || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * 1 * ||
// |     |  47||   |    || _ _ _ _ _ _ 0 _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 1 | 0 _ || _ _ _ _ | _ _ _ _ | _ _ _ _ | * * * 1 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++---------+---------+---------+---------++
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

|:todo:| Intermediate table too big.

// |    ||   S||  0|   0|| 1 1 1 1 1 1 1 1 | 1 1 1 1 1 1 1 1 || 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 || 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 | 1 1 || 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 1 1 | 1 1 1 1 ||
// +----++----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |  0 H|   0||   |    || 1 * * * * * * * | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 1 0 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 0 1 ||
// |     |   1||   |    || * 1 * * * * * * | _ 0 0 _ 0 0 0 0 || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 0 | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | 0 0 1 || 0 0 _ _ | 0 0 0 1 ||
// |     |   2||   |    || * * 1 * * * * * | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 1 0 0 | 0 0 1 | 0 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || _ _ 0 _ | 0 0 1 0 ||
// |     |   3||   |    || * * * 1 * * * * | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 1 0 ||
// |     |   4||   |    || * * * * 1 * * * | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | 0 0 1 | 1 0 0 | 0 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 1 0 0 ||
// |     |   5||   |    || * * * * * 1 * * | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 0 0 1 | 0 1 0 | 0 0 1 || _ 0 _ | _ 0 _ | _ 0 _ | 0 _ _ || _ _ _ _ | 0 1 0 0 ||
// |     |   6||   |    || * * * * * * 1 * | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | 0 0 1 | 0 0 1 | 1 0 0 || 0 0 1 | 0 0 1 | 0 _ _ | _ 0 _ || _ _ 0 0 | 1 0 0 0 ||
// |     |   7||   |    || * * * * * * * 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ || 0 0 1 | 0 0 1 | 0 0 1 | 0 1 0 || 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || _ _ _ _ | 1 0 0 0 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |  1 H|   8||   |    || 0 _ 0 0 0 _ 0 0 | 1 * * * * * * * || 0 1 | _ _ | 0 1 | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | 0 _ _ | 0 0 1 || 1 0 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | 0 _ 0 _ ||
// |     |   9||   |    || 0 0 _ 0 0 0 0 _ | * 1 * * * * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | _ _ || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 0 1 | 0 _ _ || 0 1 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | _ 0 _ 0 ||
// |     |  10||   |    || _ 0 0 _ 0 _ 0 0 | * * 1 * * * * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 _ _ | 0 0 1 || 0 0 1 | 1 0 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 _ _ _ ||
// |     |  11||   |    || 0 _ 0 0 _ 0 0 _ | * * * 1 * * * * || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | _ _ 0 _ ||
// |     |  12||   |    || 0 0 _ 0 0 _ 0 0 | * * * * 1 * * * || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | 0 0 1 || 0 0 1 | 0 0 1 | 1 0 0 | 0 0 1 || 0 1 0 0 | 0 _ _ 0 ||
// |     |  13||   |    || _ 0 0 _ 0 0 _ _ | * * * * * 1 * * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ _ _ || 0 0 1 | 0 0 1 | 0 1 0 | 0 0 1 || 0 1 0 0 | _ 0 _ _ ||
// |     |  14||   |    || _ 0 0 _ 0 0 _ 0 | * * * * * * 1 * || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ 0 _ || 0 0 1 | 0 0 1 | 0 0 1 | 1 0 0 || 1 0 0 0 | _ 0 _ _ ||
// |     |  15||   |    || 0 0 _ 0 0 _ 0 _ | * * * * * * * 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || 0 0 1 | _ 0 _ | 0 _ _ | 0 _ _ || 0 0 1 | 0 0 1 | 0 0 1 | 0 1 0 || 1 0 0 0 | _ _ _ 0 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  16||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 1 0 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 0 1 ||
// |     |  17||   |    || 0 _ _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 0 _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  18||   |    || 0 1 0 0 0 0 0 0 | _ 0 0 _ 0 0 0 0 || 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 0 | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | 0 0 1 || 0 0 _ _ | 0 0 0 1 ||
// |     |  19||   |    || _ 0 _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ 0 _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  20||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 1 0 0 | 0 0 1 | 0 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || _ _ 0 _ | 0 0 1 0 ||
// |     |  21||   |    || _ _ 0 _ _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  22||   |    || 0 0 0 1 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 1 0 ||
// |     |  23||   |    || _ _ _ 0 _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ 0 _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  24||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | 0 0 1 | 1 0 0 | 0 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 1 0 0 ||
// |     |  25||   |    || _ _ _ _ 0 _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | 0 _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  26||   |    || 0 0 0 0 0 1 0 0 | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 || _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 0 0 1 | 0 1 0 | 0 0 1 || _ 0 _ | _ 0 _ | _ 0 _ | 0 _ _ || _ _ _ _ | 0 1 0 0 ||
// |     |  27||   |    || _ _ _ _ _ 0 _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ 0 _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  28||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | 0 0 1 | 0 0 1 | 1 0 0 || 0 0 1 | 0 0 1 | 0 _ _ | _ 0 _ || _ _ 0 0 | 1 0 0 0 ||
// |     |  29||   |    || _ _ _ _ _ _ 0 _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | 0 _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  30||   |    || 0 0 0 0 0 0 0 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * || 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ || 0 0 1 | 0 0 1 | 0 0 1 | 0 1 0 || 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || _ _ _ _ | 1 0 0 0 ||
// |     |  31||   |    || _ _ _ _ _ _ _ 0 | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ 0 _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  64||   |    || 0 _ 0 0 0 _ 0 0 | 1 0 0 0 0 0 0 0 || 0 1 | _ _ | 0 1 | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | 0 _ _ | 0 0 1 || 1 0 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | 0 _ 0 _ ||
// |     |  65||   |    || _ _ _ _ _ _ _ _ | 0 _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || 0 _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  66||   |    || 0 0 _ 0 0 0 0 _ | 0 1 0 0 0 0 0 0 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | _ _ || 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 0 1 | 0 _ _ || 0 1 0 | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | _ 0 _ 0 ||
// |     |  67||   |    || _ _ _ _ _ _ _ _ | _ 0 _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ 0 _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  68||   |    || _ 0 0 _ 0 _ 0 0 | 0 0 1 0 0 0 0 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 _ _ | 0 0 1 || 0 0 1 | 1 0 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 _ _ _ ||
// |     |  69||   |    || _ _ _ _ _ _ _ _ | _ _ 0 _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | 0 _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  70||   |    || 0 _ 0 0 _ 0 0 _ | 0 0 0 1 0 0 0 0 || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | _ _ 0 _ ||
// |     |  71||   |    || _ _ _ _ 0 _ _ _ | _ _ _ 0 _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | 0 _ _ | _ _ _ || _ _ _ | _ 0 _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  72||   |    || 0 0 _ 0 0 _ 0 0 | 0 0 0 0 1 0 0 0 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | 0 0 1 || 0 0 1 | 0 0 1 | 1 0 0 | 0 0 1 || 0 1 0 0 | 0 _ _ 0 ||
// |     |  73||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ 0 _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | 0 _ _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  74||   |    || _ 0 0 _ 0 0 _ _ | 0 0 0 0 0 1 0 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ _ _ || 0 0 1 | 0 0 1 | 0 1 0 | 0 0 1 || 0 1 0 0 | _ 0 _ _ ||
// |     |  75||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ 0 _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ 0 _ | _ _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  76||   |    || _ 0 0 _ 0 0 _ 0 | 0 0 0 0 0 0 1 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ 0 _ || 0 0 1 | 0 0 1 | 0 0 1 | 1 0 0 || 1 0 0 0 | _ 0 _ _ ||
// |     |  77||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ 0 _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | 0 _ _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  78||   |    || 0 0 _ 0 0 _ 0 _ | 0 0 0 0 0 0 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 * || 0 0 1 | _ 0 _ | 0 _ _ | 0 _ _ || 0 0 1 | 0 0 1 | 0 0 1 | 0 1 0 || 1 0 0 0 | _ _ _ 0 ||
// |     |  79||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ _ 0 || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | * 1 || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ 0 _ || _ _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  96||   |    || 1 0 0 0 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 1 * * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 0 1 ||
// |     |  97||   |    || 0 1 0 0 0 0 0 0 | _ 0 0 _ 0 0 0 0 || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 || * 1 * | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | 0 0 1 || 0 0 _ _ | 0 0 0 1 ||
// |     |  98||   |    || 0 0 _ _ _ _ _ _ | _ _ _ _ _ _ _ _ || 0 1 | 0 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ 0 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  99||   |    || 0 0 1 0 0 0 0 0 | 0 _ 0 0 _ 0 0 _ || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 1 * * | 0 0 1 | 0 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || _ _ 0 _ | 0 0 1 0 ||
// |     | 100||   |    || 0 0 0 1 0 0 0 0 | 0 0 _ 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | * 1 * | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 1 0 ||
// |     | 101||   |    || _ _ 0 0 _ _ _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | 0 1 | 0 1 | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ 0 _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 102||   |    || 0 0 0 0 1 0 0 0 | 0 0 0 1 0 0 0 0 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | 0 0 1 | 1 * * | 0 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 1 0 0 ||
// |     | 103||   |    || 0 0 0 0 0 1 0 0 | _ 0 _ 0 _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 0 0 1 | * 1 * | 0 0 1 || _ 0 _ | _ 0 _ | _ 0 _ | 0 _ _ || _ _ _ _ | 0 1 0 0 ||
// |     | 104||   |    || _ _ _ _ 0 0 _ _ | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | 0 1 | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | * * 1 | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ 0 _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 105||   |    || 0 0 0 0 0 0 1 0 | 0 0 0 0 0 _ _ 0 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ | 0 1 || 0 0 1 | 0 0 1 | 0 0 1 | 1 * * || 0 0 1 | 0 0 1 | 0 _ _ | _ 0 _ || _ _ 0 0 | 1 0 0 0 ||
// |     | 106||   |    || 0 0 0 0 0 0 0 1 | 0 _ 0 _ 0 _ 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ || 0 0 1 | 0 0 1 | 0 0 1 | * 1 * || 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || _ _ _ _ | 1 0 0 0 ||
// |     | 107||   |    || _ _ _ _ _ _ 0 0 | _ _ _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 1 | 0 1 || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | * * 1 || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | 0 _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 108||   |    || 0 _ 0 0 0 _ 0 0 | 1 0 0 0 0 0 0 0 || 0 1 | _ _ | 0 1 | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | 0 _ _ | 0 0 1 || 1 * * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | 0 _ 0 _ ||
// |     | 109||   |    || 0 0 _ 0 0 0 0 _ | 0 1 0 0 0 0 0 0 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | _ _ || 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 0 1 | 0 _ _ || * 1 * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | _ 0 _ 0 ||
// |     | 110||   |    || _ _ _ _ _ _ _ _ | 0 0 _ _ _ _ _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || 0 1 | 0 1 | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ 0 | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 111||   |    || _ 0 0 _ 0 _ 0 0 | 0 0 1 0 0 0 0 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 _ _ | 0 0 1 || 0 0 1 | 1 * * | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 _ _ _ ||
// |     | 112||   |    || 0 _ 0 0 _ 0 0 _ | 0 0 0 1 0 0 0 0 || 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || 0 0 1 | * 1 * | 0 0 1 | 0 0 1 || 0 0 1 0 | _ _ 0 _ ||
// |     | 113||   |    || _ _ _ _ 0 _ _ _ | _ _ 0 0 _ _ _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ || _ _ | _ _ | 0 1 | 0 1 | _ _ | _ _ | _ _ | _ _ || _ _ _ | _ _ _ | 0 _ _ | _ _ _ || _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ 0 _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 114||   |    || 0 0 _ 0 0 _ 0 0 | 0 0 0 0 1 0 0 0 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 | 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | 0 0 1 || 0 0 1 | 0 0 1 | 1 * * | 0 0 1 || 0 1 0 0 | 0 _ _ 0 ||
// |     | 115||   |    || _ 0 0 _ 0 0 _ _ | 0 0 0 0 0 1 0 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ _ _ || 0 0 1 | 0 0 1 | * 1 * | 0 0 1 || 0 1 0 0 | _ 0 _ _ ||
// |     | 116||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ 0 0 _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | 0 1 | 0 1 | _ _ | _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | * * 1 | _ _ _ || _ 0 _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 117||   |    || _ 0 0 _ 0 0 _ 0 | 0 0 0 0 0 0 1 0 || _ _ | 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 | 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | _ 0 _ || 0 0 1 | 0 0 1 | 0 0 1 | 1 * * || 1 0 0 0 | _ 0 _ _ ||
// |     | 118||   |    || 0 0 _ 0 0 _ 0 _ | 0 0 0 0 0 0 0 1 || 0 1 | 0 1 | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 1 0 || 0 0 1 | _ 0 _ | 0 _ _ | 0 _ _ || 0 0 1 | 0 0 1 | 0 0 1 | * 1 * || 1 0 0 0 | _ _ _ 0 ||
// |     | 119||   |    || _ _ _ _ _ _ _ _ | _ _ _ _ _ _ 0 0 || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | _ _ || _ _ | _ _ | _ _ | _ _ | _ _ | _ _ | 0 1 | 0 1 || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | * * 1 || 0 _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 120||   |    || _ 0 _ _ 0 _ _ _ | 0 0 0 0 0 0 _ _ || _ _ | 0 1 | _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ || _ 0 _ | _ _ _ | 0 _ _ | _ _ _ || 0 0 1 | 0 0 1 | 0 0 1 | _ _ 0 || 1 * * * | _ _ _ _ ||
// |     | 121||   |    || _ 0 _ _ 0 _ _ _ | 0 0 0 0 _ _ 0 0 || _ _ | 0 1 | _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ || 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ | 0 1 | 0 1 || _ 0 _ | _ _ _ | 0 _ _ | _ _ _ || 0 0 1 | 0 0 1 | _ _ 0 | 0 0 1 || * 1 * * | _ _ _ _ ||
// |     | 122||   |    || _ _ 0 _ _ _ 0 _ | 0 0 _ _ 0 0 0 0 || _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ | 0 1 | _ _ || 0 1 | 0 1 | _ _ | _ _ | 0 1 | 0 1 | 0 1 | 0 1 || _ _ _ | 0 _ _ | _ _ _ | 0 _ _ || 0 0 1 | _ _ 0 | 0 0 1 | 0 0 1 || * * 1 * | _ _ _ _ ||
// |     | 123||   |    || 0 _ _ 0 0 _ 0 _ | _ _ 0 0 0 0 0 0 || 0 1 | _ _ | _ _ | 0 1 | 0 1 | _ _ | 0 1 | _ _ || _ _ | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || 0 _ _ | _ 0 _ | 0 _ _ | 0 _ _ || _ _ 0 | 0 0 1 | 0 0 1 | 0 0 1 || * * * 1 | _ _ _ _ ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 124||   |    || 0 0 0 0 0 0 _ _ | 0 _ 0 _ 0 _ _ _ || 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ || 0 1 | _ _ | 0 1 | _ _ | 0 1 | _ _ | _ _ | _ _ || 0 0 1 | 0 0 1 | 0 0 1 | _ _ 0 || 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ || _ _ _ _ | 1 * * * ||
// |     | 125||   |    || 0 0 0 0 _ _ 0 0 | _ 0 _ _ _ 0 0 _ || 0 1 | 0 1 | 0 1 | 0 1 | _ _ | _ _ | 0 1 | 0 1 || _ _ | 0 1 | _ _ | _ _ | _ _ | 0 1 | 0 1 | _ _ || 0 0 1 | 0 0 1 | _ _ 0 | 0 0 1 || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ _ | * 1 * * ||
// |     | 126||   |    || 0 0 _ _ 0 0 0 0 | 0 _ _ 0 _ _ _ _ || 0 1 | 0 1 | _ _ | _ _ | 0 1 | 0 1 | 0 1 | 0 1 || 0 1 | _ _ | _ _ | 0 1 | _ _ | _ _ | _ _ | _ _ || 0 0 1 | _ _ 0 | 0 0 1 | 0 0 1 || 0 _ _ | _ 0 _ | _ _ _ | _ _ _ || _ _ _ _ | * * 1 * ||
// |     | 127||   |    || _ _ 0 0 0 0 0 0 | _ 0 _ _ 0 _ _ 0 || _ _ | _ _ | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 | 0 1 || _ _ | 0 1 | _ _ | _ _ | 0 1 | _ _ | _ _ | 0 1 || _ _ 0 | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | _ _ _ | 0 _ _ | _ 0 _ || _ _ _ _ | * * * 1 ||
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-----------------+-----------------++-----+-----+-----+-----+-----+-----+-----+-----++-----+-----+-----+-----+-----+-----+-----+-----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

// |    ||   S||  0|   0|| 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 1 1 | 1 1 1 1 ||
// +----++----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  96||   |    || 1 * * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 0 1 ||
// |     |  97||   |    || * 1 * | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | 0 _ _ | 0 0 1 | 0 0 1 || 0 0 _ _ | 0 0 0 1 ||
// |     |  98||   |    || * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ _ 0 ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     |  99||   |    || 0 0 1 | 1 * * | 0 0 1 | 0 0 1 || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || _ _ 0 _ | 0 0 1 0 ||
// |     | 100||   |    || 0 0 1 | * 1 * | 0 0 1 | 0 0 1 || 0 0 1 | _ 0 _ | 0 _ _ | _ 0 _ || _ _ _ 0 | 0 0 1 0 ||
// |     | 101||   |    || _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ _ 0 _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 102||   |    || 0 0 1 | 0 0 1 | 1 * * | 0 0 1 || 0 0 1 | 0 1 0 | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 1 0 0 ||
// |     | 103||   |    || 0 0 1 | 0 0 1 | * 1 * | 0 0 1 || _ 0 _ | _ 0 _ | _ 0 _ | 0 _ _ || _ _ _ _ | 0 1 0 0 ||
// |     | 104||   |    || _ _ _ | _ _ _ | * * 1 | _ _ _ || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | _ 0 _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 105||   |    || 0 0 1 | 0 0 1 | 0 0 1 | 1 * * || 0 0 1 | 0 0 1 | 0 _ _ | _ 0 _ || _ _ 0 0 | 1 0 0 0 ||
// |     | 106||   |    || 0 0 1 | 0 0 1 | 0 0 1 | * 1 * || 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || _ _ _ _ | 1 0 0 0 ||
// |     | 107||   |    || _ _ _ | _ _ _ | _ _ _ | * * 1 || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ _ | 0 _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 108||   |    || 0 _ _ | 0 0 1 | 0 _ _ | 0 0 1 || 1 * * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | 0 _ 0 _ ||
// |     | 109||   |    || 0 0 1 | _ 0 _ | 0 0 1 | 0 _ _ || * 1 * | 0 0 1 | 0 0 1 | 0 0 1 || 0 0 0 1 | _ 0 _ 0 ||
// |     | 110||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ || * * 1 | _ _ _ | _ _ _ | _ _ _ || _ _ _ 0 | _ _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 111||   |    || _ 0 _ | 0 _ _ | 0 _ _ | 0 0 1 || 0 0 1 | 1 * * | 0 0 1 | 0 0 1 || 0 0 1 0 | 0 _ _ _ ||
// |     | 112||   |    || 0 _ _ | 0 0 1 | _ 0 _ | 0 _ _ || 0 0 1 | * 1 * | 0 0 1 | 0 0 1 || 0 0 1 0 | _ _ 0 _ ||
// |     | 113||   |    || _ _ _ | _ _ _ | 0 _ _ | _ _ _ || _ _ _ | * * 1 | _ _ _ | _ _ _ || _ _ 0 _ | _ _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 114||   |    || 0 0 1 | _ 0 _ | 0 _ _ | 0 0 1 || 0 0 1 | 0 0 1 | 1 * * | 0 0 1 || 0 1 0 0 | 0 _ _ 0 ||
// |     | 115||   |    || _ 0 _ | 0 _ _ | 0 0 1 | _ _ _ || 0 0 1 | 0 0 1 | * 1 * | 0 0 1 || 0 1 0 0 | _ 0 _ _ ||
// |     | 116||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | * * 1 | _ _ _ || _ 0 _ _ | _ _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 117||   |    || _ 0 _ | 0 _ _ | 0 0 1 | _ 0 _ || 0 0 1 | 0 0 1 | 0 0 1 | 1 * * || 1 0 0 0 | _ 0 _ _ ||
// |     | 118||   |    || 0 0 1 | _ 0 _ | 0 _ _ | 0 _ _ || 0 0 1 | 0 0 1 | 0 0 1 | * 1 * || 1 0 0 0 | _ _ _ 0 ||
// |     | 119||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ _ | _ _ _ | _ _ _ | * * 1 || 0 _ _ _ | _ _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 120||   |    || _ 0 _ | _ _ _ | 0 _ _ | _ _ _ || 0 0 1 | 0 0 1 | 0 0 1 | _ _ 0 || 1 * * * | _ _ _ _ ||
// |     | 121||   |    || _ 0 _ | _ _ _ | 0 _ _ | _ _ _ || 0 0 1 | 0 0 1 | _ _ 0 | 0 0 1 || * 1 * * | _ _ _ _ ||
// |     | 122||   |    || _ _ _ | 0 _ _ | _ _ _ | 0 _ _ || 0 0 1 | _ _ 0 | 0 0 1 | 0 0 1 || * * 1 * | _ _ _ _ ||
// |     | 123||   |    || 0 _ _ | _ 0 _ | 0 _ _ | 0 _ _ || _ _ 0 | 0 0 1 | 0 0 1 | 0 0 1 || * * * 1 | _ _ _ _ ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |     | 124||   |    || 0 0 1 | 0 0 1 | 0 0 1 | _ _ 0 || 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ || _ _ _ _ | 1 * * * ||
// |     | 125||   |    || 0 0 1 | 0 0 1 | _ _ 0 | 0 0 1 || _ 0 _ | _ _ _ | _ 0 _ | 0 _ _ || _ _ _ _ | * 1 * * ||
// |     | 126||   |    || 0 0 1 | _ _ 0 | 0 0 1 | 0 0 1 || 0 _ _ | _ 0 _ | _ _ _ | _ _ _ || _ _ _ _ | * * 1 * ||
// |     | 127||   |    || _ _ 0 | 0 0 1 | 0 0 1 | 0 0 1 || _ 0 _ | _ _ _ | 0 _ _ | _ 0 _ || _ _ _ _ | * * * 1 ||
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// +-----+----++---+----++-------+-------+-------+-------++-------+-------+-------+-------++---------+---------++
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

Informed Decisions

Analyzing the requirements of a possible selection shows what would happen, if a selection is made. This is very helpful for deducing some facts.

The example 3-variable conjunction from above has the following "what if" scenarios among others:

• Selecting s[8, 0] is guaranteed to generate a satoku matrix, which has at most 2 3-row clause sub-matrixes.
• Selecting s[8, 1] is guaranteed to generate a satoku matrix, which has at most 2 3-row clause sub-matrixes.
• Selecting s[8, 2] is guaranteed to generate a satoku matrix, which has at most 3 3-row clause sub-matrixes.
• Selecting s[7, 0] is guaranteed to generate a satoku matrix, which has at most 4 3-row clause sub-matrixes.
• Selecting s[7, 1] is guaranteed to generate a satoku matrix, which has at most 3 3-row clause sub-matrixes.

Since selecting s[8, 0] is equivalent to selecting s[7, 1] as they both represent the same conflict situation, it follows that selecting s[7, 1] will in fact only leave 2 instead of 3 clause sub-matrixes with 3 rows.

Selecting both s[7, 1] and s[8, 1] will leave at most 1 clause sub-matrix with 3 rows. This can be achieved by merging variables S7 and S8 (combining all rows of S7 with all rows of S8) and then selecting the row representing the combination s[7, 1] and s[8, 1].

Since we already know, that this satoku matrix is highly implosive and any decision -- weak or strong -- leads to the final single solution, the merge is done with an extra selection row, which leaves all possiblities open and therefore does not enforce the consequences of the merge[16]:

// |     || S ||  0|   0|| 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 | 1 1 | 1 1 | 1 1 1 1 1 |
// +-----++---++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  0 H|   0||  2|   5|| 1 * * | _ _ _ | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | _ _ _ _ _ |
// |     |   1||  2|   5|| * 1 * | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | _ _ _ _ _ |
// |     |   2||  2|   4|| * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  1 H|   3||  2|   5|| _ _ _ | 1 * * | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | _ _ _ _ _ |
// |     |   4||  2|   4|| _ 0 _ | * 1 * | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 0 | _ _ | _ _ _ _ _ |
// |     |   5||  2|   5|| _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | 0 1 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  2 H|   6||  2|   5|| _ _ _ | _ _ _ | 1 * * | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | _ _ _ _ _ |
// |     |   7||  2|   4|| _ 0 _ | _ _ _ | * 1 * | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 0 | _ _ | _ _ _ _ _ |
// |     |   8||  2|   4|| _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  3 H|   9||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ || 1 0 | _ _ | _ _ | _ _ _ _ _ |
// |     |  10||  2|   5|| _ _ _ | _ 0 _ | _ 0 _ | * 1 * | _ _ _ | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | _ _ _ _ _ |
// |     |  11||  2|   5|| _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | 0 1 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  4 H|  12||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | 1 * * | _ _ _ | _ _ _ || 1 0 | _ _ | _ _ | _ _ _ _ _ |
// |     |  13||  2|   5|| _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | * 1 * | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | _ _ _ _ _ |
// |     |  14||  2|   4|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  5 H|  15||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ || 1 0 | _ _ | _ _ | _ _ _ _ _ |
// |     |  16||  2|   4|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | * 1 * | _ _ _ || _ _ | 1 0 | _ _ | _ _ _ _ _ |
// |     |  17||  2|   5|| _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 || _ _ | _ _ | 0 1 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  6 H|  18||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * || 1 0 | _ _ | _ _ | _ _ _ _ _ |
// |     |  19||  2|   4|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | * 1 * || _ _ | 1 0 | _ _ | _ _ _ _ _ |
// |     |  20||  2|   4|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 || _ _ | _ _ | 1 0 | _ _ _ _ _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  7 H|  21||  1|   3|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 1 * | _ _ | _ _ | _ _ 0 0 _ | \hphantom{\neg} a
// |     |  22||  1|   4|| _ _ _ | _ _ _ | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || * 1 | _ _ | _ _ | 0 0 _ _ _ | \neg a
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  8 H|  23||  1|   3|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 * | _ _ | _ 0 _ 0 _ | \hphantom{\neg} b
// |     |  24||  1|   4|| _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ || _ _ | * 1 | _ _ | 0 _ 0 _ _ | \neg b
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |  9 H|  25||  1|   3|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 * | _ _ _ _ _ | \hphantom{\neg} c
// |     |  26||  1|   4|| _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | * 1 | _ _ _ _ _ | \neg c
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// | 10 H|  27||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ 0 | _ 0 | _ _ | 1 * * * * |
// |     |  28||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ 0 | 0 _ | _ _ | * 1 * * * |
// |     |  29||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 0 _ | _ 0 | _ _ | * * 1 * * |
// |     |  30||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 0 _ | 0 _ | _ _ | * * * 1 * |
// |     |  31||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | * * * * 1 |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

This technique shows, that the satoku matrix is a very user friendly data structure. It really tries very hard to acommodate to every whim and whisper of its customers.

Setting up all possible variables combinations generates this satoku matrix:

// |     || S ||  0|   0|| 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 | 1 1 1 || 1 1 | 1 1 | 1 1 | 1 0 0 0 1 | 1 0 0 0 1 | 1 0 0 0 1 |
// +-----++---++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  0 H|   0||  2|   5|| 1 * * | _ _ _ | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |   1||  2|   5|| * 1 * | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |   2||  2|   4|| * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  1 H|   3||  2|   5|| _ _ _ | 1 * * | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |   4||  2|   4|| _ 0 _ | * 1 * | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 0 | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |   5||  2|   5|| _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  2 H|   6||  2|   5|| _ _ _ | _ _ _ | 1 * * | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || 0 1 | _ _ | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |   7||  2|   4|| _ 0 _ | _ _ _ | * 1 * | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 0 | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |   8||  2|   4|| _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  3 H|   9||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | 1 * * | _ _ _ | _ _ _ | _ _ _ || 1 0 | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  10||  2|   5|| _ _ _ | _ 0 _ | _ 0 _ | * 1 * | _ _ _ | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |  11||  2|   5|| _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  4 H|  12||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | 1 * * | _ _ _ | _ _ _ || 1 0 | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  13||  2|   5|| _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | * 1 * | _ 0 _ | _ 0 _ || _ _ | 0 1 | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// |     |  14||  2|   4|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 | _ _ _ || _ _ | _ _ | 1 0 | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  5 H|  15||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | 1 * * | _ _ _ || 1 0 | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  16||  2|   4|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | * 1 * | _ _ _ || _ _ | 1 0 | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  17||  2|   5|| _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 | _ _ 0 || _ _ | _ _ | 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  6 H|  18||  2|   4|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ | 1 * * || 1 0 | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  19||  2|   4|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | * 1 * || _ _ | 1 0 | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  20||  2|   4|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | * * 1 || _ _ | _ _ | 1 0 | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  7 H|  21||  1|   3|| 0 _ _ | 0 _ _ | 0 _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || 1 * | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ | \hphantom{\neg} a
// |     |  22||  1|   4|| _ _ _ | _ _ _ | _ _ _ | 0 _ _ | 0 _ _ | 0 _ _ | 0 _ _ || * 1 | _ _ | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | \neg a
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  8 H|  23||  1|   3|| _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ || _ _ | 1 * | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ | \hphantom{\neg} b
// |     |  24||  1|   4|| _ _ _ | _ 0 _ | _ 0 _ | _ _ _ | _ _ _ | _ 0 _ | _ 0 _ || _ _ | * 1 | _ _ | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | \neg b
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |  9 H|  25||  1|   3|| _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ || _ _ | _ _ | 1 * | _ 0 0 0 _ | _ 0 0 0 _ | _ 0 0 0 _ | \hphantom{\neg} c
// |     |  26||  1|   4|| _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 | _ _ _ | _ _ 0 || _ _ | _ _ | * 1 | 0 0 0 0 1 | 0 0 0 0 1 | 0 0 0 0 1 | \neg c
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// | 10 H|  27||   |    || 0 0 1 | 0 1 0 | 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 | _ _ _ || 1 0 | 1 0 | 1 0 | 1 * * * * | _ 0 0 0 _ | _ 0 0 0 _ |
// |     |  28||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * 1 * * * | 0 0 0 0 0 | 0 0 0 0 0 |
// |     |  29||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * * 1 * * | 0 0 0 0 0 | 0 0 0 0 0 |
// |     |  30||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | * * * 1 * | 0 0 0 0 0 | 0 0 0 0 0 |
// |     |  31||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | * * * * 1 | _ 0 0 0 _ | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// | 11 H|  32||   |    || 0 0 1 | 0 1 0 | 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 | _ _ _ || 1 0 | 1 0 | 1 0 | _ 0 0 0 _ | 1 * * * * | _ 0 0 0 _ |
// |     |  33||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | * 1 * * * | 0 0 0 0 0 |
// |     |  34||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | * * 1 * * | 0 0 0 0 0 |
// |     |  35||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | * * * 1 * | 0 0 0 0 0 |
// |     |  36||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ 0 0 0 _ | * * * * 1 | _ 0 0 0 _ |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// | 12 H|  37||   |    || 0 0 1 | 0 1 0 | 0 _ _ | 1 0 0 | _ 0 _ | _ _ 0 | _ _ _ || 1 0 | 1 0 | 1 0 | _ 0 0 0 _ | _ 0 0 0 _ | 1 * * * * |
// |     |  38||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | 0 0 0 0 0 | * 1 * * * |
// |     |  39||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | 0 0 0 0 0 | * * 1 * * |
// |     |  40||   |    || 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 | 0 0 0 || 0 0 | 0 0 | 0 0 | 0 0 0 0 0 | 0 0 0 0 0 | * * * 1 * |
// |     |  41||   |    || _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ | _ _ _ || _ _ | _ _ | _ _ | _ 0 0 0 _ | _ 0 0 0 _ | * * * * 1 |
// +-----+----++---+----++-------+-------+-------+-------+-------+-------+-------++-----+-----+-----+-----------+-----------+-----------+
// |:info:| move point inside and press `C-u M-x satoku-mode RET'

As it turns out, neither s[7, 1] nor s[8, 1] can be selected at all. The only possible set of selections is { s[7, 0], s[8, 0], s[9, 0] }.

Advantages

The satoku matrix shows, that the distinction between variables and clauses of a SAT problem is artificial without any real advantage.

It is the strong opinion of the author, that the willy-nilly distinction leads to willy-nilly decisions and therefore is even detrimental. But ... your mileage may vary.

|:todo:| advantages, explain

Obfuscated XOR Structure

It is also possible to detect obfuscated XOR-SAT instances and deobfuscate them properly.

|:todo:| obfuscated XOR structure, explain

Per-Problem Worst Case Upper Bound

|:todo:| per-problem worst case upper bound, explain

Summary

This structural system offers a rich environment of operations based on the algebraically boring single selection operator.

So next time you think you know it all, remember that this impression comes from your delusions of grandeur.

Paradoxes

Lemma: The limited use of mathematical models in DOGgy style programming is due to the fact that mathematics treats logic universally (without a time component) and ultimately excludes paradoxes from it's scope. However, DOGgy style has both completely paradoxical axioms and a prominent time component (the program will be finished real soon).

A famous example for a paradox is the Liar paradox:

Epimenides, the Cretan, spoke in truth when he said that everything that Cretans say is false.

Self-referential statements are good candidates for paradoxes. E.g., Russell's paradox, "The set of all sets that are not members of themselves".

The mathematical resolution is basically to ignore this[17], e.g., by showing that a "set of all sets not containing themselves" cannot exist (see Russellsche Antinomie (German)):

Based on:
  y ∈ x ↔ y ∉ y, x, y are arbitrary sets

Substituting x for y, this renders a contradiction:

  x ∈ x ↔ x ∉ x,

which is used to show that:

  ¬∃ x: ∀ y: y ∈ x ↔ y ∉ y

• There is no set of all sets having themselves not as an element.
• There is no set of all sets.
• These are classes, which are not sets.

Good. ZFC set theory is saved. We get a nice theory with lots of mathematical applications.

So, who needs sets containing themselves anyway? Well, DOGgy style programmers do, and if it's only for fun. One of the first things you find about sets having themselves as element, is that you already constructed your first endless loop in form of an unterminated exponential recursion:

A    = { A, 1, 2 }
A'   = { { A', 1, 2 }, 1, 2 }
A''  = { { { { A'', 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }
A''' = { { { { { { { { A''', 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }, 1, 2 }
...

Well, this is just naive set programming :). Using references instead of expanded sets avoids this problem:

r = Ref(R)

A = { a, 1, 2 }

Done. No more recursion during construction, only when fully expanding such a thing. And of course, you should never do that without the necessary precautions.

Here is a Perl(1) example using DATA::Dumper, that can deal with arbitrary self-referential data structures perfectly well:

use Data::Dumper;

my $hashes = [ {}, {}, {} ];
my $last = undef;
foreach my $hash ( @{$hashes} ) {
    $hash->{'me'} = $hash;
    $hash->{'prev'} = $last;
    $last = $hash;
}
printf STDOUT ( "%s\n", Data::Dumper->Dump([$hashes], ['$hashes']) );

This program displays:

$hashes = [
            {
              'prev' => undef,
              'me' => $hashes->[0]
            },
            {
              'prev' => $hashes->[0],
              'me' => $hashes->[1]
            },
            {
              'prev' => $hashes->[1],
              'me' => $hashes->[2]
            }
          ];

Here is an example, which implements the contains-itself (CS)/does-not-contain-itself (NS) partition and a universal class:

• arbitrarily putting NS into CS, classifying NS as containing a reference to itself (despite all correct resolutions of Russell's paradox), however, NS does not actually contain itself,
• arbitrarily putting CS into NS, classifying CS as not containing a reference to itself,
• constructing the universal class from the union of CS and NS.

class Universe(dict):

    def __repr__(self):
        sets = [' '.join((k, repr(v))) for k, v in sorted(ditems(self))]
        return '\n'.join(sets)

    def __init__(self, *args, **kwargs):
        super(Universe, self).__init__(self, *args, **kwargs)
        self['CS'] = Set(['ns', 'v'])
        self['NS'] = Set(['cs'])

    def __getitem__(self, key):
        if key == 'V':
            V = self['CS'].union(self['NS'])
            return V
        return super(Universe, self).__getitem__(key)

    def iteritems(self):
        items = []
        for k in self['V']:
            name = k.upper()
            items.append((name, self[name]))
        return items
    items = iteritems

    def add(self, name, set_):
        if not name:
            return
        if name in ('CS', 'NS', 'V'):
            return
        if name in self:
                self[name] = self[name].union(set_)
        else:
            self[name] = set_
        ref = name.lower()
        if ref in set_:
            self['CS'].add(ref)
        else:
            self['NS'].add(ref)

    def parse(self, input_):
        for line in input_.splitlines():
            set_ = Set()
            name = set_.parse(line)
            V.add(name, set_)

class Set(set):

    def __repr__(self):
        return sformat('{{ {0} }}', ', '.join(sorted(self)))

    def parse(self, line):
        name = None
        self.clear()
        fields = line.strip().split(' ', 1)
        while True:
            if not fields:
                break
            name = fields.pop(0)
            if not fields:
                break
            set_def = fields.pop(0).replace('{', '').replace('}', '').replace(',', '').strip()
            self.update(Set(re.split('\\s+', set_def)))
            break
        return name

V = Universe()
V.parse(input_)
printe(V)

With the following input:

input_ = '''
A { a, b, c }
B { a, c }
C { d }
D { a, d }
'''

this output is produced:

A { a, b, c }
B { a, c }
C { d }
CS { a, d, ns, v }
D { a, d }
NS { b, c, cs }
V { a, b, c, cs, d, ns, v }

Feeding the output back in as input, produces a stable result.

Lemma: Mathematics is a two-edged sword. If you know the limitations of mathematical theories, it can help you avoid running into paradoxes like this and avoid the risk of endless loops and data corruption. But mathematics, like anybody else, does not like to talk about limitations so much. Your algorithm book probably does not mention these things, too. (They have a tendency to deal with nice mathematical stuff that works, not the gory fringe stuff that does not work).

Corollary: Your programming language knows nothing about mathematical theories. It gives you a data type called set, but it only faintly resembles a mathematical set. There are no provisions to protect you from the pitfalls, which have a tendency to show up only with customers.

Cybernetics is a nice approach to tackle paradoxes like the problem of future contingents.

A simple state machine (no triggers needed) for the "catalog of all catalags that do not list themselves" presents just another oscillator:

+-------+  remove c   +-------+
| c ∈ c | ----------> | c ∉ c |
|       | <---------- |       |
+-------+   add c     +-------+

So, depending on when you look, the catalog either lists itself or it does not. No contradiction necessary.

It's a little bit like Schrödinger's cat. (It's just a joke. I'm not serious!).

Here is the special flavor of delusions of grandeur regarding modeling:

All problems can be mapped to a rigid mathematical model.

I am on the safe side sticking to proven mathematics in a program.

Modal Logic

The modal fallacy.

See modal logic at Wikipedia.

Introduction to modal logic: Possible Worlds by Norman Swartz.

The basic unary (1-place) modal operators are usually written □ for Necessarily and ◇ for Possibly. In a classical modal logic, each can be expressed by the other with negation:

◇ P ↔ ~ □ ~ P

□ P ↔ ~ ◇ ~ P

Thus it is possible that it will rain today if and only if it is not necessary that it will not rain today; and it is necessary that it will rain today if and only if it is not possible that it will not rain today.

Sloppy Algorithms

Isn't it funny, that the economically most successful software is based on the (intentionally) sloppiest manifestation of algorithms, I have ever seen? :) (I'm talking about MS).

List of Mathematical Symbols

The list of mathematical symbols might be helpful to find interpretations of symbols.

Non-Mathematical Problems

Mathematicians seem to be so used to declare things negligible, that they are prone to forget that some things can simply not be neglected. Just because a theory cannot handle something, does not make it go away when you ignore it.

Since non-mathematical problems of sufficient complexity are heterogeneous, i.e., structured and unstructured sub-problems are mixed, there will never be a single good strategy to solve them.

Insisting on systematic and fully structured models, along with the common fallacy of ignoring that the map is not the territory, some highly philosophical and aggressive discussions about certain non-concepts can be had:

• Invalid use cases

  Last time I checked, a use case could very well have illusionary requirements, which still does not make it invalid. A use case can also be hard to model, or a model can be a bad fit for a use case. Still, no invalidation in sight. Price too high? Not invalid.

• False solutions

  A problem can have an arbitrary amount of solutions. If a program does not solve a problem, it does not become false, it is just not a solution to the problem. If a program solves a problem, but does not fulfill the requirements of an arbitrary model, it is still a solution. It does not magically become false. What is the frame of reference?

• Correct models

  The correctness of a model is independent from a problem. It's a mathematical thing. A model can be fully correct, but still be a bad fit to a problem. On the other hand, there are models, which are not mathematically correct (in all regards), but still be a good fit for a problem.

• Incorrect documentation

  The documentation is an abstract model of the program it describes. Since the map is not the territory, all documentation is necessarily somewhat incorrect. Like models, documentation is a good or bad fit.

• Necessary documentation

  All documentation is necessarily incomplete. When is a necessity fulfilled? Certainly, when the documentation becomes the program itself.

  Should the documentation be able to enlighten the reader? How about the daodejing, art of war, confucius, torah, bible, quran then?

Object Orientation (OO)

Let me state this clearly and firmly beforehand. I do like and want object oriented support in a programming language.

This section is meant to shine some light on the illusion that programming languages are somehow object oriented, and that there are programming languages which are not. OO is actually a matter of structure in the programmer's mind. It is not a feature of a programming language. Programming languages can have good or bad support for object oriented thought patterns. That's all.

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

struct Obj {
  long int  id;
  char     *name;
  long int  age;
};

#define OBJ_id_TYPE   long int
#define OBJ_id_OFS    0
#define OBJ_name_OFS  (OBJ_id_OFS + sizeof(OBJ_id_TYPE))
#define OBJ_name_TYPE char *
#define OBJ_age_OFS   (OBJ_name_OFS + sizeof(OBJ_name_TYPE))
#define OBJ_age_TYPE  long int
#define OBJ_SIZEOF    (OBJ_age_OFS + sizeof(OBJ_age_TYPE))

#define OBJ_DOT(obj, member) \
  (*(OBJ_ ## member ## _TYPE *)((char *)(obj) + OBJ_ ## member ## _OFS))

void hexdump(char *name, void *data, long int size) {
  int indx;
  printf("%s[%03ld]: ", name, size);
  for ( indx=0; indx<size; ++indx ) {
    printf("%02x", ((char *) data)[indx]);
  }
  printf("\n");
}

int main(int argc, char** argv) {

struct Obj obj;
obj.id = 55;
obj.name = "me";
obj.age = 53;

char oraw[OBJ_SIZEOF];
OBJ_DOT(oraw, id) = 55;
OBJ_DOT(oraw, name) = "me";
OBJ_DOT(oraw, age) = 53;

  {
    int equal_error = memcmp(&obj, &oraw, sizeof(struct Obj));
    printf("obj and oraw are%s equal\n", !equal_error ? "": " not");
    if (equal_error || 1 == 1) {
      hexdump("Obj", &obj, sizeof(struct Obj));
      hexdump("OBJ", oraw, OBJ_SIZEOF);
    }
    exit(equal_error);
  }
}

obj and oraw are equal
Obj[024]: 370000000000000005084000000000003500000000000000
OBJ[024]: 370000000000000005084000000000003500000000000000

Discipline

Lemma: Anything requiring discipline is subject to Murphy's Law.

Templates (Cut-and-Paste)

Lemma: Templates are good and necessary. Working without templates is unproductive.

A good template system does not require you to remember much and it does not require special formats.

Lemma: A template system should not force you to invent names. That is only a distraction from your current activity, and DOGgy style programmers will never choose an appropriate name at the first try.

Templates must be editable with your normal editor.

Placeholder are necessary, but filling them out should be optional wherever possible. Grep-able tags are good placeholders.

Tags serve several context dependent purposes:

• outlining (multi-level structure)
• bookmarks
• region markers
• reminders

Adhoc (On-the-fly)

Lemma: Adhoc programming is unavoidable, since avoiding it would require Discipline.

Version Dilemma (DLL Hell)

Libraries are basically a good thing. However, a combinatory explosion of effort can happen, if libraries are not available in different versions.

Although you may enjoy the sensation of a good explosion, as DOGgy style programmer, you probably dislike unnecessary effort more.

If a library becomes incompatible to previous versions, they require update efforts proportional to their use.

Lemma: Good DOGgy style programming makes sure, that libraries can always be included locally to a project, to avoid the necessity of update efforts. I.e., always carry them around in case you need them. But do not use them unless necessary!

This is counter-intuitive to a library's intended purpose of code re-use, but it ensures, that libraries and operating systems can be upgraded willy-nilly by administrators (who always schedule their upgrades at inconvenient times, and they never give you root privileges, see also Bastard Operator From Hell).

Installation Time

How long does it take you to set up your development environment on a fresh machine?

It must have your editor and templating system. So for me that is Emacs, my Emacs packages and Snippets. So it takes me 15-30 minutes.

How about you Eclipse guys? Does it even ever run, or do you need someone from IT-administration?

File-Local IDE Features

C-x C-e in Emacs allows for adhoc lisp code to be executed in any buffer.

Since adhoc lisp code can invoke functions, macros, shell-commands, compilation and actually everything else you can do in emacs, it is perfectly suited to provide for file-local IDE features.

Dynamic abbreviations vs. Intellisense

Here is a discussion of intellisense and its inherent problems: Why PHP and JavaScript IDE's Suck. So I will not go into that.

Computers are not intelligent. Computers are very well suited to store huge amounts of information accurately. But that has nothing to do with intelligence. An idiot savant can do that.

Programming languages are very simple and also not intelligent. Determining the basic context in a programming language is a very simple task. So there is not much intelligence necessary to implement intellisense.

However, determining the intented context of a programmers action is an impossible task. And not only in an algorithmic sense or due to run-time requirements.

Consider this example:

variable = MyClass()

variable.

For intellisense, typing the dot must mean, that a member of MyClass is accessed, right?

Wrong. I am intending to introduce a member, which has not been defined yet. And I do not wish to define it now (in Python or Javascript it is not even necessary), so I don't loose my train of thought. The compiler will tell me later, that I have not yet defined the member. And I will then fix it, or maybe not. It really depends on, whether I am in the right mood.

But intellisense insists on being right and pops up a list of known members, which is distracting and annoying, since I already know, that the accessed member cannot be in that list yet.

Dynamic abbreviations on the other hand are humble. They do not assume anything but the barest facts. You start to type a word, hit a key, and it tries to complete it. It applies some uppercasing/lowercasing as it sees fit (which is more often correct than incorrect). But that's it. However, it can even complete entire sentences skipping over punctuation as necessary.

It could be argued, that a list of known members is not entirely useless when defining a new member, since it shows, what names cannot be used anymore. But dynamic abbreviations can do that too. A simple grep can do that, if necessary.

The copyright notice of dabbrev.el states:

;; Copyright (C) 1985, 1986, 1992, 1994, 1996, 1997, 2000, 2001, 2002,
;;   2003, 2004, 2005, 2006, 2007, 2008, 2009, 2010, 2011, 2012
;;   Free Software Foundation, Inc.

So, why in almost 30 years, has this feature not been implemented in each and every editor known to mankind?

For dynamic abbreviations to work well, it is necessary for the editor to keep track of the usage timeline of buffers. Emacs does that. Everybody else does not. So it's basically a design flaw, when an editor does not implement dynamic abbreviations, or can only implement them inefficiently.

So, why is a flawed program calling a simple feature intellisense. For me it is neither intelligent, nor does it make any sense.

Here is a Hacker News excerpt from Y Combinator in reference to Why PHP and JavaScript IDE's Suck:

jrockway

Dynamic abbreviations ("dabbrev-expand" and "dabbrev-completion") solve the problem quite nicely 90% of the time. If you keep the documentation open in another buffer, then it works 99% of the time, as long as you have a clue on what you're doing.

People seem a little bit too concerned about getting a java-style 100% correct solution when a 90% solution is nearly as good.

baha_man

I love Emacs, but I think the lack of 'Intellisense' is one of the few good reasons to use an IDE over Emacs or Vim. Some people think Intellisense rots the brain, but I can't see anyone ever saying that about eldoc-mode.

jrockway

lisp-complete-symbol definitely does rob the brain. I've written plenty of braindead Lisp with its help :) Eldoc is not the same thing, though, since it just shows some basic documentation after you've remembered the name of the function. It's a nice "yeah, I knew that was the name" reminder. Finally, it's easy to "dive deeper" with Lisp, thanks to "describe-function" and friends. I would definitely not complain about having that for other languages. (Languages that don't have docstrings are really annoying me these days. Perl especially.)

Honestly, I use dabbrevs more often than lisp-complete-symbol when writing lisp. It usually gets me what I want with less typing. (There are a lot of lisp functions that start with the same prefix, but not as many that I've used in my editor session. So dabbrev-expand has less to look at, and hence it usually gives me what I want faster.)