Untitled
unknown
plain_text
a year ago
18 kB
5
Indexable
#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 ;
if( !input )
cout<< "fxxk you " ;//
else{
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 , string output_name )
{
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 input_file( int &variables , int &clauses , vector<int> &numbers )
{
char ch;
int in ;
string gar ;
string open ;
cout<<"open name" << endl;
cin >> open ;
ifstream input( open ) ;
if( !input )
cout<< "fuck you " ;//for debug
else{
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 debbuging_output( int variables , int arrofvariables[ ] , bool satisfiable )
{
if ( satisfiable ){
cout << "s SATISFIABLE" << endl ;
for( int i = 0 ; i < variables ; i ++ ){
cout << "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
cout << " Done " << endl;
}else{
cout << "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
cout<< "arrofvariables before algorithm " << endl;
for( int i = 0 ; i < variables ; i ++ )
cout<< arrofvariables[i] << " " ;
cout<< endl;
//=======================================
cout<< "---------------identical in algorithm--------------" << endl;
for( int i = 0 ; i < clauses ; i ++ ){
for( int j = 0 ; j < variables ; j ++ ){
cout<< forcheck[i][j] << " " ;
}
cout<< endl;
}
//========================================
//=======================================
cout<< "---------------arrofvariables--------------" << endl;
for( int j = 0 ; j < variables ; j ++ ){
cout<< arrofvariables[j] << " " ;
}
//========================================
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
{
cout<< "in DLIS" << endl;
//𝑤(𝐹, 𝑢) = ∑ 𝑑𝑘(𝐹, 𝑢)
//Φ(𝑥, 𝑦) = 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
}
cout<< "biggest == " << biggest << endl;
cout<< "symble == " << symbol << endl;
cout<< "who == " << who << endl;
//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 ;
}
cout<< "aim == " << aim << endl;
//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
cout<< "in function " << endl;
int aim = 0 ;
for( int i = 0 ; i < 2 ; i ++ )
for( int j = 0 ; j < variables ; j ++ )
counter[i][j] = 0 ;
//=======================================
cout<< "---------------identical in function start--------------" << endl;
for( int i = 0 ; i < clauses ; i ++ ){
for( int j = 0 ; j < variables ; j ++ ){
cout<< identical[i][j] << " " ;
}
cout<< endl;
}
//========================================
//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 ;
}
}
cout<< "-------counter-----------------" << endl;
for( int i = 0 ; i < 2 ; i ++ ){
for( int j = 0 ; j < variables ; j ++)
cout << counter[i][j] << " " ;
cout<< endl;
}
//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
}
void DPLL_main ( int identical[][MAX_VARIAbLE] , int clauses , int variables , int forcheck[][MAX_VARIAbLE] )
{
int arrofvariables[ variables ] ;
for ( int i = 0 ; i < variables ; i ++ )
arrofvariables [ i ] = 0 ;//all false
//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 ) ;
cout<< "truth value == " << truth_value << endl;
if( identical[0][0] == 0 )system ("pause");
//check satisfied yet
}while( truth_value != 1 && truth_value != 2) ;
if( truth_value == 1 || truth_value == 2 )
satisfiable = true ;
//==================================================================================
//outfile( argv[ 2 ] , variables , arrofvariables , satisfiable ) ;
debbuging_output( variables , arrofvariables , satisfiable ) ;
//========================================================================================
}
//=======================================
//int main( int argc , char *argv[] )
//========================================
int main ( )
{
//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 ) ;
========================================
*/
input_file( variables , clauses , numbers ) ;
int sizeofvector = numbers.size() ;
int identical [ clauses ][ MAX_VARIAbLE ] = { { 0 } , { 0 } } ;
//all zero
for( int i = 0 ; i < clauses ; i ++ )
for( int j = 0 ; j < variables ; j ++ )
identical[ i ][ j ] = 0 ;
//2.
//for debug////////////////////////////////////////////////////
cout<< "size of vector " << sizeofvector << endl ;
bool satisfiable = false ;
//devided into small clause
seperate( numbers , sizeofvector , identical , clauses , variables ) ;
int forcheck [ clauses ][ MAX_VARIAbLE ] = { { 0 } , { 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
DPLL_main( identical , clauses , variables , forcheck ) ;
return 0 ;
}
Editor is loading...
Leave a Comment