Author: | Wolfgang Scherer |
---|

Contents

Propositional logic does not provide the best abstraction for the satoku matrix. In fact it is actually quite misleading. However, it is still useful to express the principle of partial distributive expansion in propositional logic, as it provides a good amount of redundancy to understand the concept.

Since it is meant as a hint only, the description is informal to avoid a duplication of efforts. I.e., nothing in this description is necessary to define the satoku matrix.

Starting with the propositional CNF formula *P* with *m* = |*P*| disjunctive clauses *C* of size *k*:

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

Convert each disjunction *C* of literals to a disjunction *S* of conjunctions *s*:

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

As visual hint, spread each conjunction *s* of each disjunction *S* over two lines:

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

Extend each conjunction *s* with truth values TRUE to a length
of *k***m* in the following manner:

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

If pseudo code is preferred:

def spread_problem(P): PM = [] w = sum([len(C) for C in P]) o = 0 for C in enumerate(P): d = [] PM.append(d) for lit in C: c = [ true for i in range(w) ] c[o] = lit d.append(c) o += 1 return PM

Disjunctions *S* are labeled *S*_{i}, *i* = (0, 1, .., *m* − 1), *m* = |*P*|.

Conjunctions *s* are labeled *s*_{ij}, *j* = (0, 1, .., |*S*_{i}| − 1).

Literals are labeled as row, column pairs *s*_{ij, fg}, *f* = (0, 1, .., *m* − 1), *g* = (0, 1, .., |*S*_{i}| − 1).

Literals *s*_{ij, ij} are the original literals of the clause.

It is easier to work on a matrix *SM*, (or call it table, if you
must) when performing the partial distributive expansion for partial
assignments *s*_{ij} representing selections of the
corresponding selection problem:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | | | :math:`s_{{0}_{1}}` | ¬b | | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | | ¬a | | | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | | | a | | :math:`s_{{2}_{1}}` | | | b | | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | | | | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

Following the consequences of the selection problem, observe, that if
*s*_{00} is **eventually** selected, then
*s*_{20} can no longer be selected, because literal
*a* at position *s*_{20, 20} conflicts with
literal ¬*a* at position *s*_{00, 00},
therefore, *s*_{21} must **then** be selected to preserve
satisfiability.

It makes no difference, whether this required selection is made later
as a matter of circumstances, or if it is promised in advance by
refining partial assignment *s*_{00} with literal *b*
at position *s*_{00, 21}:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | b | | :math:`s_{{0}_{1}}` | ¬b | | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | | ¬a | | | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | | | a | | :math:`s_{{2}_{1}}` | | | b | | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | | | | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

By analogy, the same is true for conflicting selections
*s*_{20} and *s*_{00}:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | b | | :math:`s_{{0}_{1}}` | ¬b | | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | | ¬a | | | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | ¬b | | a | | :math:`s_{{2}_{1}}` | | | b | | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | | | | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

Distributive expansion of clauses *S*_{0}, *S*_{2} shows, that
this is exactly what will happen:

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

Determining the complete set of satisfying assignments is equivalent
to distributive expansion of the entire CNF formula *P*, which
generates the set of prime implicants *I* for a formula
*P*, where each *I* extends to one or more satisfying
assignments.

Therefore performing partial distributive expansion facilitates obtaining the complete set of satisfying assignments for a proposisitional problem in CNF.

Proceeding further, *SM* is transformed to:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | b | c | :math:`s_{{0}_{1}}` | ¬b | | a | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | | ¬a | b | c | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | ¬b | d | a | | :math:`s_{{2}_{1}}` | ¬a | | b | | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | ¬b | d | | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

*SM* is equivalent to the region of clause conflict sub-matrixes
[*S*_{00}, *S*_{33}] of the following satoku matrix:

Observe, that partial assignment *s*_{01}, which requires
partial assignment *s*_{20} is no longer consistent, since
*s*_{20} has been refined with *d* from
*s*_{11, 11} by the first round of partial
distributive expansion. It is therefore necessary to refine
*s*_{01} with *d* at position *s*_{01, 11} also:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | b | c | :math:`s_{{0}_{1}}` | ¬b | d | a | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | | ¬a | b | c | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | ¬b | d | a | | :math:`s_{{2}_{1}}` | ¬a | | b | | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | ¬b | d | | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

Following all consequences, *SM* is transformed to:

---------------------+-------+-------+-------+-------+ :math:`s_{{0}_{0}}` | ¬a | | b | c | :math:`s_{{0}_{1}}` | ¬b | d | a | | ---------------------+-------+-------+-------+-------+ :math:`s_{{1}_{0}}` | ¬a | ¬a | b | c | :math:`s_{{1}_{1}}` | | d | | | ---------------------+-------+-------+-------+-------+ :math:`s_{{2}_{0}}` | ¬b | d | a | | :math:`s_{{2}_{1}}` | ¬a | | b | c | ---------------------+-------+-------+-------+-------+ :math:`s_{{3}_{0}}` | ¬b | d | a | a | :math:`s_{{3}_{1}}` | | | | c | ---------------------+-------+-------+-------+-------+

which is equivalent to the region of clause conflict sub-matrixes
[*S*_{00}, *S*_{33}] in the following satoku matrix:

Translating *SM* into a propositional formula *PM* renders
a conjunction of disjunctions of partial assignments
*s*_{ij}:

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

Induction over the full truth table shows that *P* and
*PM* are logically equivalent. And since that is so, it is
irrelevant to propose a logical difference between CNF and a
conjunction of DNFs.

It is obvious, that each of the prime implicants *I*:

( ¬a ∧ b ∧ c ) ( a ∧ ¬b ∧ d )

obtained by a full distributive expansion of *PM* must
necessarily be a conjunction *s*_{ij}∧..∧*s*_{fg} of at least 2 non-conflicting partial assignments from
*PM*.

Under certain conditions, the set of partial assignments
*s*_{ij} represents a set *RA* of reliable
assignments *r*, which are guaranteed to extend to a satisfying
assignment under all branches of DPLL. I.e., DPLL can never resolve an
empty clause.

For a 2-SAT problem, the conditions are met as soon as the partial distributive expansion is fully completed. A 2-SAT problem is also trivially satisfiable, if the partial distributive expansion does not produce 2 contradictions in a single clause.

The satoku matrix processes propositional problems by mapping
propositional formulas specified as a conjunction of arbitrary DNFs to
the equivalent selection problem in an inverted adjacency matrix. It
further abstracts propositional variables to special cases of
2-literal clauses (*p*∨¬*p*).

It is obvious, that graph theory is necessary to describe the satoku
matrix, but not sufficient to describe partial distributive expansion
as it lacks the necessary expressiveness in regard to clause
constraints of CNF formulas. The atoms of the satoku matrix are not
vertices, but vertex clusters including edges. A variety of subatomic
particles includes edge clusters, partial assignments
(aka. selections). The ambiguity of propositional variables is
permanently exposed instead of hidden behind the necessity that a
decision has to be made *eventually*.

It is obvious, that propositional logic is sufficient and necessary to describe the satoku matrix, but it lacks the necessary expressiveness to describe partial distributive expansion in a simple and intuitive manner. It also lacks the connectivity and transformative power of a graph.

Many observations made in the context of the satoku matrix are very hard to deduce in both graph theory and propositional logic alone. However, none of those observations violates established knowledge in these fields.

For example, the mentioned set *RA* of reliable assignments does
not appear from refinement of partial assignments, unless partial
distributive expansion is performed in the exact manner described
above. There is also no incentive to construct *RA* by further
minimizing prime implicants due to the exponential time complexity of
the algorithm. A full verification of the reliability property also
has exponential time complexity (although far less than a full
distributive expansion). Therefore this useful property obviously
remains undetected, until deduction from the state of the satoku
matrix insistently suggests, that the reliable assignment presented
must actually be necessary and sufficient to solve the problem.

Another counter-intuitive effect is that *nogoods* are actually highly
desired in the context of the satoku matrix. Because they appear only
as a result of necessary deductions, they reduce the problem size,
which is a good thing. There is no back-tracking in the traditional
sense in the satoku matrix, unless a selection or decision algorithm
is implented on top of it.

The consequences from the illusionary notions of both well-defined CNFs and atomic propositional variables are especially hard to understand without the transformational power of the satoku matrix.

**Copyright**

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