3-SAT

3-SATを解く、Schoeningのアルゴリズムという乱択アルゴリズムを実装した。
変数はアルファベット１文字のみ。否定は~。
未検証。

(a|~b|~c)&(b|c|~d)
のように入力を与える。文字同士の間に空白は入れない。

#include<iostream>
#include<vector>
#include<algorithm>
#include<string>
#include<cctype>
#include<map>
#include<set>
#include<ctime>

using namespace std;

string f;         //論理式
int n;            //変数の個数
int R;            //ラウンド数
int now;          //構文解析用
int pos;          //満たしていないclause の ( のid
int litnum;       //満たしていないclause の literal の数
map<char,bool>mp; //変数の割り当て

bool literal(void){
  now++;
  if(isalpha(f[now-1]))return mp[f[now-1]];
  if(isdigit(f[now-1]))return mp[f[now-1]];
  now++;
  return !mp[f[now-1]];
}

bool clause(void){
  bool res=literal();
  while(true){
    if(f[now]=='|'){
      now++;
      bool tmp=literal();
      res|=tmp;
    }
    else break;
  }
  return res;
}

bool expression(void){
  bool res=true;
  while(true){
    if(f[now]=='('){
      int tpos=now++;
      bool tmp=clause();
      if(!tmp){
        pos=tpos;
        litnum=(now-pos+1)/2;
      }
      res&=tmp;
      now++;
    }
    else if(f[now]=='&'){
      now++;
    }
    else break;
  }
  return res;
}

typedef unsigned int uint;

static uint x=123456789,y=362436069,z=521288629,w=88675123;

void init_xor128(uint s) {
  z^=s;
  z^=z>>21;
  z^=z<<27;
  z^=z>>4;
  z*=2685821657736338717LL;
}

uint xor128(void) {
  uint t=(x^(x<<11));
  x=y; y=z; z=w;
  return ( w=(w^(w>>19))^(t^(t>>8)) );
}

bool randomWalk3Sat(void){

  for(int r=0;r<R;r++){

    for(char c='A';c<='Z';c++)mp[c]=(bool)(xor128()%2);
    for(char c='a';c<='z';c++)mp[c]=(bool)(xor128()%2);

    for(int k=0;k<3*n;k++){
      now=0;
      if(expression())return true;
      int id=pos+(int)(xor128()%litnum)*2+1;
      if(!isdigit(f[id]))mp[f[id]]=!mp[f[id]];
    }
  }
  return false;
}

int main(void){

  while(cin >> f){
    set<char>S;
    for(int i=0;i<f.size();i++)
      if(isalpha(f[i]) || isdigit(f[i]))S.insert(f[i]);

    R=1000;
    n=S.size();
    time_t timer;
    time(&timer);
    init_xor128((uint)timer);

    mp['0']=false;
    mp['1']=true;

    cout << randomWalk3Sat() << endl;
  }

  return 0;
}