Indirect Conflicts

Author: Wolfgang Scherer

Contents

4-SAT Base Problem

Indirect Conflicts are best illustrated in a 4-SAT context.

Boolean formula:

(  a0 ∨  a1 ∨  a2 ∨  a3 ) ∧
(  b0 ∨  b1 ∨  b2 ∨  b3 ) ∧
(  c0 ∨  c1 ∨  c2 ∨  c3 ) ∧
( ¬a0 ∨ ¬c2 ) ∧
( ¬a0 ∨ ¬c3 ) ∧
( ¬a1 ∨ ¬c2 ) ∧
( ¬a1 ∨ ¬c3 ) ∧
( ¬a2 ∨ ¬c0 ) ∧
( ¬a2 ∨ ¬c1 ) ∧
( ¬a3 ∨ ¬c0 ) ∧
( ¬a3 ∨ ¬c1 ) ∧
( ¬b0 ∨ ¬c0 ) ∧
( ¬b0 ∨ ¬c1 ) ∧
( ¬b1 ∨ ¬c0 ) ∧
( ¬b1 ∨ ¬c1 ) ∧
( ¬b2 ∨ ¬c2 ) ∧
( ¬b2 ∨ ¬c3 ) ∧
( ¬b3 ∨ ¬c2 ) ∧
( ¬b3 ∨ ¬c3 )

Clause vectors:

[ 1 1 1 1 _ _ _ _ _ _ _ _ ]
[ _ _ _ _ 1 1 1 1 _ _ _ _ ]
[ _ _ _ _ _ _ _ _ 1 1 1 1 ]
[ 0 _ _ _ _ _ _ _ _ _ 0 _ ]
[ 0 _ _ _ _ _ _ _ _ _ _ 0 ]
[ _ 0 _ _ _ _ _ _ _ _ 0 _ ]
[ _ 0 _ _ _ _ _ _ _ _ _ 0 ]
[ _ _ 0 _ _ _ _ _ 0 _ _ _ ]
[ _ _ 0 _ _ _ _ _ _ 0 _ _ ]
[ _ _ _ 0 _ _ _ _ 0 _ _ _ ]
[ _ _ _ 0 _ _ _ _ _ 0 _ _ ]
[ _ _ _ _ 0 _ _ _ 0 _ _ _ ]
[ _ _ _ _ 0 _ _ _ _ 0 _ _ ]
[ _ _ _ _ _ 0 _ _ 0 _ _ _ ]
[ _ _ _ _ _ 0 _ _ _ 0 _ _ ]
[ _ _ _ _ _ _ 0 _ _ _ 0 _ ]
[ _ _ _ _ _ _ 0 _ _ _ _ 0 ]
[ _ _ _ _ _ _ _ 0 _ _ 0 _ ]
[ _ _ _ _ _ _ _ 0 _ _ _ 0 ]
  a a a a b b b b c c c c
  0 1 2 3 0 1 2 3 0 1 2 3

Satoku Matrix

It can be seen, if e.g. selection rows s00 and s10 are both selected, that clause segments s00, 2, s10, 2 would be filled entirely with zeroes, making s00 and s10 unselectable. Therefore, selecting both s00 and s10 leads to a contradiction.

Plain mapping does not detect the indirect conflicts:

000-indirect-conflict.r.v-000-color.png

Plain mapping does not detect the indirect conflicts

Conflict maximization does not detect the indirect dependencies:

000-indirect-conflict.x.v-000.png

Conflict maximization does not detect the indirect dependencies

Detecting Indirect Conflicts

It is possible to use combination of selection rows in additional clauses to detect such contradictions.

Minimal Combination of 2 Selection Rows

When combining selection rows s00, s10 in a new clause with an alternative that has no dependencies at all:

000-indirect-conflict.x.v-001.png

Combine selection rows s00, s10 minimal

and running the RUA, the conflict is detected. However it is not propagated to the source selection rows:

000-indirect-conflict.x.v-002.png

Combine selection rows s00, s10 minimal, run RUA

Selection Row Variables

Construct variables for selection rows s00, s10

000-indirect-conflict.x.v-003.png

Construct variables for selection rows s00, s10

Combine selection rows s00, s10 via selection row variables

000-indirect-conflict.x.v-004.png

Combine selection rows s00, s10 via selection row variables

Combine selection rows s00, s10 via selection row variables, run RUA

000-indirect-conflict.x.v-005.png

Combine selection rows s00, s10 via selection row variables, run RUA

Combination of 2 Selection Rows with Proper Alternatives

Combine selection rows s00, s11 with alternatives

000-indirect-conflict.x.v-006.png

Combine selection rows s00, s11 with alternatives

Combine selection rows s00, s11 with alternatives, run RUA

000-indirect-conflict.x.v-007.png

Combine selection rows s00, s11 with alternatives, run RUA

Combination of a Selection Row with an Entire Clause Sub-Matrix

Combine selection row s01 with alternative rows s10, s11, s12, s13

000-indirect-conflict.x.v-008.png

Combine selection row s01 with alternative rows s10, s11, s12, s13

Combine selection row s01 with alternative rows s10, s11, s12, s13 , run RUA

000-indirect-conflict.x.v-009.png

Combine selection row s01 with alternative rows s10, s11, s12, s13 , run RUA

Remaining Conflicts

The disambiguation also works with more than one selection row combined with an entire clause sub-matrix.

Full combination of selection rows s02, s03 with sub-matrix S1 , run RUA

000-indirect-conflict.x.v-010.png

Full combination of selection rows s02, s03 with sub-matrix S1 , run RUA

3-SAT Indirect Conflicts

Indirect conflicts in a 3-SAT context are analogous to the 4-SAT context.

Translate 4-SAT to 3-SAT

Translate the 4-SAT problem to a 3-SAT problem by splitting each 4-SAT clause into 2 3-SAT clauses:

020-indirect-conflict-snf-conjunctions-3SAT.png

Translate 4-SAT to 3-SAT clauses

Derive boolean problem:

(( ¬a0 ∧ ¬p0 ) ∨ ( ¬a1 ∧ ¬p0 ) ∨ (  p0 )) ∧
(( ¬a2 ∧  p0 ) ∨ ( ¬a3 ∧  p0 ) ∨ ( ¬p0 )) ∧
(( ¬b0 ∧  p1 ) ∨ ( ¬b2 ∧  p1 ) ∨ ( ¬p1 )) ∧
(( ¬b1 ∧ ¬p1 ) ∨ ( ¬b3 ∧ ¬p1 ) ∨ (  p1 )) ∧
((  a2 ∧  a3 ∧  b0 ∧  b1 ∧ ¬p0 ∧  p2 ) ∨ (  a0 ∧  a1 ∧  b2 ∧  b3 ∧  p0 ∧  p2 ) ∨ ( ¬p2 )) ∧
((  a2 ∧  a3 ∧  b0 ∧  b1 ∧ ¬p0 ∧ ¬p2 ) ∨ (  a0 ∧  a1 ∧  b2 ∧  b3 ∧  p0 ∧ ¬p2 ) ∨ (  p2 )

Clause vectors:

[
  [ 0 _ _ _ _ _ _ _ 0 _ _ ]
  [ _ 0 _ _ _ _ _ _ 0 _ _ ]
  [ _ _ _ _ _ _ _ _ 1 _ _ ]
]
[
  [ _ _ 0 _ _ _ _ _ 1 _ _ ]
  [ _ _ _ 0 _ _ _ _ 1 _ _ ]
  [ _ _ _ _ _ _ _ _ 0 _ _ ]
]
[
  [ _ _ _ _ 0 _ _ _ _ 1 _ ]
  [ _ _ _ _ _ _ 0 _ _ 1 _ ]
  [ _ _ _ _ _ _ _ _ _ 0 _ ]
]
[
  [ _ _ _ _ _ 0 _ _ _ 0 _ ]
  [ _ _ _ _ _ _ _ 0 _ 0 _ ]
  [ _ _ _ _ _ _ _ _ _ 1 _ ]
]
[
  [ _ _ 1 1 1 1 _ _ 0 _ 1 ]
  [ 1 1 _ _ _ _ 1 1 1 _ 1 ]
  [ _ _ _ _ _ _ _ _ _ _ 0 ]
]
[
  [ _ _ 1 1 1 1 _ _ 0 _ 0 ]
  [ 1 1 _ _ _ _ 1 1 1 _ 0 ]
  [ _ _ _ _ _ _ _ _ _ _ 1 ]
]
    a a a a b b b b p p p
    0 1 2 3 0 1 2 3 0 1 2

Remap to satoku matrix:

020-indirect-conflict-snf-conjunctions-3SAT.r.v-000.png

Remapped 3-SAT problem

Detect Indirect Conflicts

Construct variables for selection rows s00, s20

020-indirect-conflict-snf-conjunctions-3SAT-001.png

Construct variables for selection rows s00, s20

Combine selection rows s00, s20 via selection row variables

020-indirect-conflict-snf-conjunctions-3SAT-002.png

Combine selection rows s00, s20 via selection row variables

Combine selection rows s00, s20 via selection row variables, run RUA

020-indirect-conflict-snf-conjunctions-3SAT-003.png

Combine selection rows s00, s20 via selection row variables, run RUA

Indirect 2-SAT Conflicts

In a 2-SAT context, there can only be indirect conflicts, if the requirements update algorithm is not applied.

In this example:

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

with clause vectors:

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

selecting rows s00 and s10 will lead to a contradiction:

050-indirect-2SAT.n.v-000.png

Indirect 2-SAT Conflicts

After running the RUA, all dependencies are detected and propagated.

050-indirect-2SAT.n.v-001.png

Indirect 2-SAT Conflicts, run RUA

Since there cannot be any indirect conflicts, unsatisfiability of a 2-SAT problem is detected after the initial RUA run.

If it was possible for 2-SAT problems to have indirect conflicts, it would also be possible to translate any k-SAT problem for k ≥ 3 to a 2-SAT problem.

1-SAT Conflicts

Trivially, 1-SAT conflicts signify unsatisfiablity. Therefore there cannot be any conflicts at all, if a 1-SAT problem is satisfiable.

Boolean formula:

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

Clause vectors:

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

Satoku matrix:

060-indirect-1SAT.r.v-000.png

1-SAT conflicts signify unsatisfiablity

Copyright

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