Satoku
Tool for Structural Analysis of SAT Problems
| Author: | Wolfgang Scherer |
|---|
Contents
- Introduction
- Satoku - The Game
- Design Principle
- Independent Set Problem and Adjacency Matrix
- Satoku Matrix
- Satoku Matrix Properties
- Requirements Update Algorithm
- Other Operations
- Conflict Maximization
- Merging Clause Sub-Matrixes
- Conflict Comparison
- Clause Reduction By Redundancy Removal
- Cross Clause Requirements
- Alternate Clause Representations
- Reverse Mapping of a Satoku Matrix
- 1,2,k-SAT, soft, hard, weak and strong
- Making Decisions
- Logical Reasoning
- Undriven Clause Learning
- 3,4-SAT Splitting
- Informed Decisions
- Advantages
- Obfuscated XOR Structure
- Per-Problem Worst Case Upper Bound
- Summary
- Clause Vectors
- Clause Vector Complement
- Footnotes
- References
Introduction
In order to limit any expectations up front, let me say that this tool is not a proof of P vs. NP (I really do not wish to participate in that discussion). It is also not meant to be a lightning fast SAT solver, although SAT problems can be solved with it (some even faster than with a variable based decision algorithm).
It is primarily an educational tool to provide some hints as to why some problems are hard and some are easy. (It sure educated me and it finally became fun after all).
If you have some experience in SAT problems, you may wish to decide beforehand, whether there is anything new here, or whether it is just a re-iteration of well-known facts.
So, in order to help make that decision, I am providing an abstract, as if this article was meant for publication in a mathematical journal:
- An algorithmic data structure, the satoku matrix, is constructed based on the mapping of arbitrary x-SAT problems, x = (1, 2, 3, ..), to an independent set problem, with additional constraints.
- The satoku matrix is shown to be a dynamic representation of all possible solutions to a SAT problem that differs from the well-known truth table. Its space requirement is O(n^2) which is better than that of a truth table O(2^n).
- An algorithm is presented, which operates on the set of all possible solutions instead of just a single possible solution. The worst case running time of the balancing algorithm (requirements update algorithm) is shown to be O(P).
- The algorithm delivers a method to trivially solve 2-SAT problems. All possible solutions can be generated based on sound decisions without the need to perform a guessing search.
- A clause based decision algorithm is presented, which is shown to have an upper bound of ceil(k/2)^m. This eliminates the need to use variables to show exponential complexity.
- It is shown, that operating on the full set of possible solutions eliminates the need to distinguish between variables and clauses at all. Variables are shown to be a special case (size 2) of general disjunctive clauses of size k, k = (1, 2, 3, ..). Therefore, variable based decision algorithms are shown to be a special case of the satoku matrix.
Although the proofs only require very basic propositional logic, the fact that the satoku matrix is a true superset of variable based algorithms means, that the satoku matrix cannot be proved in terms of the existing results of research on variable based decison algorithms.
As I do not have enough time to start that venture, my research is presented in the current form instead of an official publication, in the hope that it will at least incite some interest in my son.
Since I first wrote this in 2013, I have nevertheless started it and it is available as Structural Logic.
The terminology was purposefully chosen to differ as much as possible from the terminology of existing variable based decision algorithms. I found this helpful to trick my own prejudice which lead me time and again astray by mistaking necessarily similar concepts as identical.
If you are a professional and have to be careful about wasting your time, you may still find amusement in the fact, that iff the satoku matrix is proved correct, variable based decision algorithms can be interpreted as forcing a necessarily satisfiable 2-SAT sub-problem into a 1-SAT problem in the hope that the resulting consequences in the k-SAT sub-problem, k >= 3, can somehow be detected more easily. The information that the k-SAT sub-problem provides from the very beginning is then gradually detected to enhance the decisions[1].
If you are a student and have more time at hand, feel free to prove any part of the satoku matrix as an exercise. If you can prove it correct, you will help advance knowledge in a very prestigious part of the field. Although you will not really be concerned about P vs. NP, it still generates lots of hype, if you do not point out the irrelevance of this topic too hard. It would be nice, if you gave me feedback either way.
Just a hint from my personal experience: It may be necessary to express the concepts in commonly accepted terminology to find somebody willing to listen, but it will make it hard to explain the subtle differences without explaining the entire concept. The key argument is, that working on the entire set of solutions to begin with is indeed quite different from working on (varying) single element subsets at a time.
If you are a skilled hacker, you are probably already used to not being understood by lesser minds. So you need not concern yourself with boring proofs of self-evident facts. You can jump right in and write highly optimized versions of the satoku algorithms (e.g., satoku-mode needs a complete rewrite -- as a matter of fact, everything I produced needs a rewrite). If you rather think that people should be deserving of knowledge and work for it, go ahead and write non-GUI tools that only a selected few can understand, have a look at my collection of cryptic adhoc command line tools (to be included soon) and create a satoku tookit.
If you are a hacker mastermind, help yourself to a conspiracy theory along the lines of "mathematicians (financed by the clan of your choice) conspiring to hide the true nature of boolean satisfiability problems to make encryption seem safe". I am willing to pose as a tragic hero who was tricked into believing that there was a substantial difference between 1,2,3-SAT, so that n-complexity (input = variables) would make any sense at all. The tragedy would be that this made me stare at the obvious for almost 10 years, not realizing that m-complexity (input = clauses) was the key to the whole problem. You can insistently repeat that ceil(k/2)^m trivially shows, that not only are 1-SAT problems trivial, but also that 2-SAT problems are trivial (1^m is very trivial indeed). Vehemently explain that the only way to hide this, is by pulling a hideous "Wizard of OZ" charade of "Do not look behind the curtain (of n-complexity)!"
If you do not find yourself in any of these categories, you can just enjoy a fun game and make a donation if you like it (just kidding :)).
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[2], pp. 92, a 3-SAT problem can be mapped to an independent set problem in polynomial time.
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:
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.
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[3]:
(¬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:
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.
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].
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.
Selection Logic
The logic of selections involves the boolean values 0, 1 and the logical functions AND and (implicitely) X1.
X1 stands for single selection (see DOGgy style programming, section Ternary Logic Functions).
The hard/soft property is determined contextually and has different semantics in regard to the required updates and the relationship between selection rows. However, for the purpose of logical operations both hard ones and soft ones have the boolean value 1.
Since there are no changes from zero to one in the scope of this algorithm, these do not have to be considered (design principle to avoid weak decisions). See section Making Decisions for backtracking provisions.
Mirror Property
Each matrix cell c[f,g] has a mirror cell c[g ,f], which must be kept synchronized. Cells on the matrix diagonal are their own mirror, which makes synchronization trivial since they are obviously always synchronized to themselves.
Soft/Hard Property, Superset Rows
If there is a selection row s[i,j], with a hard one in cell c[[i,j] [f,g]], it follows, that if the selection represented by r[f] is made then the selection represented by s[i,j] must also be made. This is necessary to preserve satisfiability.
Therefore, all values in the matrix cells c[[i,j], [x,y]] of selection row s[i,j] are replaced by the logical AND of the value in c[[i,j], [x,y]] and the value in c[[f,g], [x,y]] from selection row s[f,g]:
This effectively adds all conflicts (zeroes) from selection row s[f,g] to selection row s[i,j].
It is said, that selection row s[i,j] requires selection row s[f,g] (necessary selection). Therefore, s[i,j] is called a superset row of s[f,g].
RT: O(n)
If it so happens, that a clause segment cs[[i,j], f] of a selection row s[i,j] is filled with zeroes except for a single soft one at c[[i,j], [f,g]], the soft one is converted to a hard one and the conflicts of the required selection row s[f,g] are added to row s[i,j].
RT: O(n)
If new conflicts are added to a selection row, all superset rows must be updated accordingly (see Worst Case Running Time below) .
Unselectable Rows, Unsatisfiability
If it so happens, that any clause segment cs[[i,j], f] of a selection row s[i,j] is filled entirely with zeroes, it can no longer be selected at all, i.e., it becomes unselectable. Therefore the entire row s[i,j] is filled with zeroes. Due to the mirror cell requirements, column sc[i,j] is also filled with zeroes.
RT: O(n)
If all rows in a clause sub-matrix become unselectable, the corresponding logical problem becomes unsatisfiable.
RT: O(1)
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:
Worst Case Running Time
For a satoku matrix M, a transition 1 -> 0 triggers m requirement updates, m = number of selection rows in M.
The cost for marking the maximum number of requirement updates is m.
Each requirement update involves a maximum of m linear AND operations.
Each requirement update causes a transition 1 -> 0, which in turn causes m further requirement updates.
The maximum cost for marking and applying requirement updates is therefore m * m * m = m^3.
If a selection becomes impossible, m-1 selection rows are affected and therefore m-1 requirement updates are potentially detected.
This process will definitely stop, when all clause sub-matrixes degrade to 1-SAT clauses, making them all identical. The worst case running time is therefore O(P), P = m^x, x = (1, 2, ..).
Summary
The most expensive part of the program is the algorithm to keep the matrix cells up to date.
The significance of a soft one is, that it can be changed to zero without further adverse consequences, while a hard one cannot be changed to zero without rendering the row unselectable. Therefore, a soft one can also be called a possible selection, while a hard one is called a necessary or required selection.
To make it perfectly clear, here are the only possible state transitions of matrix cell values in the scope of this algorithm:
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 ∧ rinduction 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.
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.
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):
| [sm-single] | In satoku-mode it is not possible to delete a row, when there are only two rows left. This is a restriction of the clause detection algorithm, which is not very thoroughly designed. (The insight, that rows/columns can be removed came quite late). |
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
- 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).
- 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
- 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.
- 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[4]:
( 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:
- 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.
- 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.)
1-SAT Problems
For clauses of 1-SAT problems, that means, that case 1 and 2 are identical. Both happen, as soon as a single conflict is introduced. I.e. for a 1-SAT problem to be satisfiable, there must not be any concflicts. It follows, that all ones are hard ones and no weak decisions can be made.
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
3-SAT Problems
Only k-SAT, k>=3 eventually requires weak decisions, because conflicts from two different clauses can combine during a merge operation in such a manner, that a soft one must be converted to a hard one. Since the effects of the newly detected hard one only become known, when the merge actually happens, such k-SAT problems can become unsatisfiable "later".
When a selection row becomes impossible, a 3-SAT clause sub-matrix degrades to a 2-SAT clause sub-matrix.
Indirect Impossible Selections
An indirect impossible selection occurs, when the selection of two rows eventually requires selecting a third row, which renders the entire selection invalid.
Given the following situation:
Q | * * 1 | .. | 0 - - |
..
R | 0 - - | ..
..
S | - 0 - | .. | - - 0 |
..
T | - - 0 | .. | * 1 * |
when row R and row S are selected together, the selection of row Q is also required:
=> R&S | 0 0 1 | .. | - - 0 | -> requires Q
adding the conflicts from selection row Q leads to the required selection of row T:
=> R&S&Q | 0 0 1 | .. | 0 - 0 | -> requires T
adding the conflicts from selection row T makes the entire selection impossible:
=> R&S&T&Q | 0 0 0 | ..
It is evident, that such a conflict situation requires SAT clauses with a minimum of 3 literals.
Worst Case Upper Bounds
The fact, that 2-SAT problems are immediately solvable means, that k-SAT problems can be solved by making weak decisions that reduce the satoku matrix to a set of 2-SAT problems.
The standard complexity calculations are based on weak decisions over the number of variables n that appear in a SAT problem (1-SAT decisions). I will call this complexity n-complexity (NC) to distinguish it from the complexity calculations based on the number of clauses m, which I will call m-complexity (MC).
For a SAT problem P, with clauses C, it follows, that the upper bound for the worst case running time for clause based decisions is not
k^m, k = |C|, m = |P|,
but
⌈ k/2 ⌉ ^ m
which for 3-SAT and 4-SAT is 2^m.
While m-complexity for a 1-SAT and 2-SAT problems is trivially 1^m = 1, n-complexity for 1-SAT and 2-SAT problems is counter-intuitively still 2^n. This is factually not the case, and therefore a difference must be postulated for 1,2,3-SAT, when using n-complexity.
Summary
Since any "well-formed" x-SAT, x >= 1 eventually degrades to a mixed SAT problem, the distinction between 1,2,3-SAT is essentially meaningless.
The notable special feature of 2-SAT problems is, that they produce a satoku matrix, that is either unsatisfiable or it must have at least one solution, after the initial run of the requirements update algorithm. This follows from the fact, that there cannot be any indirect impossible selections in 2-SAT problems.
So for 2-SAT problems to make the true statement that the problem is satisfiable, it is not even necessary to assign any variables at all.
However, depending on the requirements for acceptable solutions, it may become necessary to arbitrarily reduce a satoku matrix to a 1-SAT problem, if all variables must be assigned.
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:
- Make a copy of the satoku matrix to get 2 sub-problems SM0 and SM1.
- In SM0 enforce the 2-SAT decision.
- 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
/ \
Similarities between MC and NC
Starting with the satoku matrix SM:
- Make a 2 copies of SM and name them SM0, SM1.
- Make selection s[0, 0] impossible in SM0.
- Make the complementary selections s[0, 1], s[0, 2] impossible in SM1.
SM:
// | || 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'
SM0:
// | || 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'
SM1:
// | || 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'
In this case, making the 2-SAT decision in clause sub-matrix S0 is equivalent to making the 1-SAT decision for variable a (S2).
The MC reduction requirements are fulfilled in both cases, however, not all variables are fully assigned yet. I.e., some arbitrary variable decisions have to be made to produce a full assignment of the variables.
|:todo:| counter examples ... but not the large ones.
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
is copied into the variable column ranges
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:
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'
Worst Case
|:todo:| mod2-3cage-unsat-9-10: Coincidentally, for an unsatisfiable k-SAT instance based on a bipartite XOR problem, m-complexity = n-complexity = n/3 = 29. I.e. clause based and variable based decisions become equivalent.
|:check:| I think that is the reason for XOR structured problems being so hard. Let's see, whether I can find the right words ...
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[5]:
// | || 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'
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] }.
Note
Clause sub-matrix S6 never degrades to a 2-row clause sub-matrix, but the problem is still solved, since there are no conflicts left. I.e., it may or may not be necessary to degrade a satoku matrix to the representation of a 2-SAT instance.
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.
Clause Vectors
(|:todo:| so all the old stuff must be included too :), but put it in an appendix!)
The clauses of a SAT problems in symbolic notation can be mapped to a set of clause vectors, where each position in the clause vector represents a specific variable. The literals of a problem clause are mapped according to the following table:
| value | description |
|---|---|
| 0 | variable appears negated |
| 1 | variable appears unnegated |
| - | variable does not appear at all |
Example for a SAT problem with variables V = (a, b, c, d):
SAT = (a | b | !c) & (a | !b | d) [ 1 1 0 - ] [ 1 0 - 1 ] a b c d
The function to be applied to the set of literals and the function applied to the set of clause vectors are arbitrary and defined per context.
- If the clause vector represents a disjunction (OR) of literals, it is called a disjunctive clause vector.
- If the clause vector represents a conjunction (AND) of literals, it is called a conjunctive clause vector.
If nothing else is defined, a set of clause vectors represents a set of CNF clauses. I.e., the function applied to the set of clause vectors is a boolean AND, the function applied to each set of clause vector literals is a boolean OR (disjunctive clause vector).
Clause Vector Complement
The clause vector complement algorithm generates the cross product over the sets of literals defined by the clauses including redundant literal elimination (minimal set of complementary clauses, |:todo:| see Bronstein somewhere under optimization).
RT:
Worst case running time for a set of clause vectors CV with the size of a clause vector n is (|:check:| this is very high. make that the product of the number of used variables in a clause):
n^m, m = |CV|
SAT problem P, number of clauses m, number of variables n:
n^m
When the number of used variables k in each clause is fixed, the complexity becomes:
k^m
Footnotes
| [1] | It's a little bit like poking a bear with a stick ;-). |
| [2] | David M. Mount, CMSC 451 Lecture Notes, Fall 2012 (local copy) with kind permission from the author, should the document no longer be availabe at the original location. |
| [3] | This violates the requirements of a well formed 3-SAT problem in conjunctive normal form. So, strictly speaking, we are no longer dealing with a 3-SAT problem. |
| [4] | OK, I could not resist. If you want a 3-SAT CNF, you can proceed further ... The 2-literal clause vectors are now extended to 3 values, by duplicating them and adding a new variable to each instance (once negated and once unnegated): [ 1 1 1 - - - - - - ] [ - - - 1 1 1 - - - ] [ 0 - - 0 - - 0 - - ] [ 0 - - 0 - - 1 - - ] [ - 0 - - 0 - - 0 - ] [ - 0 - - 0 - - 1 - ] [ - - 0 - - 0 - - 0 ] [ - - 0 - - 0 - - 1 ] s s s s s s c c c 0 0 0 1 1 1 0 1 2 0 1 2 0 1 2 The clause vectors can then be translated to a 3-SAT problem in conjunctive normal form: ( s00 ∨ s01 ∨ s02) ∧ ( s10 ∨ s11 ∨ s12) ∧ (¬s00 ∨ ¬s10 ∨ ¬c0 ) ∧ (¬s00 ∨ ¬s10 ∨ c0 ) ∧ (¬s01 ∨ ¬s11 ∨ ¬c1 ) ∧ (¬s01 ∨ ¬s11 ∨ c1 ) ∧ (¬s02 ∨ ¬s12 ∨ ¬c2 ) ∧ (¬s02 ∨ ¬s12 ∨ c2 ) |
| [5] | Isn't it beautiful, how avoiding decisions can provide tons of information ;-). |
References
| [PW] | Possible Worlds (internet), Possible Worlds |
| [ML] | modal logic |
| [someone] | Someone, F. Sure, Something, Somewhere Sometime |
Copyright
Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.