Author: | Wolfgang Scherer |
---|

Contents

In the context of a satoku matrix, boolean variables appear as clause
sub-matrixes with 2 selection rows, where one selection row represents
the unnegated variable and the other selection row represents the
negated variable. The clause sub-matrix of a variable therefore
represents the clause
(*p*∨¬*p*)
.

Since a clause sub-matrix represents possible selections and their dependencies, the variable representation is consistent with the axioms of logic.

- A variable can be true or false
(
*p*=*T*)∨(*p*=*F*),*p*∨¬*p*=*T*. Selection*s*_{00}is interpreted as*p*=*T*, selection*s*_{01}is interpreted as*p*=*F*. Both selections are possible, therefore (*p*=*T*)∨(*p*=*F*) . - A variable cannot be both true and false
*p*∧¬*p*=*F*. The dependency*s*_{00, 01}(and its mirror*s*_{01, 00}) does not allow selecting both a variable and its negation.

An unrestricted truth table for n variables appears as a clause sub-matrix with
2^{n}
selection rows. Each selection row represents one of the
possible conjunctions of the variables.

Unrestricted Truth Table for 4 Variables

The unrestricted truth table for 4 variables can therefore be interpreted as representation of a disjunction of all possible conjunctions for 4 variables:

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

The following examples for mapping a disjunction and a conjunction of 4 variables as well as an arbitrarily defined function F, are used to illustrate the mapping options.

p | q | r | s | p ∨ q ∨ r ∨ s | p ∧ q ∧ r ∧ s | F |
---|---|---|---|---|---|---|

0 | 0 | 0 | 0 | 0 | 0 | 0 |

0 | 0 | 0 | 1 | 1 | 0 | 1 |

0 | 0 | 1 | 0 | 1 | 0 | 1 |

0 | 0 | 1 | 1 | 1 | 0 | 0 |

0 | 1 | 0 | 0 | 1 | 0 | 0 |

0 | 1 | 0 | 1 | 1 | 0 | 0 |

0 | 1 | 1 | 0 | 1 | 0 | 1 |

0 | 1 | 1 | 1 | 1 | 0 | 0 |

1 | 0 | 0 | 0 | 1 | 0 | 0 |

1 | 0 | 0 | 1 | 1 | 0 | 0 |

1 | 0 | 1 | 0 | 1 | 0 | 1 |

1 | 0 | 1 | 1 | 1 | 0 | 1 |

1 | 1 | 0 | 0 | 1 | 0 | 1 |

1 | 1 | 0 | 1 | 1 | 0 | 0 |

1 | 1 | 1 | 0 | 1 | 0 | 0 |

1 | 1 | 1 | 1 | 1 | 1 | 0 |

If the result of a logical function in a truth table row is 0, the corresponding selection in the unrestricted truth table clause of the satoku matrix is made impossible. I.e., the entire selection row is filled with zeroes.

Map disjunction of 4 variables

Map conjunction of 4 variables

Map arbitrary function F over 4 variables

Instead of disabling selection rows in an unrestricted truth table clause, it is sufficient to construct a clause with the possible selections directly.

For function F, the clause is:

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

which maps to:

The rows with a result of 0 can also be added as clauses. The corresponding conjunction of variables is negated and added as disjunctive clause.

For the disjunction example, the constraint is:

( ¬p ∧ ¬q ∧ ¬r ∧ ¬s ) = F

which is negated:

¬( ¬p ∧ ¬q ∧ ¬r ∧ ¬s ) = T

and converted to a disjunctive clause:

( p ∨ q ∨ r ∨ s ) = T

Map the constraint clause into the satoku matrix by adding requests for the variables of the disjunctive clause:

Updating requirements for the disjunctive constraint, disables
selection row
*s*_{40}
:

The constraints for function F are:

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

Add constraint requests for function F

Updating requirements for disjunctive constraints of function F disables selections in unrestricted truth table

As with the clause of possible selections, the constraint clauses can be mapped directly without the unrestricted truth table. This is equivalent to mapping a CNF problem to a satoku matrix:

Mapping the contraints of function F with conflict maximization, delivers the satoku matrix:

After removing impossible selections and redundancies, the satoku matrix presents as:

Distributive expansion shows, that the solution set is equivalent to the truth table clause for function F above:

Disjunctive resolution is derived from:

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

Disjunctive resolution is denoted here as
*s*_{ij}∩*s*_{fg}
.

By applying pair-wise resolution consecutively to the truth table
clause of a 4 variable disjunction
*S*_{4}
, clause sub-matrix
*S*_{7}
can be derived:

Disjunctive expansion is based on:

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

It is therefore allowed to add longer conjunctions to a disjunctive clause.

Applying disjunctive expansion and disjunctive resolution to clause
*S*_{5}
(the result from the previous reduction) allows
deriviation of the minimal clause sub-matrix
*S*_{11}
:

**Copyright**

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