5-Variable XOR (3-SAT)
| Author: | Wolfgang Scherer |
|---|
Contents
Base Problem (5-Variable XOR)
5-SAT Problem
( ¬a00 ∨ ¬a01 ∨ ¬a02 ∨ ¬a03 ∨ ¬a04 ) ∧ ( ¬a00 ∨ ¬a01 ∨ ¬a02 ∨ a03 ∨ a04 ) ∧ ( ¬a00 ∨ ¬a01 ∨ a02 ∨ ¬a03 ∨ a04 ) ∧ ( ¬a00 ∨ ¬a01 ∨ a02 ∨ a03 ∨ ¬a04 ) ∧ ( ¬a00 ∨ a01 ∨ ¬a02 ∨ ¬a03 ∨ a04 ) ∧ ( ¬a00 ∨ a01 ∨ ¬a02 ∨ a03 ∨ ¬a04 ) ∧ ( ¬a00 ∨ a01 ∨ a02 ∨ ¬a03 ∨ ¬a04 ) ∧ ( ¬a00 ∨ a01 ∨ a02 ∨ a03 ∨ a04 ) ∧ ( a00 ∨ ¬a01 ∨ ¬a02 ∨ ¬a03 ∨ a04 ) ∧ ( a00 ∨ ¬a01 ∨ ¬a02 ∨ a03 ∨ ¬a04 ) ∧ ( a00 ∨ ¬a01 ∨ a02 ∨ ¬a03 ∨ ¬a04 ) ∧ ( a00 ∨ ¬a01 ∨ a02 ∨ a03 ∨ a04 ) ∧ ( a00 ∨ a01 ∨ ¬a02 ∨ ¬a03 ∨ ¬a04 ) ∧ ( a00 ∨ a01 ∨ ¬a02 ∨ a03 ∨ a04 ) ∧ ( a00 ∨ a01 ∨ a02 ∨ ¬a03 ∨ a04 ) ∧ ( a00 ∨ a01 ∨ a02 ∨ a03 ∨ ¬a04 )
5-SAT Clause Vectors
[ 0 0 0 0 0 ] [ 0 0 0 1 1 ] [ 0 0 1 0 1 ] [ 0 0 1 1 0 ] [ 0 1 0 0 1 ] [ 0 1 0 1 0 ] [ 0 1 1 0 0 ] [ 0 1 1 1 1 ] [ 1 0 0 0 1 ] [ 1 0 0 1 0 ] [ 1 0 1 0 0 ] [ 1 0 1 1 1 ] [ 1 1 0 0 0 ] [ 1 1 0 1 1 ] [ 1 1 1 0 1 ] [ 1 1 1 1 0 ] a a a a a 0 0 0 0 0 0 1 2 3 4
The expected clause vector solution set (DNF) is identical to the input clause vector set (CNF), since the number of variables is odd.
3-SAT Problem
( ¬a00 ∨ ¬a01 ∨ ¬o00 ) ∧ ( ¬a02 ∨ o00 ∨ ¬o01 ) ∧ ( ¬a03 ∨ ¬a04 ∨ o01 ) ∧ ( ¬a00 ∨ ¬a01 ∨ ¬o02 ) ∧ ( ¬a02 ∨ o02 ∨ ¬o03 ) ∧ ( a03 ∨ a04 ∨ o03 ) ∧ ( ¬a00 ∨ ¬a01 ∨ ¬o04 ) ∧ ( a02 ∨ o04 ∨ ¬o05 ) ∧ ( ¬a03 ∨ a04 ∨ o05 ) ∧ ( ¬a00 ∨ ¬a01 ∨ ¬o06 ) ∧ ( a02 ∨ o06 ∨ ¬o07 ) ∧ ( a03 ∨ ¬a04 ∨ o07 ) ∧ ( ¬a00 ∨ a01 ∨ ¬o08 ) ∧ ( ¬a02 ∨ o08 ∨ ¬o09 ) ∧ ( ¬a03 ∨ a04 ∨ o09 ) ∧ ( ¬a00 ∨ a01 ∨ ¬o10 ) ∧ ( ¬a02 ∨ o10 ∨ ¬o11 ) ∧ ( a03 ∨ ¬a04 ∨ o11 ) ∧ ( ¬a00 ∨ a01 ∨ ¬o12 ) ∧ ( a02 ∨ o12 ∨ ¬o13 ) ∧ ( ¬a03 ∨ ¬a04 ∨ o13 ) ∧ ( ¬a00 ∨ a01 ∨ ¬o14 ) ∧ ( a02 ∨ o14 ∨ ¬o15 ) ∧ ( a03 ∨ a04 ∨ o15 ) ∧ ( a00 ∨ ¬a01 ∨ ¬o16 ) ∧ ( ¬a02 ∨ o16 ∨ ¬o17 ) ∧ ( ¬a03 ∨ a04 ∨ o17 ) ∧ ( a00 ∨ ¬a01 ∨ ¬o18 ) ∧ ( ¬a02 ∨ o18 ∨ ¬o19 ) ∧ ( a03 ∨ ¬a04 ∨ o19 ) ∧ ( a00 ∨ ¬a01 ∨ ¬o20 ) ∧ ( a02 ∨ o20 ∨ ¬o21 ) ∧ ( ¬a03 ∨ ¬a04 ∨ o21 ) ∧ ( a00 ∨ ¬a01 ∨ ¬o22 ) ∧ ( a02 ∨ o22 ∨ ¬o23 ) ∧ ( a03 ∨ a04 ∨ o23 ) ∧ ( a00 ∨ a01 ∨ ¬o24 ) ∧ ( ¬a02 ∨ o24 ∨ ¬o25 ) ∧ ( ¬a03 ∨ ¬a04 ∨ o25 ) ∧ ( a00 ∨ a01 ∨ ¬o26 ) ∧ ( ¬a02 ∨ o26 ∨ ¬o27 ) ∧ ( a03 ∨ a04 ∨ o27 ) ∧ ( a00 ∨ a01 ∨ ¬o28 ) ∧ ( a02 ∨ o28 ∨ ¬o29 ) ∧ ( ¬a03 ∨ a04 ∨ o29 ) ∧ ( a00 ∨ a01 ∨ ¬o30 ) ∧ ( a02 ∨ o30 ∨ ¬o31 ) ∧ ( a03 ∨ ¬a04 ∨ o31 )
3-SAT Clause Vectors
[ 0 0 _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 0 _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 0 _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 1 _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 0 _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 1 _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 0 _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 0 _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 1 _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ ] [ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ ] [ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ _ _ ] [ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ _ _ ] [ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ _ _ ] [ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ _ _ ] [ _ _ _ 0 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ _ _ ] [ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ _ _ ] [ _ _ 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ _ _ ] [ _ _ _ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ _ _ ] [ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ _ _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 _ _ ] [ _ _ _ 0 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 _ _ ] [ 1 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 0 _ ] [ _ _ 1 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 0 ] [ _ _ _ 1 0 _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 1 ] a a a a a o o o o o o o o o o o o o o o o o o o o o o o o o o o o o o o o 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1 1 1 2 2 2 2 2 2 2 2 2 2 3 3 0 1 2 3 4 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1 2 3 4 5 6 7 8 9 0 1
Complexities:
n-complexity: O(237)m-complexity: O(⌈3 ⁄ 2⌉48) = O(248)
Initial mapping including variables
ex-xor5-3sat-001.v.png
Colored matrix:
ex-xor5-3sat-001.v.cm.png
The colored matrix of the sorted problem gives a better overview:
ex-xor5-3sat-001.v-sorted.cm.png
Redundancies removed, variable identities resolved
This reduces m-complexity to:
O(⌈3/2⌉^20) = O(2^20)
ex-xor5-3sat-002.v.png
Sorted problem colored matrix:
ex-xor5-3sat-002.v-sorted.cm.png
Merge 4-SAT, variable coverage for 2-SAT reduction
Merging 4-SAT clauses, reduces m-complexity to:
O(⌈4/2⌉^10) = O(2^10)
Since splitting any of S[0] .. S[7] in the optimal manner will also reduce the other clauses of that group, the real complexity reduces to:
O(⌈4/2⌉^3) = O(2^3)
Merging 3 variables will also produce a clause with selections that reduce the core problem to 2-SAT. Therefore n-complexity is also:
O(2^3)
ex-xor5-3sat-003.v.png
Colored matrix:
ex-xor5-3sat-003.v.cm.png
Core problem identities
ex-xor5-3sat-004.v.png
Detect invalid selection combinations
ex-xor5-3sat-008.v.png
Use selection/clause resolution to detect dependencies
ex-xor5-3sat-009.v.png
Color matrix:
ex-xor5-3sat-009.v.cm.png
Consolidate Variables
Invalid Selections (Variables)
Invalid Selections (Variables)
Invalid Selections (Variables)
Invalid Selections (Variables)
Variable Identities
Variable Identities
Invalid Selections (Variables)
Invalid Selections (Variables)
XORSAT, new n-complexity O(22)
XORSAT, new n-complexity O(22)
Further redcutions with core problem only
ex-xor5-3sat-100.png
Maximal reduction
ex-xor5-3sat-101.png
The problem is therefore satisfiable. The effective m-complexity is O(P) .
Variable Identities
Instead of core problem identities, variable identities can be used to achieve a complexity reduction. .. |:todo:|
Variable Identities
ex-xor5-3sat-004-05.v.png
Variable Identities
ex-xor5-3sat-004-06.v.png
MiniSat
MiniSat_v1.14_linux ex-xor5-3sat-000.cnf ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 48 144 | 16 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 9 (inf /sec) decisions : 52 (inf /sec) propagations : 73 (inf /sec) conflict literals : 27 (0.00 % deleted) Memory used : 1.67 MB CPU time : 0 s SATISFIABLE
MiniSat_v1.14_linux ex-xor5-3sat-snf.r-000.mtx.cnf ==================================[MINISAT]=================================== | Conflicts | ORIGINAL | LEARNT | Progress | | | Clauses Literals | Limit Clauses Literals Lit/Cl | | ============================================================================== | 0 | 400 848 | 133 0 0 nan | 0.000 % | ============================================================================== restarts : 1 conflicts : 0 (nan /sec) decisions : 44 (inf /sec) propagations : 144 (inf /sec) conflict literals : 0 ( nan % deleted) Memory used : 1.67 MB CPU time : 0 s SATISFIABLE
Copyright
Copyright (C) 2013, Wolfgang Scherer, <Wolfgang.Scherer@gmx.de>. See the document source for conditions of use under the GNU Free Documentation License.