#include <stdio.h>
#include <stdlib.h>
#include <DIMAC.h>
#include <DPLL.h>
#include <WalkSAT.h>

int DPLL( HEADS *lista, int literal );
int WalkSAT( int **iWVariables, float p, long max, int *iPossibleSolution ); 
void tomb2(int * m, int s);

       int *MODELL;  
       int rek = 0;
       
       int iNumberOfVariables;
       int iNumberOfClauses;
       int P_CNF = 3;
           
main()
{
       int **RandomClauses;       
       int **value;
       
       printf( "**************************************************************\n" );
       printf( "************                                      ************\n" );
       printf( "************ - MI algoritmusok a SAT problemara - ************\n" );
       printf( "************                                      ************\n" );
       printf( "************ -         DPLL es WalkSAT            ************\n" );
       printf( "************                                      ************\n" );
       printf( "**************************************************************\n" );
       printf( "\nAdja meg a klozok szamat: " ); 
       scanf( "%d", &iNumberOfClauses );
       printf( "Adja meg a valtozok szamat: " );
       scanf( "%d", &iNumberOfVariables );
                  
       printf( "\nValtozok: %d - Klozok: %d\n", iNumberOfVariables, iNumberOfClauses );
       
       printf( "\nA folytatashoz nyomjon meg egy billentyut!\n");
       getch();
       
       system("cls");
                            
       int i, j, k;
       
       srand((unsigned) time(NULL));
       
       RandomClauses = (int **)malloc ( iNumberOfClauses * sizeof(int *) );
       for( i = 0; i < iNumberOfClauses; i++ )
            RandomClauses[ i ] = (int *)malloc( P_CNF * sizeof( int ) );
       
       value = (int **)malloc ( iNumberOfClauses * sizeof(int *) );
       for( i = 0; i < iNumberOfClauses; i++ )
            value[ i ] = (int *)malloc( P_CNF * sizeof( int ) );

       MODELL = (int *)malloc ( iNumberOfVariables * sizeof( int ) );
       for ( i = 0; i < iNumberOfVariables; i++ ) MODELL[ i ] = -1; 

// 3SAT feladat előállítás kezdete

       i = 0;
       while ( i < iNumberOfClauses )
       {
           for ( j = 0; j < P_CNF; j++ )
           {
               do
               {
                   RandomClauses[ i ][ j ] = rand() % iNumberOfVariables + 1;
                   for ( k = 0; k < j; k++ )
                       if ( RandomClauses[ i ][ k ] == RandomClauses[ i ][ j ]) 
                          break;
               } while ( k < j );
           }
           for ( j = 0; j < P_CNF; j++ )
               if ( rand() % 2 ) RandomClauses[ i ][ j ] = -RandomClauses[ i ][ j ];
       
           double sum, sum1;
           sum = 0;
           for ( j = 0; j < P_CNF; j++)
                   sum += pow( 2, RandomClauses[ i ][ j ] );
           for ( k = 0; k < i; k++ )
           {
               sum1 = 0;
               for ( j = 0; j < P_CNF; j++)
                   sum1 += pow( 2, RandomClauses[ k ][ j ] );
               if ( sum == sum1 ) 
               {
                    k = i;
                    i--;
               }
           }
           i++;
       }       
       
       printf( "A veletlenszeruen eloallitott 3SAT feladat!\n\n");
       matrix( RandomClauses, iNumberOfClauses, P_CNF );

// 3SAT feladat előállítás vége

       printf( "\nA folytatashoz nyomjon meg egy billentyut!\n");
       getch();
       
       system("cls");

// DPLL hívás kezdete

       printf( "**************************************************************\n" );
       printf( "************                                      ************\n" );
       printf( "************ -            DPLL futasa           - ************\n" );
       printf( "************                                      ************\n" );
       printf( "**************************************************************\n" );

       HEADS *lista1 = ( HEADS * )malloc( sizeof( HEADS ) );
       HEADS *lista2 = ( HEADS * )malloc( sizeof( HEADS ) );

       lista1->elso = NULL;
       lista1->utolso = NULL;
       lista1->s = 0;

       for ( i = 0; i < iNumberOfClauses ; i++ )
           lista1 = beszur_kloz( lista1, RandomClauses[ i ] );
       
       lista2 = copy_lista( lista1 );

       int lit = valaszt( lista1 );
       
       if ( DPLL( lista1, lit ) || DPLL( lista2, -lit ) )
       {
            printf("\nKIELEGITHETO\n");
            printf("\nMODELL: " );
            for ( i = 0; i < iNumberOfVariables; i++ ) printf( "%d", MODELL[ i ] ); 
       }
       else
       {
            printf("\nKIELEGITHETETLEN\n");
            printf("\nMODELL: " );
            for ( i = 0; i < iNumberOfVariables; i++ ) printf( "%d", MODELL[ i ] ); 
       }
       
       printf("\nA rekurziv hivasok szama: %d\n", rek);

// DPLL hívás vége

       printf( "\nA folytatashoz nyomjon meg egy billentyut!\n");
       getch();
       
       system("cls");

// WalkSAT hívás kezdete

       printf( "**************************************************************\n" );
       printf( "************                                      ************\n" );
       printf( "************ -      WalkSAT inicializalas       - ************\n" );
       printf( "************                                      ************\n" );
       printf( "**************************************************************\n" );

       float P;
       long MAX_SUBSTITUTION;

       printf( "\nAdja meg a moho lepes valoszinuseget: " ); 
       scanf( "%f", &P );
       printf( "Adja a maximalis futasok szamat: " );
       scanf( "%ld", &MAX_SUBSTITUTION );
                  
       printf( "\nHeurisztika valasztas valoszinusege: %f - Futasok szama: %d\n", P, MAX_SUBSTITUTION );
       
       printf( "\nA folytatashoz nyomjon meg egy billentyut!\n");
       getch();
       
       system("cls");

       printf( "**************************************************************\n" );
       printf( "************                                      ************\n" );
       printf( "************ -          WalkSAT futasa          - ************\n" );
       printf( "************                                      ************\n" );
       printf( "**************************************************************\n" );


       int modell[ iNumberOfVariables ];
            
       int isSatisfiable = WalkSAT( RandomClauses, P, MAX_SUBSTITUTION, modell );

       if ( isSatisfiable )
       {
            printf("\nKIELEGITHETO\n");
            printf("\nMODELL: " );
            for ( i = 0; i < iNumberOfVariables; i++ ) printf( "%d", modell[ i ] ); 
       }
       else
       {
            printf("\nNem tudom eldonteni a feladatot!\n");
            printf("\nAz utolso vizsgalt interpretacio: " );
            for ( i = 0; i < iNumberOfVariables; i++ ) printf( "%d", modell[ i ] ); 
       }
       
       printf("\nA megtett ciklusok szama: %d\n", rek);

// WalkSAT hívás vége

       printf( "\nA befejezeshez nyomjon meg egy billentyut!\n");
       getch();

}

int WalkSAT( int **iWVariables, float p, long max, int *iPossibleSolution )
{
       functInitialize( iPossibleSolution, iNumberOfVariables );
       
       int i, j;                               
       int **iValues;

       iValues = ( int ** ) malloc ( iNumberOfClauses * sizeof( int * ) );
       for( i = 0; i < iNumberOfClauses; i++ )
            iValues[ i ] = ( int * ) malloc( P_CNF * sizeof( int ) );
   
/* Statisztikán nyugvó elso interpretacio valasztas      
        int db[ 2 * iNumberOfVariables + 1 ];
        int m = 0;
       int pos = 0;    
              for ( i = 0; i < 2 * iNumberOfVariables + 1 ; i++ ) db[ i ] = 0;      
       
       for ( i = 0; i < iNumberOfClauses ; i++ )
           for ( j = 0; j < P_CNF; j++ )
           {
               db[ iWVariables[ i ][ j ] + iNumberOfVariables ]++;
               if ( db[ iWVariables[ i ][ j ] + iNumberOfVariables ] > max )
               {
                    m = db[ iWVariables[ i ][ j ] + iNumberOfVariables ];
                    pos = iWVariables[ i ][ j ] + iNumberOfVariables;
               }
           }
             int var[ iNumberOfVariables ]; 
       for ( i = 0; i < iNumberOfVariables; i++ )
           if ( db[ i ] < db[ (2 * iNumberOfVariables) - i ] ) var[ i ] = 1;
           else if ( db[ i ] > db[ (2 * iNumberOfVariables) - i ] ) var[ i ] = 0;
                else var[ i ] = rand() % 2;
       int tmp;
       for ( i = 0; i < (int)(iNumberOfVariables / 2); i++ )
       {
           tmp = var[ i ];
           var[ i ] = var[ iNumberOfVariables - 1 - i ];
           var[ iNumberOfVariables - 1 - i  ] = tmp;
       }
       
*/
       functLoadValues( iWVariables, iValues, iPossibleSolution, iNumberOfClauses );
       int iSolution[ iNumberOfClauses ];

       printf( "\nA kiindulo interpretacio: " );
       for ( j = 0; j < iNumberOfVariables; j++ )
       {
            printf( "%d", iPossibleSolution[ j ] );
//            iPossibleSolution[ j ] = var[ j ];
       }
       
       printf( "\n" );
//       tomb2( db, iNumberOfVariables );
//       printf( "\n" );
       int l;
       int iFalseClause = 0;
    
       for ( l = 0; l < max; l++ )
       {
           if ( isSolution( iValues, iSolution, iNumberOfClauses ) == iNumberOfClauses ) 
           {
                rek = l;
                return 1;
           }
           iFalseClause = functRandomFalseClause( iSolution );
           int iChangedVariable;
           int iValueOfChangedVariable;
           int v;
           float prob = ( ( rand() % 10 ) + 1 ) / 10.0;
           if ( prob > p )
           {
                v = rand() % P_CNF;
                iChangedVariable = abs( iWVariables[ iFalseClause ][ v ] ); 
                if ( iPossibleSolution[ iChangedVariable - 1 ] ) iPossibleSolution[ iChangedVariable - 1 ] = 0;
                else iPossibleSolution[ iChangedVariable - 1 ] = 1;   
                functLoadValues( iWVariables, iValues, iPossibleSolution, iNumberOfClauses );
//                printf( "Stochastic\n" );
//                for ( j = 0; j < iNumberOfVariables; j++ ) printf( "%d ", iPossibleSolution[ j ] );
//                printf( "\n" );      
           }
// Bármelyik szimbólum a klózban, amelyk maximalizálja a kielégített klózok számát.
           else
           {
               int iMaxNumberOfClauses = 0;
               int sum, k;
            
               int FalseClauseVars[ P_CNF ];
               for ( i = 0; i < P_CNF; i++ ) FalseClauseVars[ i ] = abs( iWVariables[ iFalseClause ][ i ] );
            
               int tmpSolution[ iNumberOfVariables ];
            
               for ( j = 0; j < P_CNF; j++ )
               {
                   for ( i = 0; i < iNumberOfVariables; i++ ) tmpSolution[ i ] = iSolution[ i ];
                   if ( tmpSolution[ FalseClauseVars[ j ] ] ) tmpSolution[ FalseClauseVars[ j ] ] = 0;
                   else tmpSolution[ FalseClauseVars[ j ] ] = 1;
                   functLoadValues( iWVariables, iValues, tmpSolution, iNumberOfClauses );
                   sum = isSolution( iValues, iSolution, iNumberOfClauses );
                   if ( iMaxNumberOfClauses < sum )
                   {
                        iMaxNumberOfClauses = sum;
                        k = j;
                   } 
               }
               if ( iPossibleSolution[ FalseClauseVars[ k ] ] ) iPossibleSolution[ FalseClauseVars[ k ] ] = 0;
               else iPossibleSolution[ FalseClauseVars[ k ] ] = 1;
               functLoadValues( iWVariables, iValues, iPossibleSolution, iNumberOfClauses );     
//               printf( "Greed\n" );
//               for ( j = 0; j < iNumberOfVariables; j++ ) printf( "%d ", iPossibleSolution[ j ] );
//               printf( "\n" );
            }        
       }
       rek = l;
       return 0;
}

int DPLL( HEADS *lista, int literal )
{
    int i, k, s;
       rek++;
       int l;
       LINE *lu;

//       printf("\nFIRST\n"); 
//       printf("%d", literal);
//       printf("\n-FIRST-\n");
       
       if ( literal > 0 ) MODELL[ literal - 1 ] = 1;
       else MODELL[ ( int ) abs( literal ) - 1 ] = 0;
       
//       if ( !lista->elso ) return 1;
             

             if ( k = nullaz_kloz( lista, literal ) )
                for ( i = 0; i < k; i++ )
                    lista = torol_kloz( lista );
          
             lista = copy_lista( lista );  
             torol_literal( lista, -literal );
             
//             bejar_elore_kloz( lista );
/* UNIT KLÓZok keresése */
             lu = NULL;
             if (lu = unit_kloz( lista, lu ))
             {
//                    printf("\nUNIT\n"); 
//                    bejar_elore_literal( lu );
//                    printf("\n-UNIT-\n");
                    if ( !check_unit( lu ) )
                    {
                         free( lista );
                         return 0;
                    }
                    else
                    {
                          l = lu->literal;
                          return DPLL( lista, l );
                    }
             } 

            if ( ! ( l = valaszt( lista ) ) ) 
            {
                 free( lista );
                 return 1;
            }

            HEADS *lista2 = ( HEADS * )malloc( sizeof( HEADS ) );
            lista2 = copy_lista( lista );
            
            return ( DPLL( lista, l ) || DPLL( lista2, -l) );
       
}

void tomb2(int * m, int s)
{
     int i;
     for ( i = s + 1; i <= 2 * s; i++ )
         printf( "%d\t", m[ i ]);
     printf( "\n" );
     for ( i = s - 1; i >= 0; i-- )
         printf( "%d\t", m[ i ]);


           
}