================================================================ reLOC 0.08-osaka : Multirobot SAT Solver (C) Copyright 2011-2013 Pavel Surynek ---------------------------------------------------------------- window size:64 Reading graph from input ... 1,0 3,0 2,1 4,1 4,3 5,3 6,4 6,5 7,6 Reading initial arrangement from input... Reading goal arrangement from input... Undirected graph: (|V|=8 |E|=9) [ Vertex: (id = 0) {1 3 } Vertex: (id = 1) {0 2 4 } Vertex: (id = 2) {1 } Vertex: (id = 3) {0 4 5 } Vertex: (id = 4) {1 3 6 } Vertex: (id = 5) {3 6 } Vertex: (id = 6) {4 5 7 } Vertex: (id = 7) {6 } Edge 0: 1 <-> 0 Edge 1: 3 <-> 0 Edge 2: 2 <-> 1 Edge 3: 4 <-> 1 Edge 4: 4 <-> 3 Edge 5: 5 <-> 3 Edge 6: 6 <-> 4 Edge 7: 6 <-> 5 Edge 8: 7 <-> 6 ] Robot arrangement: (|R| = 3, |V| = 8) [ robot locations: {1#1 2#2 3#5 } vertex occupancy: {0#0 1#1 2#2 0#3 0#4 3#5 0#6 0#7 } ] Robot arrangement: (|R| = 3, |V| = 8) [ robot locations: {1#5 2#4 3#2 } vertex occupancy: {0#0 0#1 3#2 0#3 2#4 1#5 0#6 0#7 } ] Unable to provide a new solution. Phase statistics (current phase = 'root_phase') [ Phase (name = 'root_phase') [ Total SAT solver calls = 0 Satisfiable SAT solver calls = 0 Unsatisfiable SAT solver calls = 0 Indeterminate SAT solver calls = 0 Move executions = 0 Produced CNF variables = 0 Produced CNF clauses = 0 Search steps = 0 Wall clock TIME (seconds) = 0.001 CPU/machine TIME (seconds) = 0.000 ] Sub-phases { Phase (name = 'WHCA*_solving') [ Total SAT solver calls = 0 Satisfiable SAT solver calls = 0 Unsatisfiable SAT solver calls = 0 Indeterminate SAT solver calls = 0 Move executions = 0 Produced CNF variables = 0 Produced CNF clauses = 0 Search steps = 3 Wall clock TIME (seconds) = 0.000 CPU/machine TIME (seconds) = 0.000 ] } ] ----------------------------------------------------------------