#include <bitset>
#include <iostream>
#include <iomanip>
using namespace std;

const unsigned int n = 15;    //#Variablen
const unsigned int np1 = n+1; //#Variablen+ 0-te Variable
// 0-te Variable: immer mit false besetzt
const unsigned int m = 20; //Klauseln
const unsigned int k =  3; //Ordnung des Problems

// class KNF { public:
// //int count[n]; //Häufigkeit der Variablen
// int klausel[m][k]; //gibt Literale der Klausel an, <0: negierte Variable 
// };

typedef bool belegung[np1];
typedef int KNF[m][k];

/*
Auswertung einer KNF,
bei einer falschen Klausel wird abgebrochen
*/
bool check (const KNF& F, const belegung& b)
{
  for (unsigned int i=0; i<m; i++){
    bool wert=false;
    for (unsigned int j=0; j<k; j++) {
       int v = F[i][j];
       if ( v >= 0 ){
         if ( b[v] ) { wert=true; break; }
       } else {
         if ( !b[-v] ) { wert=true; break; }
       }
    }
    if (!wert)return false ;
  }
  return true;
};

/*
Auswertung einer KNF,
es wird die Zahl der Lösungen bestimmt
*/
unsigned int count_recursive(const KNF&F, belegung& b,unsigned int i){
   if (i==n){
     if ( check(F,b) ) {return 1;}
     return 0;
   }
   i = i+1;
   b[i]=true;
   unsigned int lc = count_recursive(F,b,i);
   b[i]=false;
   lc += count_recursive(F,b,i);
   return lc;
}

/*
Auswertung einer KNF,
es wird bei der ersten Lösung abgebrochen
*/
bool check_recursive(const KNF&F, belegung& b,unsigned int i){
   if (i==n) return check(F,b);
   i=i+1;
   b[i]=true;
   if (check_recursive(F,b,i)) return true;
   b[i]=false;
   if (check_recursive(F,b,i)) return true;
   return false;
}


int main(){

cout << "Variablen: "  << n
     << ", Klauseln: " << m
     << ", Ordnung: "  << k
     << "\n";

KNF F;
for(unsigned int i=0; i<m;i++) { 
   for(unsigned int j=0; j<k;j++){
      F[i][j]=((i+j)%n + 1)*( ((i+j)%2)*2 -1 );
   }
}

for(unsigned int i=0; i<m;i++){ cout << "("<< setfill('0');
    for(unsigned int j=0; j<k;j++) {
        if (F[i][j] > 0) cout << "  X_"<< setw(2)<< F[i][j];
        if (F[i][j] < 0) cout << " ^X_"<< setw(2)<< -F[i][j];
    }
    cout << " )\n";
}

belegung b;

b[0]=false;
for (unsigned int i=1; i<=n;i++) b[i]=false;
for (unsigned int i=2; i<=n;i+=2) b[i]=true;
cout << "\nTestbelegung: \n";
for (unsigned int i=1; i<=n;i++){
    if (b[i]) cout << "  x_"<<setw(2)<< i; else cout << " ^x_"<<setw(2)<< i;
    if (i%10==0) cout <<"\n";
}
if (n%10!=0) cout <<"\n";
cout << "Resultat: "<<check(F,b) << "\n";



cout << "\nLösbar:   "<<check_recursive(F,b,0) << "\n";
cout << "Beispiel: \n";
for (unsigned int i=1; i<=n;i++){
    if (b[i]) cout << "  x_"<<setw(2)<< i; else cout << " ^x_"<<setw(2)<< i;
    if (i%10==0) cout <<"\n";
}
if (n%10!=0) cout <<"\n";

cout << "\nLösungen: "<<count_recursive(F,b,0) << "\n";

}