Untitled

#include<iostream>
#include<algorithm>
#include<string>
#include<iomanip>
#include<vector>
#include<sstream>
#include<cstdlib>
#include<fstream>
using namespace std ;
/*
tell if the algorism can be satisfied or not
 ˅, ˄, ¬: respectively represent logic OR, AND, and NOT.
Clause: Each clause is a disjunction of one or more literals, like (A ˅ B).


what i might do is
    seperate the whole input by the {} clause
    use dynamic memory to store each clause
        struct ,pointer
    what if clause contain clause
        detect the first {
        if the next clause is also { means the clause in the containing another clause
            find { and run until '}'
                if detect { first
                than
                    first determine the biggest layer
                    second use insert
since everyclause is && together then i just need to find a solution make every clause true

when cout , the variable a b c are 1 2 3 .
*/

const int MAX_VARIAbLE = 100 ;
int deletedclauses = 0 ;

void input_file( char *argv , int &variables , int &clauses , vector<int> numbers )
{
    ifstream input( argv , ios::in ) ;

    char ch;
    int in ;
    string gar ;

        input >> gar ;
        input >> gar ;
        while ( input >> in ) {
            //number or not
            if( !input.fail() ){// if it is a number
                if( variables == 0 )
                    variables = in ;
                else if( clauses == 0 )
                    clauses = in ;
                else
                    numbers.push_back( in ) ;
            }
        }

}

void output_file( char *argv , int variables , int arrofvariables[ ] , bool satisfiable )
{
    ofstream outputfile( argv , ios::out ) ;

    if ( satisfiable ){
        outputfile << "s SATISFIABLE" << endl ;

        for( int i = 0 ; i < variables ; i ++ ){
            outputfile  << "v “ " << i + 1 << " -> "
                        <<( arrofvariables[ i ] == 1 ? "True" : "False" )
                        << endl;
        }// if == 1 true ,if == -1 false , if == 0 false because the equation can already be satisfied when it havent be assign yet
        //it means no matter it is true or false the equation can be satisfied

        outputfile << " Done " << endl;
    }else{
        outputfile << "s UNSATISFIABLE" << endl ;
    }

}

void seperate ( vector<int> numbers , int sizeofvector , int identical[][MAX_VARIAbLE] , int clauses , int variables )
{
    for( int i = 0 , j = 0 , a = 0 ; a < sizeofvector ; j ++ , a ++ ){
        if( numbers[ a ] == 0 ){
            i ++ ;
            j = 0 ;
            a ++ ;
            while( numbers[a] == 0 )
                a ++ ;
            identical[ i ][ j ] = numbers[ a ] ;
        }
        else {
            identical[ i ][ j ] = numbers[ a ] ;
        }
    }
    //my rule if numbers[ a ] == 1 than [ i ][ j ] == 1
    //but if numbers [ a ] == -1
}

void eli_do ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim , int clau , int vari , int operation )
{
    if( operation == 1 ){
        for( int i = clau + 1 ; i < clauses ; i ++  )
            for( int j = 0 ; j < variables ; j ++ ){
                //delete whole clauses
                int temp = identical[i][j] ;
                identical[ i - 1 ][ j ] = temp ;
            }
    }
    if( operation == 2 ){
        for( int c = vari + 1 ; c < variables ; c ++ ){
            identical[ clau ][ c - 1 ] = identical[ clau ][ c ] ;
        }
    }
}
void elimination ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim )
{
    int clau = 0 ;
    int vari = 0 ;
    int counter = 0 ;
    //check
    for( int i = 0 ; i < clauses ; i ++ )
        for( int j = 0 ; j < variables ; j ++ ){
            if( identical[i][j] == aim ){
                clau = i ;
                vari = j ;

                eli_do( identical , clauses , variables , aim , clau , vari , 1 ) ;
                i -- ;
                j = 0 ;
                counter ++ ;
                for( int b = 0 ; b < variables ; b ++ )
                    identical[ clauses - counter ][b] = 0 ;
            }
        }

    for( int i = 0 ; i < clauses ; i ++ )
        for( int j = 0 ; j < variables ; j ++ ){
            if( identical[i][j] == aim * -1 ){
                clau = i ;
                vari = j ;

                eli_do( identical , clauses , variables , aim , clau , vari , 2 ) ;
                i -- ;
                j = 0 ;
            }
        }
}

void elimination_PLE ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int aim )
{
    for( int i = 0 ; i < clauses ; i ++ )
        for( int j = 0 ; j < variables ; j ++ ){
            if( identical[ i ][ j ] == aim ){
                //delete whole clauses
                for( int a = i + 1 ; a < clauses ; a ++ ){
                    for( int b = 0 ; b < variables ; b ++ ){
                        int temp = identical[i][j] ;
                        identical[ i - 1 ][ j ] = temp ;
                    }
                }
            }
        }
}

int DPLL_algorithm ( int forcheck[][MAX_VARIAbLE] , int clauses , int variables , int arrofvariables[] )
{   //calculate the truth value of the clause

    //what algorithm really do is
    //calculate every clause at a time and and with bool_temp

    int bool_inside = 0 ;
    int bool_iden = 0 ;
    int temp = 0 ;
    int truth_value = 0 ;

    for( int i = 0 ; i < clauses ; i ++ ){
        for( int j = 0 ; j < variables ; j ++ ){
            //what's the variable , such as : a, -b ,c ...
            if( forcheck[i][j] != 0 ){
                temp = forcheck[i][j] ;
                    if( temp < 0 )
                        bool_iden = arrofvariables[ temp*-1 - 1 ] * temp  ;
                    else
                        bool_iden = arrofvariables[ temp - 1 ] * temp  ;
                if( bool_iden != 0 ){
                    if( bool_iden == 1 || bool_inside == 1 )
                        bool_inside = 1 ;
                }
            }
        }
        if( truth_value == 1 && bool_inside == 1 )
            truth_value = 1 ;
        else
            truth_value = 0 ;
    }
    //see if unsatisfiable
    int check = 0 ;
    for( int i = 0 ; i < variables ; i ++ )
        if( arrofvariables[i] != 0 )
            check ++ ;
    if( check == variables && truth_value == 0)
        truth_value = 2 ;

    return truth_value ;
}

void DLIS ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int counter[][MAX_VARIAbLE] , int arrofvariables[] ) //call by DPLL
{
    //𝑤(𝐹, 𝑢) = ∑ 𝑑𝑘(𝐹, 𝑢)
    //Φ(𝑥, 𝑦) = max{𝑥, 𝑦}
    /*
    determine priority of variables by search how many clauses contain the variable
    assign the variable that contained by the most clauses true if a is the most contained variable
    false if -a is the most contained
    */
    int biggest = 0 ;
    int symbol = 0 ;
    int who = 0 ;
    int aim = 0 ;

    //determine whose show up the most times
    for( int i = 0 ; i < 2 ; i ++ )
        for( int j = 0 ; j < variables ; j ++ )
            if( counter[i][j] > biggest ){
                biggest = counter[i][j] ;
                symbol = i ;// y
                who = j ;   // x
            }

    //assign true if the positive version is more than its negative version of the variable
    //else assign false

    if( symbol == 0 ){
        arrofvariables[ who ] = 1 ;
        aim = who + 1 ;
    }
    else{
        arrofvariables[ who ] = -1 ;
        aim = who + 1 ;
        aim *= -1 ;
    }

    //delete clauses contain the variable
    elimination( identical , clauses , variables , aim ) ;
}

void DPLL_funtion ( int identical[][ MAX_VARIAbLE ] , int clauses , int variables , int arrofvariables[] ,int counter[][MAX_VARIAbLE] )
{   //including assign variables true or false
    int aim = 0 ;

    for( int i = 0 ; i < 2 ; i ++ )
        for( int j = 0 ; j < variables ; j ++ )
            counter[i][j] = 0 ;

    //unit propagation //...............................................................
    //there is a clauses that only contain a variable
       //(A) ˄ (A ˅ B ˅ D) ˄ (¬A ˅ B) ˄ (¬A ˅ B ˅ C)
        //Because (A) is the unit clause, A must be set to “TRUE”. The formula can be
        //simplified to (B) ˄ (B ˅ C)

        // looking for clause with only one variables
        for( int i = 0 ; i < clauses ; i ++ )
            for( int j = 0 ; j < 2 ; j ++ ){
                if ( ( identical[ i ][ 1 ] == 0 )  && (identical[i][0] != 0 ) ){//already 0 when j = 2
                    //means the clauses has only one variable
                    int temp = identical[ i ][ j - 1 ] ;//what's the variable
                    arrofvariables[ temp - 1 ] = 1 ;
                    aim = temp ;

                    elimination ( identical , clauses , variables , aim ) ;
                    //check every clauses has the variable
                    //delete the clauses that containing a and the variable -a in other clauses
                }
            }

    //pure literal elimination //..................................................................
    //there is a variable only exist in a clause and shown one times
        //Example:
        //(A) ˄ (A ˅ B) ˄ (¬A ˅ B ˅ C)
        //Because C appears only once throughout the entire formula., C can be
        //assigned to “TRUE”. The formula can be simplified to (A) ˄ (A ˅ B)

        //see each variables contained by how many clauses
        //save in counter
        for( int i = 0 ; i < clauses ; i ++ ){
            for( int j = 0 ; j < variables ; j ++ ){
                if( identical[i][j] > 0 ){
                    int temp = identical[i][j] ;
                    counter[0][ temp - 1 ] ++ ;
                }else if ( identical[i][j] < 0 ){
                    int temp = identical[i][j] ;
                    temp *= -1 ;
                    counter[1][ temp - 1 ] ++ ;
                }else break ;
            }
        }

        //assign the variable into true if the variable only show in positive or negative
        //check the counter array to see if there any variable that satisfied
        for( int i = 0 ; i < 2 ; i ++ )
            for( int j = 0 ; j < variables ; j ++ ){
                if( ( counter[0][j] != counter[1][j] ) && ( counter[0][j] == 0 || counter[1][j] == 0 )  ){
                    if( i == 0 ){
                        aim = ( j + 1 ) ;
                        arrofvariables[ j ] =  1 ;
                    }
                    else{
                        cout<< "wrong here "<< endl;
                        aim = ( j + 1 ) * -1 ;
                        arrofvariables[ j ] =  -1 ;
                    }
                    elimination_PLE ( identical , clauses , variables , aim ) ;
                }
            }

    //if( the whole question is already empty )
        //return true ;
    //if ( there is one clause is empty )
        //return false ;
    //because 0 && with other clauses is 0
}

bool DPLL_main ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int forcheck[][MAX_VARIAbLE] , int arrofvariables[] )
{
    //0 = not assigned yet , 1 = true , -1 = false
    int counter[ 2 ][ MAX_VARIAbLE ] = { 0 } ;
        for ( int i = 0 ; i < 2 ; i ++ )
            for ( int j = 0 ; j < variables ; j ++ )
                counter[ i ][ j ] = 0 ; //for all zero

    int truth_value = 0 ;
    bool satisfiable = false ;
        do{
            DPLL_funtion( identical , clauses , variables , arrofvariables , counter ) ;
            // delete what should be delete
            DLIS( identical , clauses , variables , counter , arrofvariables) ;
            //assign and delete
            truth_value = DPLL_algorithm( forcheck , clauses , variables , arrofvariables ) ;

            if( identical[0][0] == 0 )
                break ;
            //check satisfied yet
        }while( truth_value != 1 && truth_value != 2) ;

        if( truth_value == 1 || truth_value == 2 )
            satisfiable = true ;
    return satisfiable ;

}

int main( int argc , char *argv[] )
{
    //open the file first
    //....get question
    int variables = 0 , clauses = 0 ;
    vector< int > numbers ;

    //compile your .cpp by : g++ -std=c++11 112501557_Final.cpp -o Final.out
    //when execute your .out by : ./Final.out testcase1.cnf testcase1.txt
    //argv[0] represent ./Final.out
    //argv[1] represent testcase1.cnf
    //argv[2] represent testcase1.txt
    //1.open the file and get the data stored in a string

    input_file( argv[ 1 ] , variables , clauses , numbers ) ;

    int sizeofvector = numbers.size() ;
     int arrofvariables[ variables ] ;
        for ( int i = 0 ; i < variables ; i ++ )
            arrofvariables [ i ] = 0 ;//all false

    int identical [ 200 ][ MAX_VARIAbLE ] = { 0 } ;
    //all zero
        for( int i = 0 ; i < clauses ; i ++ )
            for( int j = 0 ; j < variables ; j ++ )
                identical[ i ][ j ] = 0 ;
    //2.

    bool satisfiable = false ;
    //devided into small clause
    seperate( numbers , sizeofvector , identical , clauses , variables ) ;

     int forcheck [ 200 ][ MAX_VARIAbLE ] = { 0 } ;
     //all zero
        for( int i = 0 ; i < clauses ; i ++ )
            for( int j = 0 ; j < variables ; j ++ )
                forcheck[ i ][ j ] = 0 ;

     for( int i = 0 ; i < clauses ; i ++ )
        for( int j = 0 ; j  <variables ; j ++ )
            forcheck[i][j] = identical[i][j] ;

    //3.calculate the formula
    //4.get the truth value of clauses

    satisfiable = DPLL_main( identical , clauses , variables , forcheck , arrofvariables ) ;
    output_file( argv[ 2 ] , variables , arrofvariables , satisfiable ) ;
    return 0 ;
}