# Variables, Truth Table, Resolution and Expansion

Author: Wolfgang Scherer

# Variables

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) . Representation of variables in a satoku matrix

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 s00 is interpreted as p = T , selection s01 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 s00, 01 (and its mirror s01, 00 ) does not allow selecting both a variable and its negation.

# Truth Table

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

Unrestricted Truth Table for 4 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 )
)
```

## Mapping Logical Functions from a Truth Table

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

### Disable Selection in Unrestricted Truth Table

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 disjunction of 4 variables

Map conjunction of 4 variables Map conjunction of 4 variables

Map arbitrary function F over 4 variables Map arbitrary function F over 4 variables

### Construct Possible Selections

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: Map arbitrary function F over 4 variables directly

### Add Constraints for Invalid Selections

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: Add constraint requests for disjunction

Updating requirements for the disjunctive constraint, disables selection row s40 : Updating requirements for disjunctive constraint disables s40

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 Add constraint requests for function F

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

### Mapping Constraints Directly

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: Map contraints of function F directly

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

After removing impossible selections and redundancies, the satoku matrix presents as: Contraints of function F cleaned up

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

# Resolution and Expansion

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 sijsfg .

By applying pair-wise resolution consecutively to the truth table clause of a 4 variable disjunction S4 , clause sub-matrix S7 can be derived: Continuous pair-wise resolution

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 S5 (the result from the previous reduction) allows deriviation of the minimal clause sub-matrix S11 : Expansion and resolution for derviation of minimal clause sub-matrix S11 .