Rationale for the Satoku Matrix

Author: Wolfgang Scherer

Contents

The question is: Is it worth the effort to document the satoku matrix formally[1]?

The answer to that question is "yes", if:

1.1) At least one of the following conclusions is new.

1.2) The conclusions do not contradict any established mathematical or
logical principles.

If any of the conclusions is invalid or old news, I would be highly interested to know about it, because it makes my task easier.

If I use the incorrect terms to describe a principle, I would also be highly thankful to learn about it, because it also makes my task easier.

I marked assumptions that I make, which I am not 100% certain about.

What I know so far is that

Note

The class of regular XORSAT problems was only choosen for its symmetric properties. The analysis applies to all SAT problems equally.

All CNF Satisfiability Problems Can Be Made Worse

Observation: The running time of variable based decision algorithms varies significantly for 3-regular bipartite graphs depending on whether the problem is encoded as regular XORSAT problem or whether it is encoded as the corresponding independent set problem.

There is a difference in actual running times for the same problem between 32s, 227612s and indefinite (>777881s) (MiniSat).

Example: Feed three differently encoded versions of the same problem mod2-3cage-unsat-9-10.cnf, into a SAT-Solver and watch the effects on running time. (I used MiniSAT v1.14, CryptoMiniSat 2 v2.9.8 and lingeling/treengeling ats 57807c8f410a9e676816984a0ad0c410e485bcae)

Running times of SAT solver MiniSAT:

Variation Running Time Solved Comment
Case 1 32s yes which was expected
Case 2 22761s yes this makes the results strange at first glance
Case 3 777881s no which was expected

Running times of SAT solver CryptoMiniSat:

Variation Running Time Solved Comment
Case 1 0.85s yes which was expected, since it has XOR support
Case 2 73616s no this is strange, no solution after 20 hours, although MiniSAT only took 6 hours
Case 3 73430s no which was expected

The problem is based on a 3-regular bipartite graph, so the structure is well-known (regular XORSAT):

030-reduced-sat.v-000.png

Structural analysis of regular XORSAT

For further details see Structural Decomposition of Regular XORSAT.

Note

This example was chosen for fireworks effect. The results do not depend on the structure of the problem. They can be seen with arbitrary CNF-problems.

But They Can Also Be Made Better

All three versions for the experiment are invariant in the context of the satoku matrix. I.e., the hardness of the problem is identical, although the input size measured in total number of variables and 2-literal clauses varies significantly. However, the number of k-literal clauses, k ≥ 3 is constant. (Oops, case 2 has m/2 due to redundanc eliminiation. I will fix that later).

Case 1 is also isomorphic to case 3. After stage 1 of the satoku matrix algorithm, all three cases become isomorphic.

The original structure can be discovered efficiently and the XORSAT encoding can be restored.

Experiment

The dimacs files used are:

Analysis with the satoku matrix makes the following predictions for n-complexity (based on number of variables) and m-complexity (based on number of clauses) for the original problem:

n-complexity: 229
m-complexity: 229

Since 2-literal clauses can be ignored after construction of the satoku matrix, m-complexity is expected to be constant at 229 .

lingeling/treengeling are a class of their own.

The most interesting result is case 2, where MiniSat outruns CryptoMiniSat in time (but not in the number of decisions).

  1. Feed the original problem:

    87 variables
    232 clauses
    696 literals

    into the SAT-Solver:

    $ lingeling mod2-3cage-unsat-9-10.cnf
    c Lingeling SAT Solver
    c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
    s UNSATISFIABLE
    c 33531 decisions, 204827.0 decisions/sec
    c 0.2 seconds, 1.9 MB
    

    Very good.

 c Treengeling Cube and Conquer SAT Solver
 c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
 s UNSATISFIABLE
 c 0.03 wall clock time, 0.03 process time
 c 9417 decisions, 282623 decisions per second

Extremely good.
 $ MiniSat_v1.14_linux mod2-3cage-unsat-9-10.cnf
 restarts              : 26
 decisions             : 9885877        (308144 /sec)
 CPU time              : 32.082 s
 UNSATISFIABLE

The number of decisions for MiniSat v1.14 is between :math:`2^{23}` and
:math:`2^24`. This is consistent with the observation, that
unsatisfiability of a real XORSAT problem is ususally detected when
there are still about 12 clauses left (4-SAT). Since each decision
removes 2 clauses, this results in effective savings of 6
decisions. Hence :math:`2^{(29-6)} = 2^{23}`.
 $ cryptominisatLinux64 mod2-3cage-unsat-9-10.cnf
 c Finding non-binary XORs:     0.00 s (found:      32, avg size: 3.8)
 c restarts                 : 38
 c decisions                : 197651      (0.85      % random)
 c CPU time                 : 0.85        s
 s UNSATISFIABLE

CryptoMiniSat only needs between :math:`2^{17}` and :math:`2^{18}`
decisions (probably Gauss-Jordan).
 $ MiniSat_v2.2.0 mod2-3cage-unsat-9-10.cnf
 restarts              : 65535
 decisions             : 76108189       (0.00 % random) (585108 /sec)
 CPU time              : 130.075 s
 UNSATISFIABLE

MiniSat v2.2.0 (simp) needs between :math:`2^26` and :math:`2^27`
decisions.
  1. Apply the satoku matrix conflict bias to the problem, remove redundant clauses, convert it to a simple selection problem with conflict bias:

    696 variables
    6688 clauses
    13608 literals

    and to a simple selection problem with conflict bias and redundancy removal:

    348 variables
    1730 clauses
    3576 literals

    and feed it into the SAT-Solver:

    $ lingeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts.cnf
    c Lingeling SAT Solver
    c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
    c 8647016 decisions, 68950.9 decisions/sec
    c 125.4 seconds, 16.3 MB
    
    $ lingeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf
    c Lingeling SAT Solver
    c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
    c 9647858 decisions, 72686.7 decisions/sec
    c 132.7 seconds, 18.1 MB
    

    Number of decisions between 223 and 224 . So the XOR-structure is detected properly. Why the reduced problem needs more decisions is beyond my imagination (random stuff?).

 $ treengeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts.cnf
 c Treengeling Cube and Conquer SAT Solver
 c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
 s UNSATISFIABLE
 c 18130940 decisions, 207242 decisions per second

 $ treengeling mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf
 c Treengeling Cube and Conquer SAT Solver
 c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
 s UNSATISFIABLE
 c 20269340 decisions, 211620 decisions per second

Number of decisions between :math:`2^24` and :math:`2^26`. So the
XOR-structure is detected properly. (different number of decisions?)
 $ MiniSat_v1.14_linux mod2-3cage-unsat-9-10-vertec-cover-with-conflicts-red-elim.cnf
 restarts              : 37
 decisions             : 523453042      (22998 /sec)
 CPU time              : 22761.1 s
 UNSATISFIABLE

The number of decisions for MiniSat is almost :math:`2^29`. This is
consistent with the observation that the most suitable variables
for the encoding affect 4 clauses for one assignment and only a
single clause for the complementary assignment. It is therefore
harder to detect unsatisfiablity.
 $ cryptominisatLinux64 mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf
 *** INTERRUPTED ***
 c restarts                 : 415
 c decisions                : 90622941    (0.10      % random)
 c CPU time                 : 73616.17    s

CryptoMiniSat is a lot slower. I have no idea why.
  1. Convert the original problem to a simple selection problem without conflict bias:

    696 variables
    2320 clauses
    4872 literals

    and feed it to the SAT-Solver:

    $ lingeling mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf
    c Lingeling SAT Solver
    c Version ats 57807c8f410a9e676816984a0ad0c410e485bcae
    c
    c  seconds         irredundant          redundant clauses agility   height
    c          variables clauses conflicts large ternary binary    glue         MB
    c
    c S    0.0     696     2320         0       0      0     0   0  0.0   0.0    0
    c S    1.0     464     1392     27799    4009    304   117  34 18.5  37.4    2
    c P    2.0     464     1392     60204    5646    408   117  34 20.3  35.0    1
    c P    5.0     464     1392    140205   10112    588   131  33 21.7  33.3    1
    c S   10.0     464     1392    260130   18148    760   131  32 22.8  36.1    5
    c S   20.1     464     1392    446840   29573    902   131  36 24.6  35.8    8
    c S   30.0     464     1392    688412   17527    975   131  36 24.9  34.9    3
    c S   40.0     464     1392    880593   29760   1023   131  34 25.1  34.2    8
    c S   50.0     464     1392   1112193   24998   1073   131  35 25.1  33.6    6
    c S   60.0     464     1392   1301436   31551   1099   131  34 25.1  33.1    6
    c S  120.0     464     1392   2547965   10803   1194   131  35 24.9  31.7    2
    c S  180.0     464     1392   3824238   44801   1313   131  33 23.9  30.4   16
    c S  240.0     464     1392   4820001   44862   1389   131  35 22.8  29.9   12
    c S  300.1     464     1392   5498966   78208   1471   131  33 22.7  29.9   20
    c S  600.1     464     1392   8209890   77636   1568   131  30 22.6  29.7   31
    c S  900.0     464     1392  13119364   49052   1725   131  33 22.0  28.6   17
    c S 1800.1     464     1392  22958750   98750   1846   131  34 20.9  27.8   47
    c S 2700.0     464     1392  29859729  232033   1865   131  33 20.6  28.1   85
    c S 3600.1     464     1392  39400947   80448   1914   131  34 20.2  27.8   27
    c S 4500.1     464     1392  49381455   66009   1967   131  34 20.2  27.8   24
    c S 5400.1     464     1392  56661440  156566   1989   131  34 20.2  27.7   63
    c S 6300.3     464     1392  61936487  211346   2010   131  33 20.3  27.6   44
    c S 7200.1     464     1392  68721909   55905   2015   131  33 20.2  27.2   14
    c
    c  seconds         irredundant          redundant clauses agility   height
    c          variables clauses conflicts large ternary binary    glue         MB
    c
    c S 10800.1     464     1392  89996521  174065   2044   131  34 20.0  26.7   77
    c S 14400.2     464     1392 104510218  378905   2059   131  34 20.1  26.5   99
    c S 18000.3     464     1392 117971974  435974   2063   131  32 20.0  26.2  134
    c S 21600.0     464     1392 130310650  383997   2065   131  34 20.1  26.2  115
    c S 25200.1     464     1392 160551060  155962   2075   131  31 20.0  26.3   63
    c S 28800.0     464     1392 192551073   95808   2076   131  31 19.9  26.2   28
    c S 32400.1     464     1392 213821405  113555   2076   131  33 20.0  26.5   52
    c S 36000.1     464     1392 229422256  242874   2076   131  32 20.0  26.5   96
    **INTERRUPTED**
    
 $ MiniSat_v1.14_linux mod2-3cage-unsat-9-10-vertec-cover-without-conflicts.cnf
 *** INTERRUPTED ***
 restarts              : 43
 decisions             : 12838157330    (16504 /sec)
 CPU time              : 777881 s

The number of decisions for MiniSat is between :math:`2^33` and
:math:`2^34`, which is consistent with the observation that for
this encoding the most suitable variables only affect a single
clause for both alternatives of an assignment. The predicted
n-complexity in this case is :math:`2^58`.
 $ cryptominisatLinux64 mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf
 *** INTERRUPTED ***
 c restarts                 : 163482
 c decisions                : 211788006   (0.15      % random)
 c CPU time                 : 73430.12    s

I do not expect CryptoMiniSat to solve the problem
faster. Therefore I did not let it run 9 days.

Verify Original Input (Case 1)

If you do not want to take my word for it, you can simply download the original problem from the archive hjkn-mod2-benchmarks.tar.gz on the web site Matti Järvisalo - SAT Benchmarks.

Roll Your Own (Case 3)

The input for case 3) encodes the original as independent set problem. It can be generated in this manner:

  • Start with an empty mapped problem.

  • For each clause of the original problem:

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

    assign a new variable to each literal and add a clause to the mapped problem containing the unnegated variables as literals (vertex set of independent set problem, "select at least one literal from each clause"):

    (c0 ∨ c1 ∨ c2) ∧ (c3 ∨ c4 ∨ c5)
    
  • For each clause in the mapped problem add the necessary 2-SAT clauses to ensure, that only one literal can be selected (edges of independent set problem, inverted vertex cover problem):

    (¬c0 ∨ ¬c1)
    (¬c0 ∨ ¬c2)
    (¬c1 ∨ ¬c2)
    
    (¬c3 ∨ ¬c4)
    (¬c3 ∨ ¬c5)
    (¬c4 ∨ ¬c5)
    
  • For each literal in a clause of the original problem that conflicts with a literal from a different clause, add a 2-SAT clause, that excludes selection of the conflicting literals (edges of independent set problem, inverted vertex cover problem):

    (¬c1 ∨ ¬c4)
    (¬c2 ∨ ¬c5)
    

Principle of Case 2

The input for case 2) is a little bit more complex, and it's really better to just take my word for its correctness, unless you wish to dive into the satoku matrix right away.

The principle is:

  • Map each clause of the original problem:

    (a ∨  b ∨ ¬c),
    (a ∨ ¬b ∨  c)
    

    to a biased DNF (making the possible selections more specific but still equivalent, not only equisatisfiable):

    (a ∨ (¬a ∧  b) ∨ (¬a ∧ ¬b ∧ ¬c)),
    (a ∨ (¬a ∧ ¬b) ∨ (¬a ∧  b ∧  c))
    
  • Remove redundant clauses by following the logical consequences (I have no idea how to do that without the satoku matrix, so you can just keep them, it really does not matter).

  • Map the result to the vertex cover problem corresponding to the independent set problem as explained above. It should be clear how to determine, whether two conjunctions represent conflicting selections or not.

Exponential Attack

A selection problem can again be encoded as independent set problem, and therefore the number of variables increases even more. The actual hardness of the problem stays the same, but a decision algorithm does not know anything about it. It never realizes, that it solves the same problem over and over.

This is a simple way to make problems appear harder than they actually are.

The Structure of Regular XORSAT Problems Can Be Recovered Efficiently

This is a special case, where the satoku matrix can recover the XOR structure of the problem very efficiently from the independent set encoding. I.e., the original variable set can be discovered.

One insight I gained from the satoku matrix was: structure cannot be destroyed, just diluted beyond recognition. Logic is really a funny animal.

For Other Types of Problems, The Mileage Varies, But Is Generally Good

It is generally possible to recover structural information from problems encoded as independent set problems efficiently.

In fact, the maximal structural ambiguity of the independent set 2-literal conflict clauses (inverted vertex-cover problem) is necessary to recover the structure. The principle being: First dilute maximally, then distill in clever ways.

It is even possible to recover an independent set problem from a pure encoding as vertex cover problem (2-SAT). Although, in that case I have no clue how efficient (yet).

Except For Hirsch Type Multi-Variable XORS

These are interwoven multi-variable selectors. There is no conflict maximization possible. They can be flattened, but that does not really help.

Analyzing The Conflict Structure of SAT Problems Gives Strict Upper Bounds For Complexity

The hardness of a problem is strictly defined by m-complexity. The input size is based on number and size of clauses. The absolute worst case upper bound for m-complexity is ceil(k ⁄ 2)m . It is not km .

Analysis of conflict structure and simple transformations based on amortized distributive expansion (only expand, if it strictly reduces overall complexity) reveal the structure of problems and can be used to efficiently deduce suitable variable subsets for decision algorithms.

There Is No Difference Between Clauses And Variables

There is no substantial difference between a traditional selection problem (independent set problem) and a decision problem. In the context of the satoku matrix, a decision algorithm simply confines the possible selections to the variable clauses. A traditional selection problem confines the possible selections to the mapped CNF clauses.

Assumption: The definition "select at least one literal from a clause" seems to lead to a semantic confusion what a selection from a clause and what a decision over a set of variables are.

Making a selection from a clause does not mean that any of the selections in other clauses referencing the same variable are ever made.

The mapping of a propositional formula to an independent set problem from above (Roll Your Own (Case 3)) shows exactly, what "at least one" and "exactly one" stand for.

The correct definition is "select exactly one literal from a clause".

There Are No Atomic Variables In k-SAT CNF Clauses, k > 1

Atomic variables only appear in 1-SAT clauses. Since 1-SAT problems cannot have conflicts without becoming unsatisfiable, all variables are atomic. However, they are also fully determined. I.e., there is no room for any decisions to be made. All selections from the clauses are possible and required:

060-indirect-1SAT.r.v-000.png

1-SAT example

CNF Is An Abstraction

A CNF formula with clauses of length k, k > 1 is an abstraction or representant of a set of conjunctions of DNF formulas D, where |D| > 1 .

CNF:

(a ∨ b ∨ c)

Set of DNFs D (list is not complete!):

((a          ) ∨ (     b     ) ∨ (          c))

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

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

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

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

(I have a truth table somewhere, which proves the equivalence). |:todo:| (I know, that I did not catch them all). |:todo:|

Trivially, a 1-literal CNF clause is the representant of a single element set of DNFs.

CNF:

(a)

Set of DNFs D:

((a))

Remember that clauses of the form (p∨¬p) are not allowed in CNFs? Good, because it makes it easier to define the set of DNFs for variables being the special case of a 2-literal disjunction, where the set of DNFs for each literal is actually a single element. (This is really the only thing "special" about a variable).

Variable clause:

(p ∨ ¬p)

Set of DNFs D for a variable clause:

((p) ∨ (¬p))

It is really not so special, since the biased expansions of a variable would be:

((      p) ∨ ( ¬p ∧ ¬p))
((¬¬p ∧ p) ∨ (      ¬p))

which is trivially equivalent to:

((p) ∨ (¬p))

General SAT Problem

A general SAT Problem can now be defined as normal CNF SAT-problem with the optional addition of a 2-literal variable clause for each of the variables:

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

Optional means, that the variables can be removed arbitrarily without incfluence on the final set of solutions. It also means, that variables can be ignored for sub-algorithms that determine the solving state. (What can be ignored and removed is a whole new can of worms, but very managable and easily provable).

When mapping to a satoku matrix, clauses can be replaced by any representant from the set of DNFs. (It can be done as a pre-mapping step also).

The mapping to a satoku matrix handles variables specially, in that each alternative conjunction of a variable clause is extended across the entire formula (this is not strictly necessary, but it avoids superfluous redundancies):

(c0 ∨ c1 ∨ c2) ∧ (c3 ∨ c4 ∨ c5) ∧ (c6 ∨ c7 ∨ c8) ∧
((¬c3 ∧ ¬c6) ∨ (¬c0)) ∧
((¬c4 ∧ ¬c7) ∨ (¬c1)) ∧
((¬c5)       ∨ (¬c2 ∧ ¬c8))

Example satoku matrix with plain variable clauses:

100-full-variable-mapping.v-000.png

Satoku matrix with plain variable clauses

Example satoku matrix with conjunctive bias clauses:

100-full-variable-mapping.x.v-000.png

Satoku matrix with conjunctive literal clauses

Hopefully, this example shows, that variable clauses are indistinguishable from CNF clauses. They look like clauses, smell like clauses and squirm like clauses:

110-full-variable-mapping-permutation-000.png

Variable clauses are indistinguishable from CNF clauses

Further Generalization

The mapping to a satoku matrix can handle any type of conjunctions of DNFs. There is no need to confine them to CNFs and their representants.

Amortized Distributive Expansion

Amortized means, that distributive expansion is only performed, if it actually reduces problem complexity.

The consequences of mapping different representants for the clauses can be seen, when performing amortized distributive expansion.

Amortized distributive expansion for reduced complexity, plain variable clauses:

100-full-variable-mapping.v-001.png

Distributive expansion for reduced complexity, plain variable clauses

The clause sub-matrix S5 defines a set of reliable implicants, which is in turn the defining set for the prime implicants of this problem. In fact it is equivalent to the set of prime implicants in this case.

Amortized distributive expansion for reduced complexity, conjunctive literal clauses:

100-full-variable-mapping.x.v-001.png

Distributive expansion for reduced complexity, conjunctive literal clauses

The clause sub-matrix S5 defines a set of reliable implicants, which is in turn the defining set for the implicants of this problem (no longer for the prime implicants!). Their advantage is, that they are unique, which facilitates counting solutions.

Solving Strategies

If desired, a traditional decision algorithm can be implemented on top of the satoku matrix. As well as a traditional selection algorithm. Graph algorithms can also be run, although I have no idea (yet) what they actually do.

But why restrict yourself to a single possibility, if you can have it all?

The natural goal for the satoku matrix is to reduce the problem to a set of 2-SAT problems. A 2-SAT satoku matrix is necessarily free of terminal contradictions or terminates as unsatisfiable, after a single run of the requirements update algorithm (hence the m-complexity of k ⁄ 2⌉m instead of km ).

If a selection row is present, which reduces the k-SAT problem to a 2-SAT problem, the selection can simply be made to verify it and generate a set of reliable assignments.

If the encoding variables are suitable, it is possible to find a set of variables R , where every conjunction of those variables (r0r1∧...∧ri), ri ∈ R reduces the k-SAT problem to a 2-SAT problem. This results in an effective n-complexity of 2|R| . This is the reason for the dependency from encoding variables observed for decision algorithms.

|:todo:| move somewhere else?

For 2-SAT problems the clause bias can be chosen in such a manner, that the number of clauses becomes minimal. This generates reliable assignments of maximal length.

It really depends on the actual state of the matrix which strategy is best.

Here is a good random 3-SAT example, showing clearly that sometimes a simple deduction from the state of specific selection rows is better than any decision at all. (I'm just kidding! I will construct a better example when there is time. Right now it shows, that some more clauses can also be handled.)

043-CHECK-07-genAlea-40-171-LONG.pmaxc.x.v-001.png

043-CHECK-07-genAlea-40-171-LONG.pmaxc.x.v-001.png

Anyway, after matrix construction, the matrix delivers the following information without any decisions whatsoever:

There is one unconditionally required core assignment, i.e. it is the common subset of all implicants. These variables are determined and cannot be assigned otherwise:

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

There are 2 fully verifiable selections (they reduce the k-SAT problem to a 2-SAT/1-SAT problem). Their reliable assignments are:

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

2 of the reliable assignments are also implicants:

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

1 reliable assignment is not an implicant:

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

And this is what you get from a decision algorithm:

==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |     171      513 |      57       0        0     nan |  0.000 % |
==============================================================================
restarts              : 1
conflicts             : 29             (inf /sec)
decisions             : 45             (inf /sec)
propagations          : 397            (inf /sec)
conflict literals     : 106            (20.90 % deleted)
Memory used           : 1.66 MB
CPU time              : 0 s

SATISFIABLE

So it takes 45 dangerously exponential decisions to find out, that the problem is satisfiable.

And the other one:

c This is CryptoMiniSat 2.9.8
c restarts                 : 1
c conflicts                : 29          (inf       / sec)
c decisions                : 41          (0.00      % random)
c conflict literals        : 116         (31.36     % deleted)
s SATISFIABLE
v 1 2 -3 -4 5 6 -7 -8 -9 10 -11 -12 13 14 -15 -16 17 -18 -19 -20 -21 22 -23 -24 25 -26 27 -28 29 30 -31 32 -33 34 35 36 37 38 39 40 0

The solution fits the required core assignment perfectly:

[ 1 1 0 _ 1 _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ 0 _ _ 0 _ 0 _ _ _ _ 0 _ _ 1 _ _ 1 _ ] // core assignment

[ 1 1 0 0 1 1 0 0 0 1 0 0 1 1 0 0 1 0 0 0 0 1 0 0 1 0 1 0 1 1 0 1 0 1 1 1 1 1 1 1 ] // solution

Structural Decomposition of Regular XORSAT

Case 1 of Experiment

Regular XORSAT, 3-SAT, original problem (case 1 of experiment):

031-reduced-sat-3SAT.v-000.png

Regular XORSAT, 3-SAT, original problem

Case 2 of Experiment

Regular XORSAT, 3-SAT, satoku matrix stage 1, added conflicts (base problem for case 2 of experiment)

031-reduced-sat-3SAT.x.v-000.png

Regular XORSAT, 3-SAT, satoku matrix stage 1, added conflicts

Regular XORSAT, 3-SAT, satoku matrix stage 1, reencoded as independent set problem (case 2 of experiment):

034-reduced-sat-3SAT.x.v-001.mtx+intra.r.v-000.png

Regular XORSAT, 3-SAT, satoku matrix stage 1, reencoded as independent set problem

Regular XORSAT, 3-SAT, satoku matrix stage 1, reencoded as independent set problem, SAT solver perspective:

034-reduced-sat-3SAT.x.v-001.mtx+intra.u.v-000.png

Regular XORSAT, 3-SAT, satoku matrix stage 1, reencoded as independent set problem, SAT solver perspective

Case 3 of Experiment

Regular XORSAT, 3-SAT, reencoded as selection problem (case 3 of experiment):

035-reduced-sat-3SAT.v-000.mtx+intra.v-000.png

Regular XORSAT, 3-SAT, reencoded as selection problem

Full Logs of SAT-Solver Experiment

MiniSat_v1.14_linux

mod2-3cage-unsat-9-10.cnf:

$ MiniSat_v1.14_linux mod2-3cage-unsat-9-10.cnf
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |     232      696 |      77       0        0     nan |  0.000 % |
|       100 |     232      696 |      84     100     1823    18.2 |  0.013 % |
|       251 |     232      696 |      93     132     1925    14.6 |  0.013 % |
|       477 |     232      696 |     102      91     1132    12.4 |  0.013 % |
|       814 |     232      696 |     112     139     1844    13.3 |  0.013 % |
|      1320 |     232      696 |     124     116     1428    12.3 |  0.013 % |
|      2079 |     232      696 |     136      95     1165    12.3 |  0.013 % |
|      3218 |     232      696 |     150     149     2035    13.7 |  0.013 % |
|      4926 |     232      696 |     165     145     2098    14.5 |  0.013 % |
|      7488 |     232      696 |     181     120     1561    13.0 |  0.013 % |
|     11332 |     232      696 |     199     169     2534    15.0 |  0.013 % |
|     17099 |     232      696 |     219     155     1878    12.1 |  0.013 % |
|     25748 |     232      696 |     241     141     1708    12.1 |  0.013 % |
|     38723 |     232      696 |     265     261     3340    12.8 |  0.013 % |
|     58185 |     232      696 |     292     251     3162    12.6 |  0.013 % |
|     87377 |     232      696 |     321     305     4116    13.5 |  0.013 % |
|    131167 |     232      696 |     353     182     2295    12.6 |  0.013 % |
|    196852 |     232      696 |     389     236     2756    11.7 |  0.013 % |
|    295379 |     232      696 |     428     362     4849    13.4 |  0.013 % |
|    443168 |     232      696 |     470     305     3873    12.7 |  0.013 % |
|    664851 |     232      696 |     518     389     4560    11.7 |  0.013 % |
|    997376 |     232      696 |     569     499     6237    12.5 |  0.013 % |
|   1496165 |     232      696 |     626     314     3871    12.3 |  0.013 % |
|   2244348 |     232      696 |     689     589     8167    13.9 |  0.014 % |
|   3366623 |     233      696 |     758     665     8210    12.3 |  0.027 % |
|   5050035 |     229      684 |     834     482     5464    11.3 |  1.163 % |
==============================================================================
restarts              : 26
conflicts             : 6516168        (203110 /sec)
decisions             : 9885877        (308144 /sec)
propagations          : 92282116       (2876445 /sec)
conflict literals     : 87119249       (19.39 % deleted)
Memory used           : 2.05 MB
CPU time              : 32.082 s

UNSATISFIABLE

mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf:

$ MiniSat_v1.14_linux mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    1730     3576 |     576       0        0     nan |  0.000 % |
|       101 |    1730     3576 |     633     101     2881    28.5 |  0.001 % |
|       252 |    1731     3576 |     696     251     6098    24.3 |  0.001 % |
|       478 |    1734     3576 |     766     474    10979    23.2 |  0.001 % |
|       816 |    1738     3576 |     843     808    19184    23.7 |  0.001 % |
|      1324 |    1740     3576 |     927     777    20474    26.4 |  0.001 % |
|      2083 |    1751     3576 |    1020    1038    25913    25.0 |  0.002 % |
|      3223 |    1754     3576 |    1122    1026    22338    21.8 |  0.001 % |
|      4931 |    1774     3576 |    1234     816    21661    26.5 |  0.001 % |
|      7493 |    1784     3576 |    1358    1285    36315    28.3 |  0.001 % |
|     11337 |    1791     3576 |    1493    1460    42005    28.8 |  0.001 % |
|     17103 |    1800     3576 |    1643    1581    50885    32.2 |  0.001 % |
|     25753 |    1807     3576 |    1807    1542    42402    27.5 |  0.001 % |
|     38730 |    1830     3576 |    1988    1060    27313    25.8 |  0.001 % |
|     58192 |    1842     3576 |    2187    1161    29061    25.0 |  0.001 % |
|     87385 |    1861     3576 |    2406    1229    31548    25.7 |  0.001 % |
|    131174 |    1879     3576 |    2646    1724    45714    26.5 |  0.001 % |
|    196858 |    1887     3576 |    2911    2024    66899    33.1 |  0.001 % |
|    295386 |    1895     3576 |    3202    1750    58822    33.6 |  0.001 % |
|    443175 |    1916     3576 |    3522    3059   104660    34.2 |  0.001 % |
|    664859 |    1933     3576 |    3875    2945   102476    34.8 |  0.001 % |
|    997385 |    1945     3576 |    4262    2460    85460    34.7 |  0.001 % |
|   1496176 |    1949     3576 |    4688    2275    80916    35.6 |  0.001 % |
|   2244358 |    1953     3576 |    5157    2566    88599    34.5 |  0.001 % |
|   3366632 |    1954     3576 |    5673    3564   120184    33.7 |  0.001 % |
|   5050045 |    1954     3576 |    6240    3859   121915    31.6 |  0.001 % |
|   7575162 |    1960     3576 |    6864    4065   152471    37.5 |  0.001 % |
|  11362839 |    1960     3576 |    7551    6923   219702    31.7 |  0.007 % |
|  17044352 |    1960     3576 |    8306    6207   177760    28.6 |  0.007 % |
|  25566625 |    1960     3576 |    9137    5991   215173    35.9 |  0.001 % |
|  38350028 |    1960     3576 |   10050    5453   187002    34.3 |  0.001 % |
|  57525135 |    1960     3576 |   11055    9157   344012    37.6 |  0.001 % |
|  86287793 |    1960     3576 |   12161    8826   301639    34.2 |  0.001 % |
| 129431781 |    1960     3576 |   13377   11976   461638    38.5 |  0.007 % |
| 194147763 |    1960     3576 |   14715    9009   339113    37.6 |  0.001 % |
| 291221737 |    1960     3576 |   16187   13619   520440    38.2 |  0.001 % |
| 436832698 |    1961     3576 |   17805   11715   422829    36.1 |  0.012 % |
==============================================================================
restarts              : 37
conflicts             : 492799432      (21651 /sec)
decisions             : 523453042      (22998 /sec)
propagations          : 32650223888    (1434474 /sec)
conflict literals     : 19118584028    (15.50 % deleted)
Memory used           : 28.08 MB
CPU time              : 22761.1 s

UNSATISFIABLE

mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf:

$ MiniSat_v1.14_linux mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf
==================================[MINISAT]===================================
| Conflicts |     ORIGINAL     |              LEARNT              | Progress |
|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |
==============================================================================
|         0 |    2320     4872 |     773       0        0     nan |  0.000 % |
|       100 |    2320     4872 |     850     100     2696    27.0 |  0.000 % |
|       250 |    2320     4872 |     935     250     7730    30.9 |  0.000 % |
|       475 |    2320     4872 |    1028     475    15025    31.6 |  0.000 % |
|       813 |    2320     4872 |    1131     813    26086    32.1 |  0.000 % |
|      1322 |    2320     4872 |    1244    1322    40334    30.5 |  0.000 % |
|      2081 |    2320     4872 |    1369     783    18378    23.5 |  0.000 % |
|      3220 |    2320     4872 |    1506    1108    31069    28.0 |  0.000 % |
|      4929 |    2320     4872 |    1656    1230    32439    26.4 |  0.000 % |
|      7492 |    2320     4872 |    1822    1874    64202    34.3 |  0.000 % |
|     11336 |    2320     4872 |    2004    1689    54535    32.3 |  0.000 % |
|     17102 |    2320     4872 |    2205    2206    92348    41.9 |  0.000 % |
|     25752 |    2320     4872 |    2426    1703    65328    38.4 |  0.000 % |
|     38727 |    2320     4872 |    2668    1945    77118    39.6 |  0.000 % |
|     58188 |    2320     4872 |    2935    1915    71077    37.1 |  0.000 % |
|     87382 |    2320     4872 |    3229    2012    76019    37.8 |  0.000 % |
|    131173 |    2320     4872 |    3551    2072    75605    36.5 |  0.000 % |
|    196858 |    2320     4872 |    3907    2105    72181    34.3 |  0.000 % |
|    295385 |    2320     4872 |    4297    3485   127768    36.7 |  0.000 % |
|    443174 |    2320     4872 |    4727    3926   177139    45.1 |  0.000 % |
|    664860 |    2320     4872 |    5200    4542   209943    46.2 |  0.000 % |
|    997387 |    2320     4872 |    5720    3700   156595    42.3 |  0.000 % |
|   1496175 |    2320     4872 |    6292    4308   191208    44.4 |  0.000 % |
|   2244358 |    2320     4872 |    6921    3566   159429    44.7 |  0.000 % |
|   3366633 |    2320     4872 |    7613    4742   234022    49.4 |  0.000 % |
|   5050044 |    2320     4872 |    8375    7289   326987    44.9 |  0.000 % |
|   7575163 |    2320     4872 |    9212    7408   339034    45.8 |  0.000 % |
|  11362840 |    2320     4872 |   10134    5888   214951    36.5 |  0.000 % |
|  17044352 |    2320     4872 |   11147    6992   321011    45.9 |  0.000 % |
|  25566622 |    2320     4872 |   12262    7620   324590    42.6 |  0.000 % |
|  38350025 |    2320     4872 |   13488    9132   447983    49.1 |  0.000 % |
|  57525131 |    2320     4872 |   14837    8502   373241    43.9 |  0.000 % |
|  86287791 |    2320     4872 |   16320   12710   621498    48.9 |  0.000 % |
| 129431780 |    2320     4872 |   17953   14970   801196    53.5 |  0.000 % |
| 194147763 |    2320     4872 |   19748   10371   514816    49.6 |  0.000 % |
| 291221738 |    2320     4872 |   21723   13446   680208    50.6 |  0.000 % |
| 436832698 |    2320     4872 |   23895   12423   624677    50.3 |  0.000 % |
| 655249138 |    2320     4872 |   26285   13921   733198    52.7 |  0.000 % |
| 982873799 |    2320     4872 |   28913   16449   748971    45.5 |  0.000 % |
| 1474310791 |    2320     4872 |   31804   19079   886125    46.4 |  0.000 % |
| -2083501017 |    2320     4872 |   34985   23194  1083272    46.7 |  0.000 % |
| -977767784 |    2320     4872 |   38483   28154  1360430    48.3 |  0.000 % |
| 680832066 |    2320     4872 |   42332   17063   858971    50.3 |  0.000 % |
*** INTERRUPTED ***
restarts              : 43
conflicts             : 10835521721    (13930 /sec)
decisions             : 12838157330    (16504 /sec)
propagations          : 1071321181196   (1377230 /sec)
conflict literals     : 571262903478   (15.21 % deleted)
Memory used           : 147.38 MB
CPU time              : 777881 s
*** INTERRUPTED ***

cryptominisatLinux64

mod2-3cage-unsat-9-10.cnf:

$ cryptominisatLinux64 mod2-3cage-unsat-9-10.cnf
c Outputting solution to console
c This is CryptoMiniSat 2.9.8
c Finding non-binary XORs:     0.00 s (found:      32, avg size: 3.8)
c conflicts                : 158517      (185611.88 / sec)
c decisions                : 197651      (0.85      % random)
c bogo-props               : 393560907   (460831202.64 / sec)
c conflict literals        : 2699507     (17.83     % deleted)
c Memory used              : 37.68       MB
c CPU time                 : 0.85        s
s UNSATISFIABLE

Full log mod2-3cage-unsat-9-10.cnf.log.crypto.

mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf:

$ cryptominisatLinux64 mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf
c This is CryptoMiniSat 2.9.8
*** INTERRUPTED ***
c num threads              : 1
c restarts                 : 415
c dynamic restarts         : 118
c static restarts          : 297
c full restarts            : 7
c total simplify time      : 0.01
c learnts DL2              : 0
c learnts size 2           : 1649
c learnts size 1           : 0           (0.00      % of vars)
c filedLit time            : 121.38      (0.16      % time)
c v-elim SatELite          : 116         (33.33     % vars)
c SatELite time            : 3924.53     (5.33      % time)
c v-elim xor               : 0           (0.00      % vars)
c xor elim time            : 6.58        (0.01      % time)
c num binary xor trees     : 3
c binxor trees' crown      : 7           (2.33      leafs/tree)
c bin xor find time        : 0.00
c OTF clause improved      : 753548      (0.01      clauses/conflict)
c OTF impr. size diff      : 865263      (1.15       lits/clause)
c OTF cl watch-shrink      : 75306345    (0.87      clauses/conflict)
c OTF cl watch-sh-lit      : 526543155   (6.99       lits/clause)
c tried to recurMin cls    : 4345605     (5.02       % of conflicts)
c updated cache            : 67090       (0.02       lits/tried recurMin)
c clauses over max glue    : 0           (0.00      % of all clauses)
c conflicts                : 86498724    (1175.00   / sec)
c decisions                : 90622941    (0.10      % random)
c bogo-props               : 16863905858054 (229078816.06 / sec)
c conflict literals        : 2926984465  (35.30     % deleted)
c Memory used              : 1307.41     MB
c CPU time                 : 73616.17    s

Full log mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf.log.crypto.

mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf:

$ cryptominisatLinux64 mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf
c This is CryptoMiniSat 2.9.8
*** INTERRUPTED ***
c num threads              : 1
c restarts                 : 163482
c dynamic restarts         : 163209
c static restarts          : 273
c full restarts            : 7
c total simplify time      : 0.30
c learnts DL2              : 0
c learnts size 2           : 2088
c learnts size 1           : 0           (0.00      % of vars)
c filedLit time            : 129.57      (0.18      % time)
c v-elim SatELite          : 232         (33.33     % vars)
c SatELite time            : 27678.63    (37.69     % time)
c v-elim xor               : 0           (0.00      % vars)
c xor elim time            : 12.76       (0.02      % time)
c num binary xor trees     : 0
c binxor trees' crown      : 0           (-nan      leafs/tree)
c bin xor find time        : 0.00
c OTF clause improved      : 1726122     (0.01      clauses/conflict)
c OTF impr. size diff      : 2161892     (1.25       lits/clause)
c OTF cl watch-shrink      : 107939754   (0.71      clauses/conflict)
c OTF cl watch-sh-lit      : 600143904   (5.56       lits/clause)
c tried to recurMin cls    : 6396250     (4.19       % of conflicts)
c updated cache            : 150519      (0.02       lits/tried recurMin)
c clauses over max glue    : 0           (0.00      % of all clauses)
c conflicts                : 152569643   (2077.75   / sec)
c decisions                : 211788006   (0.15      % random)
c bogo-props               : 12581748824367 (171343166.74 / sec)
c conflict literals        : 4818835838  (28.25     % deleted)
c Memory used              : 3297.49     MB
c CPU time                 : 73430.12    s

Full log mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf.log.crypto.

treengeling

Full log mod2-3cage-unsat-9-10.cnf.log.tling.

Full log mod2-3cage-unsat-9-10-vertex-cover-with-conflicts.cnf.log.tling.

Full log mod2-3cage-unsat-9-10-vertex-cover-with-conflicts-red-elim.cnf.log.tling.

Full log mod2-3cage-unsat-9-10-vertex-cover-without-conflicts.cnf.log.tling.

[1]I will eventually document the satoku matrix in any case. However, if there is nothing new, I can spare myself the effort of annoying anybody else with my lack of mathematical knowledge.

Copyright

Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.