Author: | Wolfgang Scherer |
---|

Contents

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

It can be seen, if e.g. selection rows
*s*_{00}
and
*s*_{10}
are both selected, that clause segments
*s*_{00, 2}, *s*_{10, 2}
would be filled entirely with
zeroes, making
*s*_{00}
and
*s*_{10}
unselectable. Therefore, selecting both
*s*_{00}
and
*s*_{10}
leads to a contradiction.

Plain mapping does not detect the indirect conflicts:

Conflict maximization does not detect the indirect dependencies:

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

When combining selection rows
*s*_{00}, *s*_{10}
in a
new clause with an alternative that has no dependencies at all:

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

Construct variables for selection rows
*s*_{00}, *s*_{10}

Combine selection rows
*s*_{00}, *s*_{10}
via selection row variables

Combine selection rows
*s*_{00}, *s*_{10}
via selection row variables, run RUA

Combine selection rows
*s*_{00}, *s*_{11}
with alternatives

Combine selection rows
*s*_{00}, *s*_{11}
with alternatives, run RUA

Combine selection row
*s*_{01}
with alternative rows
*s*_{10}, *s*_{11}, *s*_{12}, *s*_{13}

Combine selection row
*s*_{01}
with alternative rows
*s*_{10}, *s*_{11}, *s*_{12}, *s*_{13}
, run RUA

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

Full combination of selection rows
*s*_{02}, *s*_{03}
with sub-matrix
*S*_{1}
, run RUA

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

Translate the 4-SAT problem to a 3-SAT problem by splitting each 4-SAT clause into 2 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:

Construct variables for selection rows
*s*_{00}, *s*_{20}

Combine selection rows
*s*_{00}, *s*_{20}
via selection row variables

Combine selection rows
*s*_{00}, *s*_{20}
via selection row variables, run RUA

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
*s*_{00}
and
*s*_{10}
will lead
to a contradiction:

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

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.

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:

**Copyright**

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