Author: | Wolfgang Scherer |
---|

**Old News**

- Distributive expansion of CNF problems resulting in a set of minimal partial solutions is well known.

**News**

- Distributive expansion to retrieve a unique set of partial solutions.
- Direct collection of partial solutions which are guaranteed to be satisfiable by successive clause elimination.

It is sufficient to use a very simple example to demonstrate the features of the different solution sets, that can be obtained with a satoku matrix.

Boolean formula:

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

Clause vectors:

[ 1 1 _ _ ] [ 0 _ 1 _ ] [ _ 1 _ 0 ] p q r s

Applying distributive expansion to a CNF boolean formula delivers a DNF formula, where each elementary conjunction represents a possibly partial solution for the CNF problem. These solutions are minimal, i.e., after assigning the truth values to the variables, each clause of the CNF problem has at least one literal which is true. Any remaining unassigned variables can be bound arbitrarily either way without changing the final result. (Found in an old issue of Bronstein).

As far as I am concerned, that is suffcient to define a solution. I really do not understand, that a proper solution should have to assign all variables. Especially with optimization in mind, minimal solutions are really the better way to go.

Here is the distributive expansion for the given example problem, done manually in the boolean way:

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

The result of the programmatic distributive expansion via clause vectors (satoku.py --expand):

[ 1 _ 1 0 ] [ 0 1 _ _ ] [ _ 1 1 _ ] p q r s

Basic mapping to a satoku matrix

Distributive expansion of core problem: Add quadruplicate requests for
*s*_{00}, *s*_{01}, *s*_{10}, *s*_{11}, *s*_{20}, *s*_{21}

Distributive expansion of core problem: Run RUA

Distributive expansion of core problem: Remove contradictions, identify conjunctions

Remove redundant selections from solution set to obtain minimal solutions

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

Mapping to satoku matrix with conflict maximization

Remove redundant clause in core problem, distributive expansion, identify unique solutions

A micromal solution is a variable assignment that guarantees, that no matter which other assignments are made to satisfy as yet unsatisfied clauses consecutively, the result will still be a solution for the problem.

Note

See properly formalized version below (Verification of Partial Assignments).

This type of solution can be retrieved directly from the plain satoku
matrix after requirements update. Choose any partial assignment in the
intersecting region of the core problem and the variable region and
convert it to a conjunctive clause vector (
*s*_{21}
):

[ _ _ _ 0 ] // conjunction

Remove satisfied clauses from the original problem clause vectors:

[ _ _ _ 0 ] // solution (conjunction) ----------- [ 1 1 _ _ ] // unsatisfied clauses (disjunctions) [ 0 _ 1 _ ] [ _ 1 _ 0 ] => [ 1 1 _ _ ] // unsatisfied clauses [ 0 _ 1 _ ]

Consecutively choose a literal from unsatisfied clauses, add it to the partial solution and remove the satisfied clauses:

[ 1 _ _ 0 ] ----------- [ 1 1 _ _ ] [ 0 _ 1 _ ] => [ 0 _ 1 _ ]

Remove the negated literal from the unsatisfied clauses:

[ 1 _ _ 0 ] ----------- [ 0 _ 1 _ ] => [ _ _ 1 _ ]

Note, that if a single literal remains in a clause, it must be added to the partial solution immediately:

[ 1 _ 1 0 ] ----------- [ _ _ 1 _ ] => []

Use the following method to retrieve solutions from the satoku matrix avoiding some duplicate solutions.

Choose one of the longest partial assignments in the intersecting
region of the core problem and the variable region and convert it to a
clause vector (
*s*_{10}
):

[ 0 1 _ _ ] ----------- [ 1 1 _ _ ] [ 0 _ 1 _ ] [ _ 1 _ 0 ] => []

Since there are no remaining clauses, every clause is satisfied. Therefore, this is also a regular minimal solution.

Now disable this selection in the matrix to avoid duplicate assignments:

Choose the next longest partial assignment, e.g.
*s*_{21}
:

[ _ _ 1 0 ] ----------- [ 1 1 _ _ ] [ 0 _ 1 _ ] [ _ 1 _ 0 ] => [ 1 1 _ _ ]

Only one clause remains, which can be satisfied either way.

Now disable this selection in the matrix and remove redundant selection rows/clauses:

If the core problem section does not present any conflicts
(
*s*_{01}
), the global problem status can be used as sole
solution:

[ _ 1 1 _ ] ----------- [ 1 1 _ _ ] [ 0 _ 1 _ ] [ _ 1 _ 0 ] => []

Map a set of disjunctive clauses from a CNF problem to a set of disjunctive problem clause vectors, where a column stands for a variable.

- If a variable appears unnegated in a clause, set the value in the corresponding clause vector column to 1.
- If a variable appears negated in a clause, set the value in the corresponding clause vector column to 0.
- If a variable does not appear negated in a clause, set the value in the corresponding clause vector column to `_´.

If a column value is set to 0 or 1, it is assigned. If a column value is set to `_´ it is not assigned.

The complement of 0 is 1 and the complement of 1 is 0. The complement of `_´ is again `_´.

Example for variables
*a*0, *a*1, *a*2, *a*3, *a*4, *a*5, *a*6, *a*7, *a*8
:

[ 1 0 1 _ _ _ _ _ _ ] // OR, disjunctions [ 1 1 0 _ _ _ _ _ _ ] [ 0 1 1 _ _ _ _ _ _ ] [ 0 0 0 _ _ _ _ _ _ ] [ 0 _ _ 0 0 _ _ _ _ ] [ 0 _ _ 1 1 _ _ _ _ ] [ 1 _ _ 1 0 _ _ _ _ ] [ 1 _ _ 0 1 _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ 1 ] [ _ 0 _ _ _ 1 _ _ 1 ] [ _ 1 _ _ _ 1 _ _ 0 ] [ _ 0 _ _ _ 0 _ _ 0 ] [ _ _ 0 _ _ 1 1 _ _ ] [ _ _ 0 _ _ 0 0 _ _ ] [ _ _ 1 _ _ 1 0 _ _ ] [ _ _ 1 _ _ 0 1 _ _ ] [ _ _ _ 0 _ _ _ 1 1 ] [ _ _ _ 0 _ _ _ 0 0 ] [ _ _ _ 1 _ _ _ 0 1 ] [ _ _ _ 1 _ _ _ 1 0 ] [ _ _ _ _ 0 _ 0 0 _ ] [ _ _ _ _ 1 _ 1 0 _ ] [ _ _ _ _ 0 _ 1 1 _ ] [ _ _ _ _ 1 _ 0 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8

A partial assignment vector is a clause vector representing a conjunction. Example:

[ 1 _ _ _ _ _ 1 _ 0 ] // AND, conjunction a a a a a a a a a 0 1 2 3 4 5 6 7 8

Place the partial assignment vector on top of the problem clause vectors and separate them with a horizontal line.

Remove all problem clause vectors, that match a variable assignment (0 or 1) in the partial assignment vector at the top (clauses are satisfied).

Example:

[ 1 _ _ _ _ _ 1 _ 0 ] // AND, conjunction --------------------- [ 0 1 1 _ _ _ _ _ _ ] // OR, disjunctions [ 0 0 0 _ _ _ _ _ _ ] [ 0 _ _ 0 0 _ _ _ _ ] [ 0 _ _ 1 1 _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ 1 ] [ _ 0 _ _ _ 1 _ _ 1 ] [ _ _ 0 _ _ 0 0 _ _ ] [ _ _ 1 _ _ 1 0 _ _ ] [ _ _ _ 0 _ _ _ 1 1 ] [ _ _ _ 1 _ _ _ 0 1 ] [ _ _ _ _ 0 _ 0 0 _ ] [ _ _ _ _ 1 _ 0 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8

For each assigned variable in the partial assignment vectors, remove the complementary assignment from each problem clause vector, by setting the corresponding column to `_´ (satisfying variable assignment is impossible).

Example:

[ 1 _ _ _ _ _ 1 _ 0 ] // AND, conjunction --------------------- [ _ 1 1 _ _ _ _ _ _ ] // OR, disjunctions [ _ 0 0 _ _ _ _ _ _ ] [ _ _ _ 0 0 _ _ _ _ ] [ _ _ _ 1 1 _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ _ ] [ _ 0 _ _ _ 1 _ _ _ ] [ _ _ 0 _ _ 0 _ _ _ ] [ _ _ 1 _ _ 1 _ _ _ ] [ _ _ _ 0 _ _ _ 1 _ ] [ _ _ _ 1 _ _ _ 0 _ ] [ _ _ _ _ 0 _ _ 0 _ ] [ _ _ _ _ 1 _ _ 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8

If a conjunctive clause is reduced to a single assigned variable, set the corresponding column of the partial assignment vector to that value (required assignment). If the column in the partial assignment vector already contains the complementary value, the partial assignment vector is a contradiction.

If a conjunctive clause is reduced, such that no variables are assigned, the partial assignment vector is a contradiction.

If there are still unsatisfied problem clause vecotrs left, but no problem clause vector contains a single value, arbitrarily choose a variable assignment from any problem clause vector and add it to the partial assignment vector.

It is important, that the variable assignment must be chosen from the problem clause vectors. It is not allowed to arbitrarily choose a variable assignment, that does not satisfy any clause!

Example:

Choose a3 = 0 and proceed [ 1 _ _ 0 _ _ 1 _ 0 ] // AND, conjunction --------------------- [ _ 1 1 _ _ _ _ _ _ ] // OR, disjunctions [ _ 0 0 _ _ _ _ _ _ ] [ _ _ _ 0 0 _ _ _ _ ] [ _ _ _ 1 1 _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ _ ] [ _ 0 _ _ _ 1 _ _ _ ] [ _ _ 0 _ _ 0 _ _ _ ] [ _ _ 1 _ _ 1 _ _ _ ] [ _ _ _ 0 _ _ _ 1 _ ] [ _ _ _ 1 _ _ _ 0 _ ] [ _ _ _ _ 0 _ _ 0 _ ] [ _ _ _ _ 1 _ _ 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8

Then proceed with the verification process.

If no problem clause vectors are left (all clauses are satisfied), the partial assignment vector is a satisfying assignment for the original CNF problem. It is called a solution to the problem.

Example:

[ 1 _ _ 0 1 _ 1 0 0 ] // AND, conjunction --------------------- [ _ 1 1 _ _ _ _ _ _ ] // OR, disjunctions [ _ 0 0 _ _ _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ _ ] [ _ 0 _ _ _ 1 _ _ _ ] [ _ _ 0 _ _ 0 _ _ _ ] [ _ _ 1 _ _ 1 _ _ _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8 Choose a2 = 1 and proceed [ 1 0 1 0 1 0 1 0 0 ] // AND, conjunction --------------------- a a a a a a a a a 0 1 2 3 4 5 6 7 8

If it is not possible to remove a variable assignment from a solution so that still all clauses are satisfied, the solution is called minimal. Distributive expansion of a CNF delivers a DNF with all minimal solutions.

If it is impossible to derive a contradiction from a solution and a non-empty set of problem clause vectors, the solution is called sub-minimal.

If it is not possible to remove a variable assignment from a solution, without allowing derivation of a contradiction, the solution is called micromal.

The initial solution is micromal for the above example:

[ 1 _ _ _ _ _ 1 _ 0 ] // initial solution (AND) a a a a a a a a a 0 1 2 3 4 5 6 7 8

E.g., if a0 is removed from the initial solution:

[ _ _ _ _ _ _ 1 _ 0 ] // a0 removed a a a a a a a a a 0 1 2 3 4 5 6 7 8

it is possible to derive a contradiction:

Choose a0 = 0 and proceed [ 0 _ _ _ _ _ 1 _ 0 ] // AND, conjunction --------------------- [ _ 0 1 _ _ _ _ _ _ ] // OR, disjunctions [ _ 1 0 _ _ _ _ _ _ ] [ _ _ _ 1 0 _ _ _ _ ] [ _ _ _ 0 1 _ _ _ _ ] [ _ 1 _ _ _ 0 _ _ _ ] [ _ 0 _ _ _ 1 _ _ _ ] [ _ _ 0 _ _ 0 _ _ _ ] [ _ _ 1 _ _ 1 _ _ _ ] [ _ _ _ 0 _ _ _ 1 _ ] [ _ _ _ 1 _ _ _ 0 _ ] [ _ _ _ _ 0 _ _ 0 _ ] [ _ _ _ _ 1 _ _ 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8 Choose a1 = 0 and proceed [ 0 0 0 _ _ 0 1 _ 0 ] // AND, conjunction --------------------- [ _ _ _ 1 0 _ _ _ _ ] // OR, disjunctions [ _ _ _ 0 1 _ _ _ _ ] [ _ _ _ _ _ _ _ _ _ ] // CONTRADICTION [ _ _ _ 0 _ _ _ 1 _ ] [ _ _ _ 1 _ _ _ 0 _ ] [ _ _ _ _ 0 _ _ 0 _ ] [ _ _ _ _ 1 _ _ 1 _ ] a a a a a a a a a 0 1 2 3 4 5 6 7 8

**Copyright**

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