From 4f436df9c1ed8c92803ac2d494f74239557364cf Mon Sep 17 00:00:00 2001 From: Hamed Gorjiara Date: Wed, 25 Jul 2018 19:19:22 -0700 Subject: [PATCH] Adding new encoding for nqueens (It has a bug) + code refactoring + Adding new Benchmark to Sudoku --- nqueens/nqueens.cc | 194 ++++++++++++++++++++- sudoku-csolver/problems/36x36-1000.problem | 36 ++++ 2 files changed, 224 insertions(+), 6 deletions(-) create mode 100644 sudoku-csolver/problems/36x36-1000.problem diff --git a/nqueens/nqueens.cc b/nqueens/nqueens.cc index d3317081..be0d6b25 100644 --- a/nqueens/nqueens.cc +++ b/nqueens/nqueens.cc @@ -9,6 +9,7 @@ #include "solver_interface.h" #include "csolver.h" #include "common.h" +#include using namespace std; @@ -42,6 +43,69 @@ void LessEqualOneToCNF(vector literals, vector< vector > & cnf){ } } +bool validateSolution(int N, int *table, int size){ + for(int k=0; k0){ + int row = k/N; + int col = k%N; + for (int j= row*N; j<(row+1)*N; j++) + if(j!=k && table[j] >0){ + return false; + } + for(int j=0; j0){ + return false; + } + } + + int i=row; + int j = col; + while( i>0 && j>0){ + int indx = i--*N+j--; + if(k!=indx && table[indx]>0){ + return false; + } + } + i=row; + j=col; + while(i>0 && j0){ + return false; + } + } + i=row; + j=col; + while(i0){ + int indx = i++*N+j--; + if(k!=indx && table[indx]>0){ + return false; + } + } + i=row; + j=col; + while(i0){ + return false; + } + } + + } + } + return true; +} + +void printValidationStatus(int N, int *table, int size){ + if(validateSolution(N, table, size)){ + printf("***CORRECT****\n"); + }else{ + printf("***WRONG******\n"); + } + +} + void printSolution(int N, int *table, int size){ for(int i=0; i 0){ @@ -135,6 +199,7 @@ void originalNqueensEncoding(int N){ break; case IS_SAT:{ printSolution(N, &solver->solution[1], solver->solutionsize); + printValidationStatus(N, &solver->solution[1], solver->solutionsize); break; } default: @@ -144,11 +209,8 @@ void originalNqueensEncoding(int N){ deleteIncrementalSolver(solver); } -void initializingElements(CSolver * solver, int N, vector &Xs, vector &Ys){ - -} -void csolverNQueens(int N){ +void csolverNQueensSub(int N){ CSolver *solver = new CSolver(); uint64_t domain[N]; for(int i=0; i &constraints){ + int size = constraints.size(); + if(size <1){ + return; + } else if(size ==1){ + solver->addConstraint(constraints[0]); + }else{ +// solver->addConstraint(solver->applyLogicalOperation(SATC_OR, &constraints[0], size)) + for(int i=0; iapplyLogicalOperation(SATC_NOT, constraints[i]); + BooleanEdge const2 = solver->applyLogicalOperation(SATC_NOT, constraints[j]); + BooleanEdge array[] = {const1, const2}; + solver->applyLogicalOperation(SATC_OR, (BooleanEdge *)array, 2); + } + } + + } +} + +void differentInEachRow(CSolver* solver, int N, vector &elems){ + Predicate *eq = solver->createPredicateOperator(SATC_EQUALS); + for(int i=0; iapplyPredicate(eq, inputs2, 2); + solver->addConstraint(solver->applyLogicalOperation(SATC_NOT, equals)); + } + } + + +} + +void diagonallyDifferentConstraint(CSolver *solver, int N, vector &elems){ + Predicate *eq = solver->createPredicateOperator(SATC_EQUALS); + for(int i=N-1; i>0; i--){ + cout << "i:" << i << "\t"; + vector diagonals; + for(int j=i; j>=0; j--){ + int index = i-j; + Element* e1 = elems[index]; + cout << "e" << e1 <<"=" << j << ", "; + Element* e2 = solver->getElementConst(2, (uint64_t) j); + Element* in[] = {e1, e2}; + BooleanEdge equals = solver->applyPredicate(eq, in, 2); + diagonals.push_back(equals); + + } + cout << endl; + atmostOneConstraint(solver, diagonals); + } + for(int i=1; i< N-1; i++){ + cout << "i:" << i << "\t"; + vector diagonals; + for(int j=i; jgetElementConst(2, (uint64_t) j); + Element* in[] = {e1, e2}; + BooleanEdge equals = solver->applyPredicate(eq, in, 2); + diagonals.push_back(equals); + + } + cout << endl; + atmostOneConstraint(solver, diagonals); + + } + +} + +void diagonallyDifferentConstraintBothDir(CSolver *solver, int N, vector &elems){ + diagonallyDifferentConstraint(solver, N, elems); + reverse(elems.begin(), elems.end()); + cout << "Other Diagonal:" << endl; + diagonallyDifferentConstraint(solver, N, elems); +} + + +void csolverNQueens(int N){ + if(N <=1){ + cout<<"Q" << endl; + return; + } + CSolver *solver = new CSolver(); + uint64_t domain[N]; + for(int i=0; icreateSet(1, domain, N); + vector elems; + for(int i=0; igetElementVar(domainSet)); + } + + differentInEachRow(solver, N, elems); + diagonallyDifferentConstraintBothDir(solver, N, elems); +// solver->serialize(); + if (solver->solve() != 1){ + printf("Problem is Unsolvable ...\n"); + }else { + int table[N*N]; + memset( table, 0, N*N*sizeof(int) ); + for(int i=0; igetElementValue(elems[i]); + printf("X=%d, Y=%d\n", x, i); + ASSERT(N*x+i < N*N); + table[N*x+i] = 1; + } + printSolution(N, table, N*N); + printValidationStatus(N, table, N*N); + } + delete solver; +} + + + int main(int argc, char * argv[]){ if(argc < 2){ - printf("Two arguments are needed\n./nqueen [-csolver]\n"); + printf("Two arguments are needed\n./nqueen [--csolver]\n"); exit(-1); } int N = atoi(argv[1]); if(argc <3){ printf("Running the original encoding ...\n"); originalNqueensEncoding(N); - }else if( strcmp( argv[2], "-csolver") == 0 ){ + }else if( strcmp( argv[2], "--csolver") == 0 ){ printf("Running the CSolver encoding ...\n"); csolverNQueens(N); } diff --git a/sudoku-csolver/problems/36x36-1000.problem b/sudoku-csolver/problems/36x36-1000.problem new file mode 100644 index 00000000..144d4e39 --- /dev/null +++ b/sudoku-csolver/problems/36x36-1000.problem @@ -0,0 +1,36 @@ +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 2.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 8.000000000000000000e+00 +0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 2.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+01 2.400000000000000000e+01 1.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+00 +0.000000000000000000e+00 2.200000000000000000e+01 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 8.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 0.000000000000000000e+00 7.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 4.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.600000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 3.600000000000000000e+01 1.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.300000000000000000e+01 1.800000000000000000e+01 1.200000000000000000e+01 2.200000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 9.000000000000000000e+00 +0.000000000000000000e+00 3.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 1.700000000000000000e+01 0.000000000000000000e+00 1.400000000000000000e+01 1.800000000000000000e+01 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.600000000000000000e+01 5.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.600000000000000000e+01 1.000000000000000000e+01 1.300000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 2.900000000000000000e+01 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 4.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 8.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 1.600000000000000000e+01 2.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.300000000000000000e+01 0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 3.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 9.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+01 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 1.900000000000000000e+01 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 6.000000000000000000e+00 5.000000000000000000e+00 +3.200000000000000000e+01 3.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 1.200000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 1.800000000000000000e+01 0.000000000000000000e+00 1.700000000000000000e+01 0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 2.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.300000000000000000e+01 0.000000000000000000e+00 1.100000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 1.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 2.600000000000000000e+01 0.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.500000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 0.000000000000000000e+00 1.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 2.300000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+01 +0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 3.600000000000000000e+01 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+00 +0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 8.000000000000000000e+00 4.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 1.800000000000000000e+01 1.100000000000000000e+01 0.000000000000000000e+00 1.300000000000000000e+01 1.700000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 9.000000000000000000e+00 0.000000000000000000e+00 1.600000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 2.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.300000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 2.600000000000000000e+01 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.500000000000000000e+01 +0.000000000000000000e+00 2.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 8.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.600000000000000000e+01 1.600000000000000000e+01 1.800000000000000000e+01 0.000000000000000000e+00 2.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 4.000000000000000000e+00 +0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 2.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 0.000000000000000000e+00 1.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 1.000000000000000000e+00 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 2.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.500000000000000000e+01 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 9.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.500000000000000000e+01 1.600000000000000000e+01 1.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 +0.000000000000000000e+00 1.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 6.000000000000000000e+00 3.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.600000000000000000e+01 0.000000000000000000e+00 3.400000000000000000e+01 +0.000000000000000000e+00 2.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.200000000000000000e+01 0.000000000000000000e+00 2.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 6.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 8.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 2.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 +0.000000000000000000e+00 2.700000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.000000000000000000e+01 1.400000000000000000e+01 0.000000000000000000e+00 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 1.600000000000000000e+01 0.000000000000000000e+00 2.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 2.400000000000000000e+01 2.900000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 3.600000000000000000e+01 1.100000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 7.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.100000000000000000e+01 0.000000000000000000e+00 2.800000000000000000e+01 +0.000000000000000000e+00 1.500000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 7.000000000000000000e+00 2.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 2.200000000000000000e+01 3.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.900000000000000000e+01 2.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.700000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.400000000000000000e+01 2.900000000000000000e+01 1.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.100000000000000000e+01 +0.000000000000000000e+00 7.000000000000000000e+00 3.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 5.000000000000000000e+00 0.000000000000000000e+00 2.300000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 8.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 3.600000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.900000000000000000e+01 +0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 2.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 1.300000000000000000e+01 3.400000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 1.800000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.200000000000000000e+01 0.000000000000000000e+00 3.000000000000000000e+01 0.000000000000000000e+00 0.000000000000000000e+00 0.000000000000000000e+00 3.600000000000000000e+01 -- 2.34.1