Various Resolution Algorithms

Author: Wolfgang Scherer

Contents

Base Problem (3-variable AND)

EXAMPLE-3-AND-000.png

EXAMPLE-3-AND-000.png

Selection Normal Form (SNF)

EXAMPLE-3-AND-000.mtx.fca.png

EXAMPLE-3-AND-000.mtx.fca.png

Selection Row Variables

EXAMPLE-3-AND-001-sel-row-variables.png

EXAMPLE-3-AND-001-sel-row-variables.png

X1 Not Row Or All

EXAMPLE-3-AND-002-x1-not-row-or-all-00.png

EXAMPLE-3-AND-002-x1-not-row-or-all-00.png

EXAMPLE-3-AND-002-x1-not-row-or-all-01.png

EXAMPLE-3-AND-002-x1-not-row-or-all-01.png

EXAMPLE-3-AND-002-x1-not-row-or-all-02.png

EXAMPLE-3-AND-002-x1-not-row-or-all-02.png

EXAMPLE-3-AND-002-x1-not-row-or-all-03.png

EXAMPLE-3-AND-002-x1-not-row-or-all-03.png

EXAMPLE-3-AND-002-x1-not-row-or-all-04.png

EXAMPLE-3-AND-002-x1-not-row-or-all-04.png

EXAMPLE-3-AND-002-x1-not-row-or-all-05.png

EXAMPLE-3-AND-002-x1-not-row-or-all-05.png

EXAMPLE-3-AND-002-x1-not-row-or-all-06.png

EXAMPLE-3-AND-002-x1-not-row-or-all-06.png

EXAMPLE-3-AND-002-x1-not-row-or-all-07.png

EXAMPLE-3-AND-002-x1-not-row-or-all-07.png

EXAMPLE-3-AND-002-x1-not-row-or-all-08.png

EXAMPLE-3-AND-002-x1-not-row-or-all-08.png

EXAMPLE-3-AND-002-x1-not-row-or-all-09.png

EXAMPLE-3-AND-002-x1-not-row-or-all-09.png

X1 Not Row Or All - Short

EXAMPLE-3-AND-003-x1-not-row-or-all-short-00.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-00.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-01.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-01.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-02.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-02.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-03.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-03.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-04.png

EXAMPLE-3-AND-003-x1-not-row-or-all-short-04.png

X1 Conflict Or None

EXAMPLE-3-AND-004-x1-conflict-or-none-00.png

EXAMPLE-3-AND-004-x1-conflict-or-none-00.png

EXAMPLE-3-AND-004-x1-conflict-or-none-01.png

EXAMPLE-3-AND-004-x1-conflict-or-none-01.png

EXAMPLE-3-AND-004-x1-conflict-or-none-02.png

EXAMPLE-3-AND-004-x1-conflict-or-none-02.png

EXAMPLE-3-AND-004-x1-conflict-or-none-03.png

EXAMPLE-3-AND-004-x1-conflict-or-none-03.png

EXAMPLE-3-AND-004-x1-conflict-or-none-04.png

EXAMPLE-3-AND-004-x1-conflict-or-none-04.png

EXAMPLE-3-AND-004-x1-conflict-or-none-05.png

EXAMPLE-3-AND-004-x1-conflict-or-none-05.png

EXAMPLE-3-AND-004-x1-conflict-or-none-06.png

EXAMPLE-3-AND-004-x1-conflict-or-none-06.png

EXAMPLE-3-AND-004-x1-conflict-or-none-07.png

EXAMPLE-3-AND-004-x1-conflict-or-none-07.png

EXAMPLE-3-AND-004-x1-conflict-or-none-08.png

EXAMPLE-3-AND-004-x1-conflict-or-none-08.png

EXAMPLE-3-AND-004-x1-conflict-or-none-09.png

EXAMPLE-3-AND-004-x1-conflict-or-none-09.png

Fast 2-SAT Reduction

EXAMPLE-3-AND-005-fast-2SAT-reduction-00.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-00.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-01.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-01.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-02.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-02.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-03.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-03.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-04.png

EXAMPLE-3-AND-005-fast-2SAT-reduction-04.png

X1 Conflict Or None - All

EXAMPLE-3-AND-006-x1-conflict-or-none-all-00.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-00.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-01.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-01.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-03.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-03.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-04.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-04.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-05.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-05.png

X1 Not Sel Row Or All

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-00.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-00.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-01.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-01.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-02.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-02.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-03.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-03.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-04.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-04.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-05.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-05.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-06.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-06.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-07.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-07.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-08.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-08.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-09.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-09.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-10.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-10.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-11.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-11.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-12.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-12.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-13.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-13.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-14.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-14.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-15.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-15.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-16.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-16.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-17.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-17.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-18.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-18.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-19.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-19.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-20.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-20.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-21.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-21.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-22.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-22.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-23.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-23.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-24.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-24.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-25.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-25.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-26.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-26.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-27.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-27.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-28.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-28.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-29.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-29.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-30.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-30.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-31.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-31.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-32.png

EXAMPLE-3-AND-006-x1-conflict-or-none-all-02-x1-not-sel-row-or-all-32.png

Variable Identities

EXAMPLE-3-AND-007.mtx.fca-variable-identities-00.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-00.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-01.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-01.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-02.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-02.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-03.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-03.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-04.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-04.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-05.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-05.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-06.png

EXAMPLE-3-AND-007.mtx.fca-variable-identities-06.png

Selection Row Identities

EXAMPLE-3-AND-008.mtx.fca-sel-row-identities-00.png

EXAMPLE-3-AND-008.mtx.fca-sel-row-identities-00.png

EXAMPLE-3-AND-008.mtx.fca-sel-row-identities-01.png

EXAMPLE-3-AND-008.mtx.fca-sel-row-identities-01.png

Copyright

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