/* To compile you need the GNU Multiple precision libraries, available from http://www.swox.com/gmp then something like gcc -O3 -lgmp -o mult_circ multiplier_circuit.c */ #include #include #include #include #include /* ========================================================================================== CIRCUIT VARIABLES */ #define NEG(X) (-1*(X)) /* First Variable "1" is for TRUE/FALSE */ static long TRUE = 1; static long FALSE = -1; /* Variables are numbered as A - factor n bits B - factor n bits R - result 2n bits T - n temporary values of n bits (summands) C - n-1 carry bit values of n bits S - n-2 temporary values of n+1 bits (sums) */ /* Return the variable for the ith bit of the first multiplicand */ long A(int i, int n) { return ((long)i+(long)2); } /* Return the variable for the ith bit of the second multiplicand */ long B(int i, int n) { return (A(i,n)+(long)n); } /* Return the variable for the ith bit of the product of A and B */ long R(int i, int n) { return (B(i,n)+(long)n); } /* Return the variable for the ith bit of the jth row in the multiplication summands T[i] represents a copy of A when B[i] is 1, otherwise it is all 0's */ long C(int j, int i, int n) { return (R(i,n) + (long)(2*n) + (long)(j*n)); } /* Return the variable for the ith bit of the sum of the jth row and sum of everything above the jth row */ long S(int j, int i, int n) { return (C(n-1,i,n)+(long)(j*(n+1))); } /* Return the variable for the ith bit of the jth row in the multiplication summands T[i] represents a copy of A when B[i] is 1, otherwise it is all 0's */ long T(int j, int i, int n) { return (S(n-2,i,n)+(long)(j*n)); } /* ========================================================================================== CIRCUIT COMPONENTS */ void WriteUnit(FILE* problem, int a) { fprintf(problem,"%d 0\n", a); } /* for multiplication we need: iff a then c = b (a & b <=> c) (~a v ~b v c) && (~c v b) (~c v a) */ void Write_AandB_EQ_C(FILE* problem, int a, int b, int c) { fprintf(problem,"%d %d %d 0\n", NEG(a), NEG(b), c); fprintf(problem,"%d %d 0\n", a, NEG(c)); fprintf(problem,"%d %d 0\n", b, NEG(c)); } void Write_A_EQ_B(FILE* problem, int a, int b) { fprintf(problem,"%d %d 0\n", b, NEG(a)); fprintf(problem,"%d %d 0\n", a, NEG(b)); } /* A mul bit full adder is a full adder when the multiplication bit, "a", is true, to give the result for ax + y, however a vector operation aX is assumed to take place, thus all carry bits are forced to zero when "a" is zero. The circuit implements the adder when "a" is true, correctly passes the sum on when "a" is false. The adder is made from cnf clauses for a full adder. Variable parameters denote the inputs and outputs. Read the following truth table cases as inputs --> output, therefore (NEG(inputs) OR output) is the clause that covers the case. x y c-in | c-out s ------------------ 0 0 0 | 0 0 0 0 1 | 0 1 0 1 0 | 0 1 0 1 1 | 1 0 1 0 0 | 0 1 1 0 1 | 1 0 1 1 0 | 1 0 1 1 1 | 1 1 */ void WriteMulBitFullAdder(FILE* problem, int a, int x, int y, int c_in, int sum, int c_out) { assert(problem); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, y, c_in, NEG(c_out)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, y, c_in, NEG(sum)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, y, NEG(c_in), NEG(c_out)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, y, NEG(c_in), sum); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, NEG(y), c_in, NEG(c_out)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, NEG(y), c_in, sum); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, NEG(y), NEG(c_in), c_out); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), x, NEG(y), NEG(c_in), NEG(sum)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), y, c_in, NEG(c_out)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), y, c_in, sum); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), y, NEG(c_in), c_out); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), y, NEG(c_in), NEG(sum)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), NEG(y), c_in, c_out); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), NEG(y), c_in, NEG(sum)); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), NEG(y), NEG(c_in), c_out); fprintf(problem,"%d %d %d %d %d 0\n", NEG(a), NEG(x), NEG(y), NEG(c_in), sum); //These two lines aren't strictly necessary fprintf(problem,"%d %d 0\n", a, NEG(c_in)); fprintf(problem,"%d %d 0\n", a, NEG(c_out)); fprintf(problem,"%d %d %d 0\n", a, NEG(y), sum); fprintf(problem,"%d %d %d 0\n", a, y, NEG(sum)); } /* ========================================================================================== DIMACS INSTANCE GENERATION */ void WriteDIMACSHeader(FILE* problem, int n) { int v,c; assert(n>1); fprintf(problem,"c Composite (Restricted): are there two n-bit factors A and B whose product is the input C\n"); fprintf(problem,"c Multiplication of 2 n bit numbers to produce a given 2n bit number.\n"); fprintf(problem,"c Encode (decode) source code from http://web.rsise.anu.edu.au/~andrews/composite .\n"); fprintf(problem,"c Variable 1 is a constant for True \n",n,A(0,n),A(n-1,n)); fprintf(problem,"c Factor A is %d bits in vars %d to %d\n",n,A(0,n),A(n-1,n)); fprintf(problem,"c Factor B is %d bits in vars %d to %d\n",n,B(0,n),B(n-1,n)); fprintf(problem,"c Product R is %d bits in vars %d to %d\n",2*n,R(0,n),R(2*n-1,n)); //fprintf(problem,"c The %d intermediate summands T are %d bits in vars %d to %d\n",n,n,T(0,0,n),T(n-1,n-1,n)); fprintf(problem,"c The %d carry bit vectors C are %d bits in vars %d to %d\n",n-1,n,C(0,0,n),C(n-2,n-1,n)); fprintf(problem,"c The %d intermediate sums S are %d bits in vars %d to %d\n",n-2,n+1,S(0,0,n),S(n-3,n,n)); v = 1 + n + n + 2*n + (n-1)*n + (n-2)*(n+1); //= 2n^2 + 2n - 1 fprintf(problem,"c Total of %d vars\n",v,S(n-2,0,n)); // c = specify (n-1) add ops + 2n constants for setting the product // Each ad op is 2 eqs + n WFA's for first two rows c = 2*n + (4 + n*20) + (n-2)*(3+n*20); fprintf(problem,"c Total of %d clauses.\n",c); fprintf(problem,"p cnf %d %d\n",v,c); //Constant for TRUE fprintf(problem, "1 0\n"); } /* Generate the basic circuit for a multiplication of two numbers of size "n" bits. */ void WriteDIMACSBody_Multiplier(FILE* problemfile, unsigned int n) { int row, col; //Generate the summands: if A[i] then T[i] = B /* for (row=0;row>1, and where R[0]=T[0][0] //Then for i= 1 to n-3, S[i] = T[i+1] + S[i]>>1 , and where R[i]=S[i][0] //Then R[2n-1]..R[n-1] = T[n-1]<<1 + S[n-2], noting that R[n-1]=S[n-2][0] //assume A and B are odd and thus so is input R WriteUnit(problemfile, A(0,n)); WriteUnit(problemfile, B(0,n)); WriteUnit(problemfile, NEG(C(0,0,n)));//rightmost carries are all false //Note we take advantage of A(0) being true for (col=0;col-1;--i){ if (rBits[i] == '1') { fprintf(problemfile, "%d 0\n",R((2*n-1)-i,n)); } else { fprintf(problemfile, "%d 0\n",-1*R((2*n-1)-i,n)); } } } void WriteProblem(char* filename, char* rBits, unsigned int n) { FILE* problemfile; if (!(problemfile = fopen(filename,"w"))) { fprintf(stderr,"Can't open output file %s for writing.\n",filename); exit(0); } //we assume there are at least 2 separate vector addition operations: the starting point and //the final result therefore n should be greater than 2 assert(n>2); WriteDIMACSHeader(problemfile, n); WriteDIMACSBody_Multiplier(problemfile, n); WriteDIMACSBody_Result(problemfile, rBits, n); } /* ========================================================================================== POST TEST SOLUTION INPUT Solution file should contain a list of (signed) integers 1 to v, where v is the number of variables in the problem. The variables are considered false if negative, true if positive. */ void CheckSol(char *filename) { FILE* solfile; int i,buf; int v=0; int numbits; char *abits; char *bbits; char *rbits; mpz_t aval; mpz_t bval; mpz_t rval; mpz_t cval; mpz_init(aval); mpz_init(bval); mpz_init(rval); mpz_init(cval); if (!(solfile = fopen(filename,"r"))) { fprintf(stderr,"Can't open solution file %s for reading.\n",filename); exit(0); } while (fscanf(solfile,"%d",&buf)==1){ v++; } rewind(solfile); numbits = ((int)sqrt((double)(4 + (8*(v+1)) )) - 2)/4; printf("Number of Bits in Products is %d\n",numbits); abits = malloc(sizeof(char)*numbits+1); bbits = malloc(sizeof(char)*numbits+1); rbits = malloc(sizeof(char)*2*numbits+1); fscanf(solfile,"%d",&buf);//scan over initial constant for (i =1;i<=numbits;++i){ fscanf(solfile,"%d",&buf); abits[numbits-i] = (buf > 0)?'1':'0'; } abits[numbits]=0; for (i =1;i<=numbits;++i){ fscanf(solfile,"%d",&buf); bbits[numbits-i] = (buf > 0)?'1':'0'; } bbits[numbits]=0; for (i =1;i<=(2*numbits);++i){ fscanf(solfile,"%d",&buf); rbits[(2*numbits)-i] = (buf > 0)?'1':'0'; } rbits[2*numbits]=0; mpz_set_str(aval,abits,2); mpz_set_str(bval,bbits,2); mpz_set_str(rval,rbits,2); printf("Assuming the file product is correct, the two calculations should agree.\n"); printf("File : "); mpz_out_str(stdout,10,aval); printf(" * "); mpz_out_str(stdout,10,bval); printf(" = "); mpz_out_str(stdout,10,rval); printf("\n"); mpz_mul(cval,aval,bval); printf("Multiply File factors: "); mpz_out_str(stdout,10,aval); printf(" * "); mpz_out_str(stdout,10,bval); printf(" = "); mpz_out_str(stdout,10,cval); printf("\n"); (mpz_cmp(rval,cval)==0)?printf("OK\n"):printf("FAIL!!!!!\n"); mpz_clear(aval);mpz_clear(bval);mpz_clear(rval);mpz_clear(cval); free(abits); free(bbits); free(rbits); } /* ========================================================================================== TEST GENERATION ROUTINES AND MAIN Most of the test routine code was generated by another program. */ void some_tests(); void simple_tests(); void SAT2004tests(); int main(int argc, char **argv) { if (argc == 2){ printf("Checking solution in %s\n",argv[1]); CheckSol(argv[1]); } //some_tests(); //simple_tests(); //SAT2004tests(); //super_huge(); } void some_tests() { //7*7=49 WriteProblem("test1.cnf", "110001", 3); //23*29 WriteProblem("test2.cnf", "1010011011", 5); //227*241 WriteProblem("test3.cnf", "1101010110110011", 8); //149*131 WriteProblem("test4.cnf", "0100110000111111", 8); //7*5=35 WriteProblem("test5.cnf", "100011", 3); //5*5=25 WriteProblem("test6.cnf", "011001", 3); //3*5=25 WriteProblem("test7.cnf", "001111", 3); //60127*36209 WriteProblem("test16.cnf", "10000001110001000111111101101111", 16); //73847*87317 WriteProblem("test17.cnf", "0110000000010101100010110011000011", 17); WriteProblem("test33.cnf", "011011110010111011000000111000100101001100101111111111011011101011", 33); WriteProblem("test24.cnf", "011101111110001110110111011001111001110010010101", 24); } void super_huge() { char *huge1 = "11000010110010111011001001001111110110111111100100100011101101100001\ 00100110100011100011111100010001101000111000100101101101111001000101\ 01110100101100111011101001011000011100110000110010111101011001010010\ 10010011100010000110010011100010001000100011111011101110101101110000\ 01001010000101111100111111010000100011010001011010110100011010001001\ 00011010011000010100011101000111010110011001001110011100011011100100\ 10011010101011111110011111110010010110010101010101001000110001110100\ 11000001110101111111101110001101001001001100110100010101110010110010\ 00111011010011001101000010100011"; WriteProblem("Composite288BitPrimes-0.cnf", huge1, 288); char *huge2 = "10101110010110111011010011110010011001100000000000110010010110011100\ 11111001101001101111010100100001110000111100000000110100000100000001\ 01110110110011110001011011011111010100111001010100110100011101101110\ 10101110001110110010000111101101111001101100001111000111101100000011\ 10111101110010100010000010110011000111000000000001100111111111111010\ 01111001011111100100111010010001000001011001011110000111001111101110\ 11110001000100111010011000001111111011001100110110010101110111101011\ 01011011001010111111000100000000011001101011111000100010001001001010\ 11001110001010011101010100110010110111000000101101011010011101001101\ 0010110100000000011011110001"; WriteProblem("Composite320BitPrimes-0.cnf", huge2, 320); } void simple_tests() { //57259*38933 WriteProblem("Composite016BitPrimes-0.cnf", "10000100110111111110000100000111", 16); //47881*65027 WriteProblem("Composite016BitPrimes-1.cnf", "10111001100101010001111100011011", 16); //50261*37423 WriteProblem("Composite016BitPrimes-2.cnf", "01110000000111001000010110011011", 16); //61331*33569 WriteProblem("Composite016BitPrimes-3.cnf", "01111010101101110001101011110011", 16); //40577*50833 WriteProblem("Composite016BitPrimes-4.cnf", "01111010111100011000110100010001", 16); //56873*58111 WriteProblem("Composite016BitPrimes-5.cnf", "11000100111111010111110011010111", 16); //56087*55343 WriteProblem("Composite016BitPrimes-6.cnf", "10111001000000111010000100111001", 16); //61441*35507 WriteProblem("Composite016BitPrimes-7.cnf", "10000010000010000101101010110011", 16); //42221*39229 WriteProblem("Composite016BitPrimes-8.cnf", "01100010101110001111000101111001", 16); //48947*34123 WriteProblem("Composite016BitPrimes-9.cnf", "01100011100011011000001011110001", 16); //198859*131939 WriteProblem("Composite018BitPrimes-0.cnf", "011000011011110111001100011110000001", 18); //174767*176857 WriteProblem("Composite018BitPrimes-1.cnf", "011100110010010011100101110001010111", 18); //246527*140867 WriteProblem("Composite018BitPrimes-2.cnf", "100000010101111010111110001010111101", 18); //220931*205949 WriteProblem("Composite018BitPrimes-3.cnf", "101010011000000010101101000001110111", 18); //169991*183307 WriteProblem("Composite018BitPrimes-4.cnf", "011101000001010100000001110001001101", 18); //216761*143567 WriteProblem("Composite018BitPrimes-5.cnf", "011100111110111000010101011110010111", 18); //194687*170711 WriteProblem("Composite018BitPrimes-6.cnf", "011110111100111110010001100010101001", 18); //158371*148157 WriteProblem("Composite018BitPrimes-7.cnf", "010101110110100011001100000001010111", 18); //245561*234967 WriteProblem("Composite018BitPrimes-8.cnf", "110101101111000111001100010111011111", 18); //193799*206027 WriteProblem("Composite018BitPrimes-9.cnf", "100101001011111000100100100010001101", 18); //726589*770311 WriteProblem("Composite020BitPrimes-0.cnf", "1000001001010000101100001001100010101011", 20); //667531*749467 WriteProblem("Composite020BitPrimes-1.cnf", "0111010001111011110000010000111000101001", 20); //875969*547577 WriteProblem("Composite020BitPrimes-2.cnf", "0110111110101101111111100000101010111001", 20); //629803*924751 WriteProblem("Composite020BitPrimes-3.cnf", "1000011110011010011001011110010101000101", 20); //699373*748249 WriteProblem("Composite020BitPrimes-4.cnf", "0111100111010111011010101101110111100101", 20); //711539*847157 WriteProblem("Composite020BitPrimes-5.cnf", "1000110001011000110011001110010111001111", 20); //725009*943567 WriteProblem("Composite020BitPrimes-6.cnf", "1001111101000111001101101011001010111111", 20); //1039349*849427 WriteProblem("Composite020BitPrimes-7.cnf", "1100110110001110000001101100000100101111", 20); //540751*657079 WriteProblem("Composite020BitPrimes-8.cnf", "0101001010111010011111011101001001111001", 20); //988231*762547 WriteProblem("Composite020BitPrimes-9.cnf", "1010111101110100011011010001101110100101", 20); //4110527*3450869 WriteProblem("Composite022BitPrimes-0.cnf", "11001110011010101101010101110110011111001011", 22); //2429729*2519603 WriteProblem("Composite022BitPrimes-1.cnf", "01011001000101100000110011011000000110010011", 22); //3195487*2549311 WriteProblem("Composite022BitPrimes-2.cnf", "01110110100010110100101110110010111101100001", 22); //3095341*2575021 WriteProblem("Composite022BitPrimes-3.cnf", "01110011111111001010111000001111111101101001", 22); //2844641*3918067 WriteProblem("Composite022BitPrimes-4.cnf", "10100010001100000011001101100110001010010011", 22); //2638849*2623087 WriteProblem("Composite022BitPrimes-5.cnf", "01100100101110100011001101011000001001101111", 22); //3644959*3653687 WriteProblem("Composite022BitPrimes-6.cnf", "11000001110010111011001100110011100010101001", 22); //4190009*3597437 WriteProblem("Composite022BitPrimes-7.cnf", "11011011010110000110010011001001001011010101", 22); //3810557*2577989 WriteProblem("Composite022BitPrimes-8.cnf", "10001110111100111010101000111111011000110001", 22); //2973559*2914183 WriteProblem("Composite022BitPrimes-9.cnf", "01111110000110010111110000011010100011000001", 22); //14515243*13277101 WriteProblem("Composite024BitPrimes-0.cnf", "101011110100011100110011110110000100011000001111", 24); //10365049*11404741 WriteProblem("Composite024BitPrimes-1.cnf", "011010111000001100010010101111011000001000011101", 24); //9628793*10725647 WriteProblem("Composite024BitPrimes-2.cnf", "010111011110110110010111110000101011110000010111", 24); //9705859*9509191 WriteProblem("Composite024BitPrimes-3.cnf", "010100111111000100010010110000111101111001010101", 24); //13260479*14127941 WriteProblem("Composite024BitPrimes-4.cnf", "101010100110001101000000110000100000111001111011", 24); //12329393*12603127 WriteProblem("Composite024BitPrimes-5.cnf", "100011010101001101001100100010000110111111000111", 24); //10647523*9549499 WriteProblem("Composite024BitPrimes-6.cnf", "010111000111100111011111011110111111010011010001", 24); //10908617*9918163 WriteProblem("Composite024BitPrimes-7.cnf", "011000100110011010111111101001011111010010101011", 24); //11623769*16262093 WriteProblem("Composite024BitPrimes-8.cnf", "101010111110101100111100000000101110101101000101", 24); //14643533*10688753 WriteProblem("Composite024BitPrimes-9.cnf", "100011100101101011101000111111111110000101111101", 24); } void SAT2004tests() { //13775107*10436989 WriteProblem("Composite-024BitPrimes-0.cnf", "100000101100001000110101111100001011000101110111", 24); //11202097*11963177 WriteProblem("Composite-024BitPrimes-1.cnf", "011110011110001001000001100010101100000011011001", 24); //9209531*11891323 WriteProblem("Composite-024BitPrimes-2.cnf", "011000111001101000011001101110110000000111011001", 24); //13441009*10830301 WriteProblem("Composite-024BitPrimes-3.cnf", "100001000110010100110010011101101101110000001101", 24); //14868547*13001557 WriteProblem("Composite-024BitPrimes-4.cnf", "101011111101000101111011111000000101111100111111", 24); //15373829*8535469 WriteProblem("Composite-024BitPrimes-5.cnf", "011101110101100010110010110100001001001001100001", 24); //11046143*13259999 WriteProblem("Composite-024BitPrimes-6.cnf", "100001010011011100100010010011000111111000100001", 24); //12813413*8901923 WriteProblem("Composite-024BitPrimes-7.cnf", "011001111011110110011001001001100010001011001111", 24); //9977819*13022267 WriteProblem("Composite-024BitPrimes-8.cnf", "011101100010110010010011010111101011001101111001", 24); //14486513*15453121 WriteProblem("Composite-024BitPrimes-9.cnf", "110010111001100111100101010110010001101110110001", 24); //3207921401*2908343093 WriteProblem("Composite-032BitPrimes-0.cnf", "1000000101111001111000011000000110000101101110010011110010001101", 32); //3890562131*3762706531 WriteProblem("Composite-032BitPrimes-1.cnf", "1100101100101000010101001000100111001011110101111111010000011001", 32); //3689946049*3266129599 WriteProblem("Composite-032BitPrimes-2.cnf", "1010011101000000101111100111010001000000100011100110001011111111", 32); //2364693433*3906760859 WriteProblem("Composite-032BitPrimes-3.cnf", "1000000000110101000000010110010111011001110110100111100100000011", 32); //3721043357*2665264193 WriteProblem("Composite-032BitPrimes-4.cnf", "1000100110100010010000111001000100100000001100000110100011011101", 32); //2649388999*3519973621 WriteProblem("Composite-032BitPrimes-5.cnf", "1000000101101011110100101111000110001010001010000101100101110011", 32); //3769792111*4216782943 WriteProblem("Composite-032BitPrimes-6.cnf", "1101110010011011010101110001100001110110111100101111001100110001", 32); //2390689909*3180528643 WriteProblem("Composite-032BitPrimes-7.cnf", "0110100110000101100111100110101111100011110011011110110101011111", 32); //2272574219*3506915773 WriteProblem("Composite-032BitPrimes-8.cnf", "0110111010011010001001111110100101100010110100010011101000011111", 32); //2995575179*2960011009 WriteProblem("Composite-032BitPrimes-9.cnf", "0111101100001101101011101101110110011000001101110101111010001011", 32); //251831384682113*213502101384269 WriteProblem("Composite-048BitPrimes-0.cnf", "101011011011101010100001100011100001110111110110000001010000001110010100100001110110100011001101", 48); //236353270130423*172289727066913 WriteProblem("Composite-048BitPrimes-1.cnf", "100000111001001111010010000100011000001111110000110101010000101101110101100011000111101011010111", 48); //185594098391887*146532223517111 WriteProblem("Composite-048BitPrimes-2.cnf", "010101111101111110011010011111111000010101100000001100000001111110001010101000101101010001111001", 48); //262526825896583*268408591506191 WriteProblem("Composite-048BitPrimes-3.cnf", "111000111010111011010100110111101010111001011000111001001000111111001000001101000000101011101001", 48); //209984798484847*141100205547199 WriteProblem("Composite-048BitPrimes-4.cnf", "010111111011110001110011001111110101101110000000001110101010110111101100101001101010101111010001", 48); //237389811289349*160313366720597 WriteProblem("Composite-048BitPrimes-5.cnf", "011110101111011111010000010111101001100111101100101011101111101111010100001101011100001010101001", 48); //170398907512879*247585420075417 WriteProblem("Composite-048BitPrimes-6.cnf", "100010000101000101010100110111011100011101001110100000111111110010000110110110011110001100010111", 48); //243669948699797*219769209125819 WriteProblem("Composite-048BitPrimes-7.cnf", "101011010000100001111001100000100010111101011011101001100000011110000111101110101001111111010111", 48); //270196293072037*207432624314411 WriteProblem("Composite-048BitPrimes-8.cnf", "101101010001100101101101010100001101000111001111001101010000011101001001001011010000111110110111", 48); //185752395564487*162254261925149 WriteProblem("Composite-048BitPrimes-9.cnf", "011000010110001001111110011101000001110111011110100000010001000100001101010001001001101010001011", 48); //12380864347663953329*17846289558156280691 WriteProblem("Composite-064BitPrimes-0.cnf", "10100110001110011110011011010101111110101101000110010001110011111001101010111111101110100001100100000000111110001101100110000011", 64); //11750051364013096481*13227528431279206997 WriteProblem("Composite-064BitPrimes-1.cnf", "01110100111011011001100110101001010001100011000001100001111010001111010010111100001010110000000000000000110011011101001011110101", 64); //15138872185407589121*14491174817266966201 WriteProblem("Composite-064BitPrimes-2.cnf", "10100101000010110000111100111001101010101110101111000000010010111000001010001100010011011010000011101001110101110101000110111001", 64); //9417466978216143599*12969534641766215939 WriteProblem("Composite-064BitPrimes-3.cnf", "01011011111000110101011100001000000011111100101101011001111110010111010101010001010111111010100011110001111100001111111111001101", 64); //11059688640408220451*15255916104800820811 WriteProblem("Composite-064BitPrimes-4.cnf", "01111110111011110110001001100100010101001100100100010100011001101101110101001001010111001010011001100000010101001001010101000001", 64); //12521446321409629231*12443568359592696119 WriteProblem("Composite-064BitPrimes-5.cnf", "01110101001110000011001010111101011101000000110001011110011000011111111111101001001001010010000110000111110010001010010100011001", 64); //15035135756201353801*12011219235841453363 WriteProblem("Composite-064BitPrimes-6.cnf", "10000111110111000110110111001101100011101000100010000110000101000011100101010010011011100010001100100110011110111110100110001011", 64); //17727686155806616709*18069976461629906249 WriteProblem("Composite-064BitPrimes-7.cnf", "11110000111111110000010111000011000100101000110110110000110010110111101110010111111000011010000011111101010111000000001011101101", 64); //14323289712840599507*10971607184129888167 WriteProblem("Composite-064BitPrimes-8.cnf", "01110110001110011110010011110110001000101001010000001101100000111100010100011100000101101011101011001011101001010001011110100101", 64); //15290017099012968971*13629748433968282223 WriteProblem("Composite-064BitPrimes-9.cnf", "10011100110010000011010001000001110001100011000001011000000110001111011101010000111001010000010000011111000000011101000011000101", 64); //45104976240411944596356961633*65052912923454776627543511673 WriteProblem("Composite-096BitPrimes-0.cnf", "011101111010101010010101001011110111000010010000100100101111001001011110010001110101111100001011001001011000100000100000110101111110101010100011100001111011101000100000000010111110110011011001", 96); //42180980935522011866949042253*62171680235219115890267707157 WriteProblem("Composite-096BitPrimes-1.cnf", "011010101111001111001001000111001111110100101110001001000101000010011010100111100001000110011011001101010111110001111110010001101100111011001110111100101110100000110010001001101111000101010001", 96); //45990650507572218555831689143*64925308113181047927772021693 WriteProblem("Composite-096BitPrimes-2.cnf", "011110011100011011011000111010001001000111000111110001011010001010100010110011101101001000110111110111111111100100111111011001011001110010010111101000110001011001001100100011101000111100011011", 96); //44265589964789819309493092183*55899607424859342739654425749 WriteProblem("Composite-096BitPrimes-3.cnf", "011001001110101000111110110001111010111011010110010111001111100010110101101100010001001010000010010001110011110100110011101110011101101000101000000101000010100010011001100100010000000110100011", 96); //41078618104173950180451135787*50164434711602793100424446447 WriteProblem("Composite-096BitPrimes-4.cnf", "010101000000101010001111111001100101011011001110111000011100000111001011001000001000111111010001010011110011011010000101011101110101010101110000100101010010101010001101101111001001001000100101", 96); //55665955431654807483158403119*48688400769399429321496179697 WriteProblem("Composite-096BitPrimes-5.cnf", "011011101000100010110101101101000000011001100010011101100111111100000101011001101011101011000110101010001010010011010000010011110001001011010010000101010100110001000111101001010010000100111111", 96); //50781300698869083728155214809*75422259980585544762440016647 WriteProblem("Composite-096BitPrimes-6.cnf", "100111000011001101111100111111010010110011111000011100101001100010110001000001001110101110111010110001110111011100001111011011111011010001100100111111101001010000001010111001010000010111101111", 96); //76762489618594715428888175483*48949755492661828548882582641 WriteProblem("Composite-096BitPrimes-7.cnf", "100110010011111000101111000001100000001110101011000100000110101100101001101010001101101001001110000001100110001110110101001101111101000101001110000010101011011111101110110011010110110101001011", 96); //60899881211795443290487585763*71650258060269742658080889021 WriteProblem("Composite-096BitPrimes-8.cnf", "101100011111010011111011111110100011011001001000001111101000110101011110100001011111000011111001011111100001001001111001111111110001100000000101010011001100011010000100100101111111111010010111", 96); //44927020372448993517592669349*50965757093946719726310203977 WriteProblem("Composite-096BitPrimes-9.cnf", "010111010110000111111111001101111011001100011111100110010000100111010000001111110101000111100101011111111000000010101010010111101101101101011011001001000010010000111101011011111110010100001101", 96); } void test_SAT2004tests() { //13453763*13947743 WriteProblem("Composite-024BitPrimes-0.cnf", "101010101010101010010101011101100001100001011101", 24); //15537343*14823071 WriteProblem("Composite-024BitPrimes-1.cnf", "110100010111011101111101100110000011010010100001", 24); //14084233*15811339 WriteProblem("Composite-024BitPrimes-2.cnf", "110010101000100100110001000100001101100011100011", 24); //13929049*15394823 WriteProblem("Composite-024BitPrimes-3.cnf", "110000110000011100011000100010100111000001101111", 24); //9891131*11157403 WriteProblem("Composite-024BitPrimes-4.cnf", "011001000101111100001000111100010010011110111001", 24); //9040529*14177063 WriteProblem("Composite-024BitPrimes-5.cnf", "011101001001000101111001000000001111011100010111", 24); //9027427*12142397 WriteProblem("Composite-024BitPrimes-6.cnf", "011000111011000110100011011100100000111110010111", 24); //11902823*13527463 WriteProblem("Composite-024BitPrimes-7.cnf", "100100100111000100111001101111100011101100110001", 24); //15760249*11853731 WriteProblem("Composite-024BitPrimes-8.cnf", "101010011110100011100101110000010000010100001011", 24); //10042861*13215221 WriteProblem("Composite-024BitPrimes-9.cnf", "011110001011010011110110101001110000010011010001", 24); //3547987483*2476690943 WriteProblem("Composite-032BitPrimes-0.cnf", "0111100111110010101001100001110010101011101101110011101111100101", 32); //2803061617*2550464863 WriteProblem("Composite-032BitPrimes-1.cnf", "0110001100110110101111011101000011001100101101000110011111101111", 32); //2169364933*2347253803 WriteProblem("Composite-032BitPrimes-2.cnf", "0100011010101010100110001001001111000010000011100010110000010111", 32); //4007197879*2197814527 WriteProblem("Composite-032BitPrimes-3.cnf", "0111101000111001000001101000010000101011001100001101111001001001", 32); //3202508167*2290190029 WriteProblem("Composite-032BitPrimes-4.cnf", "0110010111001000110110101000100000111101011101101111011100011011", 32); //2208972083*2265571159 WriteProblem("Composite-032BitPrimes-5.cnf", "0100010101110011110110100010000000010101111101010011100101010101", 32); //2306436229*3920776291 WriteProblem("Composite-032BitPrimes-6.cnf", "0111110101111111010000110011011110110111101001100111001101101111", 32); //3189083437*2962815391 WriteProblem("Composite-032BitPrimes-7.cnf", "1000001100100000011001110011001111001000011010110111001111110011", 32); //4285720091*2861107169 WriteProblem("Composite-032BitPrimes-8.cnf", "1010101000101011000010010010011110111010101110011111101010111011", 32); //2478476549*2250876281 WriteProblem("Composite-032BitPrimes-9.cnf", "0100110101101011101011100010111001000011110111011110000001011101", 32); //208278765074351*245539711509667 WriteProblem("Composite-048BitPrimes-0.cnf", "101001010011111010011010001000011101011000010111010101000100010101011111011011101001000001101101", 48); //162055270360427*247106263748849 WriteProblem("Composite-048BitPrimes-1.cnf", "100000010110010001010111100100011000101010111111011011001001001101111010000111000010100110111011", 48); //162583683334937*200880838200787 WriteProblem("Composite-048BitPrimes-2.cnf", "011010011000011110101100101101000001100001011011111111011000110011110010011000001001001010011011", 48); //271360297719029*240609840170387 WriteProblem("Composite-048BitPrimes-3.cnf", "110100101111100000111101111000000000100000110100010010101100011000100101011000001001000110101111", 48); //222523869521267*194329871549497 WriteProblem("Composite-048BitPrimes-4.cnf", "100010111011100111001100110101111000110011110011110100111011110010011010000010011110001010011011", 48); //281104938185389*197718063849301 WriteProblem("Composite-048BitPrimes-5.cnf", "101100111001011001001110000001111010001111111101011010110110000011011101000111011100011001110001", 48); //202651185245813*144518001669397 WriteProblem("Composite-048BitPrimes-6.cnf", "010111101010000101101101010101110100000011111001100010011101110010101011010011001100100010011001", 48); //216975300699853*196307911325231 WriteProblem("Composite-048BitPrimes-7.cnf", "100010011010000011100111100101001101111110011111101100011110001010100001110101110101110110100011", 48); //264354127717259*177131193332777 WriteProblem("Composite-048BitPrimes-8.cnf", "100101110100110100001000000111100001010101010000010010101111110111010101111111100010110101000011", 48); //212358763038503*231797632161041 WriteProblem("Composite-048BitPrimes-9.cnf", "100111110000110101011010001011010000100011010110010101010011011011110110010110010010110010010111", 48); //17780310699444115483*14318527578836154481 WriteProblem("Composite-064BitPrimes-0.cnf", "10111111100001111101011100001110001001110101111111110110111100101010111010011010000101010011011100010000110010101000101111101011", 64); //12381756054635361671*14487961813238784769 WriteProblem("Composite-064BitPrimes-1.cnf", "10000110111101001001000011001110100011010101110011010011110001000011001010001011110001010000100100000111010011010010101010000111", 64); //15241587579502977107*12540351854160349151 WriteProblem("Composite-064BitPrimes-2.cnf", "10001111110010110011110010110110011111110001110101101101001000011111010001101100101010100010011011000100110000010010110101001101", 64); //16154324979006673681*18053258793243329801 WriteProblem("Composite-064BitPrimes-3.cnf", "11011011011001110111100111011110110010100101100001100001010111111001101001011001010010101001111100101001110000001100000010011001", 64); //15349872801085286677*17436433507412786687 WriteProblem("Composite-064BitPrimes-4.cnf", "11001001010110101111000110110111001011001100101101100010010011101001111111001000110000011001101011000100000001010010110011101011", 64); //18342258723008111891*11887551655160720887 WriteProblem("Composite-064BitPrimes-5.cnf", "10100100000010011101101000111000110000000111000011010111001011001100001011101011100011001100111100110101100010101101110001010101", 64); //11339018897491015529*10702883236458462671 WriteProblem("Composite-064BitPrimes-6.cnf", "01011011010011010001111110011000000011001011001001001100000001100000010010001000000010110100100101010001001110010001001011100111", 64); //14100805044007404211*15213177145357302211 WriteProblem("Composite-064BitPrimes-7.cnf", "10100001011000101010110000110010111110011010011111000100110001111100111011010100110001001000101010110001010000010010100101011001", 64); //16773442347614892791*15279710259420734161 WriteProblem("Composite-064BitPrimes-8.cnf", "11000000110100000100110100111000000100000101011110111000100000101100011110100001111100101101110100110010111111001010100110100111", 64); //12011790801578749553*10198113470177769151 WriteProblem("Composite-064BitPrimes-9.cnf", "01011100001010000010111001000000010101011100000100111111001000001101011111101101101010101111111011110110011001001111110001001111", 64); //63647199100157892952616971193*42471275377870823461586751127 WriteProblem("Composite-096BitPrimes-0.cnf", "011011100011111001111110000000111110000101100111111000011111000010111111011000111100101010100101010110010100000011010111001001011111111100111000111100010000010100110110110100101010100000011111", 96); //52660636110758811429242464513*50777709398871440678331629453 WriteProblem("Composite-096BitPrimes-1.cnf", "011011010000110110111000101100010000011001000111011111000111111000100011101000101100100110001001000100001010110110000000111110110110010101001011011001011010001001111001110011111001010010001101", 96); //77596362154639774775064500287*74100459610531133089599836357 WriteProblem("Composite-096BitPrimes-2.cnf", "111010101000000000000111100100001010100110010000101100101110010000101000111011100000010100000100111001101001111001010111001001011010011010000111000111000011011110101100110110000101100001111011", 96); //64696861274062369773383368957*61329899692425451601838921901 WriteProblem("Composite-096BitPrimes-3.cnf", "101000011101001001001110110101010101111101001101000011001001011101100001000000100101111011011100111010010000110100101011100000011000110110111111100000000001110001010001001011011110001011111001", 96); //54228481858725522102474322751*50189997392106799790910548821 WriteProblem("Composite-096BitPrimes-4.cnf", "011011110000000000101000110110001011010000100011010101010111111111111100001010111000011001011000101001101100010100100100101111100011100011110010000111110000000101111010101101101001100011101011", 96); //62538422585483194546417316737*67210554311220683214708274213 WriteProblem("Composite-096BitPrimes-5.cnf", "101010110110101111100101000000110101101111100011001010100101111011101110100000010011010010110001110010010111010001011100000010011011000001110001101101010001101010011010010011010110010110100101", 96); //72451898444486503852182630761*61119089759061780343381896457 WriteProblem("Composite-096BitPrimes-6.cnf", "101101001001100010000000111000001011011110111110100010101010111000011111010100001011011010001100000111111100010111010100110001000001110110101010010100010010111101111111001111000111000110110001", 96); //40272569228564311734762135127*65848380454443854030341794493 WriteProblem("Composite-096BitPrimes-7.cnf", "011011000010011011110100100001110100000101110001110110111001110000010000110011100001101110001111011010000011111001111101011000100110000100101101010001111100100110011001000011101010110000111011", 96); //39633234136547892674942690947*75252065846772373812944890963 WriteProblem("Composite-096BitPrimes-8.cnf", "011110011010001010010010101000010001001100101100010111010111111110011100110001101110010100111100101111100101010010100100110000100010100000111110110010010101101001010010111000110000000001111001", 96); //44252395638530248087151732927*64236004244180029104592692907 WriteProblem("Composite-096BitPrimes-9.cnf", "011100111110111000011001001001010000000001011110100000111000110111100100110001000000000011111111111010011111111000111011011000101011110010001001101010111010010010110111010001011101000110010101", 96); }