Language: C++

#include <cstdio>
#include <cstdint>
#include <cstring>
#include <cassert>
#include <cctype>
#include <algorithm>
#include <vector>
#include <string>
#include <map>

//#define fprintf(...) void(0)

std::vector<std::string> preprocess(const std::string &s, std::string &t) {
  t.clear();
  std::vector<std::string> res;
  for (size_t i=0; i<s.length(); ++i) {
    if (isalpha(s[i])) {
      std::string cur(1, s[i]);
      while (++i < s.length() && isalpha(s[i])) {
        cur += s[i];
      }
      res.push_back(cur);
      t += res.size()+'0';
      if (i < s.length()) {
        t += s[i];
      }
    } else {
      t += s[i];
    }
  }
  for (size_t i=0; i<res.size(); ++i)
    fprintf(stderr, "%s%s", i>0? ", ":"", res[i].c_str());
  fprintf(stderr, "\n");
  assert(res.size() == 1 || res.size() == 2);
  return res;
}

enum Cond {
  A, NA,
  B, NB,
  AaB, NAoNB,
  NAaB, AoNB,
  AoB, NAaNB,
  NAoB, AaNB,
};

const char *CondStr[]={
  "A", "!A", "B", "!B",
  "A&B", "!A|!B", "!A&B", "A|!B",
  "A|B", "!A&!B", "!A|B", "A&!B",
};

Cond not_cond(Cond x) {
  //fprintf(stderr, "! %s\n", CondStr[int(x)]);
  return Cond(int(x)^1);
}

Cond apply_cond(Cond x, int op, Cond y) {
  if (!(x == A || x == NA)) {
    assert(false);
  }
  //fprintf(stderr, "%s %c %s\n", CondStr[int(x)], op, CondStr[int(y)]);
  if (op == '&') {
    if (x == A && y == B) return AaB;
    if (x == NA && y == B) return NAaB;
    if (x == A && y == NB) return AaNB;
    if (x == NA && y == NB) return NAaNB;
  } else if (op == '|') {
    if (x == A && y == B) return AoB;
    if (x == NA && y == B) return NAoB;
    if (x == A && y == NB) return AoNB;
    if (x == NA && y == NB) return NAoNB;
  }
  assert(false);
}

Cond parse(const std::string &s, size_t &i,
           const std::vector<std::string> &ops={"|&", ""}, size_t p=0) {

  if (ops[p].empty()) {
    if (s[i] == '(') {
      Cond tmp=parse(s, ++i, ops, 0);
      assert(s[i] == ')');
      ++i;
      return tmp;
    } else if (s[i] == '~') {
      ++i;
      if (s[i] == '1') {
        ++i;
        return NA;
      } else if (s[i] == '2') {
        ++i;
        return NB;
      } else if (s[i] == '~') {
        ++i;
        return parse(s, i, ops, 0);
      } else {
        assert(s[i] == '(');
        Cond tmp=parse(s, ++i, ops, 0);
        assert(s[i] == ')');
        ++i;
        return not_cond(tmp);
      }
    } else if (s[i] == '1') {
      ++i;
      return A;
    } else if (s[i] == '2') {
      ++i;
      return B;
    }
    assert(false);
  }

  Cond res=parse(s, i, ops, p+1);
  while (i < s.length()) {
    int op=s[i];
    if (!std::count(ops[p].begin(), ops[p].end(), op)) break;
    Cond tmp=parse(s, ++i, ops, p+1);
    res = apply_cond(res, op, tmp);
  }
  return res;
}

int V;
const int MAX_V=2000;
std::vector<int> G[MAX_V], rG[MAX_V], vs;
bool used[MAX_V];
int cmp[MAX_V];

void add_edge(int from, int to) {
  G[from].push_back(to);
  rG[to].push_back(from);
}

void dfs(int v) {
  used[v] = true;
  for (int i=0; i<int(G[v].size()); ++i)
    if (!used[G[v][i]]) dfs(G[v][i]);
  vs.push_back(v);
}

void rdfs(int v, int k) {
  used[v] = true;
  cmp[v] = k;
  for (int i=0; i<int(rG[v].size()); ++i)
    if (!used[rG[v][i]]) rdfs(rG[v][i], k);
}

int scc() {
  memset(used, 0, sizeof used);
  vs.clear();
  for (int v=0; v<V; ++v)
    if (!used[v]) dfs(v);

  memset(used, 0, sizeof used);
  int k=0;
  for (int i=vs.size()-1; i>=0; --i) {
    if (!used[vs[i]]) rdfs(vs[i], k++);
  }
  return k;
}

int main() {
  size_t N, M;
  scanf("%zu %zu", &N, &M);

  std::map<std::string, size_t> vars;
  std::vector<std::pair<Cond, std::vector<std::string>>> conds;
  for (size_t i=0; i<N; ++i) {
    char buf[512];
    scanf("%s", buf);
    std::string s=buf;
    std::string t;
    std::vector<std::string> lits=preprocess(s, t);
    fprintf(stderr, "t: %s\n", t.c_str());
    for (const auto &lit: lits) {
      if (vars.find(lit) != vars.end()) {
        size_t size=vars.size();
        vars.emplace(lit, size);
      }
    }
    size_t j=0;
    Cond cond=parse(t, j);
    conds.emplace_back(cond, lits);
  }

  V = conds.size()*2;
  int NOT=conds.size();
  for (size_t i=0; i<conds.size(); ++i) {
    Cond cond=conds[i].first;
    fprintf(stderr, "%s\n", CondStr[int(cond)]);
    std::vector<std::string> lits=conds[i].second;
    if (lits.size() == 1) {
      assert(cond == A || cond == NA);
      int a=vars[lits[0]];
      add_edge(a, a);
      add_edge(a, 
      add_edge(vars[lits[0]], NOT+vars[lits[0]]);
      add_edge(NOT+vars[lits[0]], vars[lits[0]]);
    } else {
      assert(lits.size() == 2);
      int a=vars[lits[0]], b=vars[lits[1]];

      std::string fmt;
      switch (cond) {
      case NAaB:
      case NAaNB:
      case NAoB:
      case NAoNB:
        fmt += "!";
        /* fall through */
      case AaB:
      case AaNB:
      case AoB:
      case AoNB:
        fmt += "%s";
        break;
      }

      switch (cond) {
      case AaB:
      case AaNB:
      case NAaB:
      case NAaNB:
        fmt += " & ";
          break;
      default:
        fmt += " | ";
      }

      switch (cond) {
      case AaNB:
      case NAaNB:
      case AoNB:
      case NAoNB:
        fmt += "!";
        /* fall through */
      default:
        fmt += "%s\n";
      }

      fprintf(stderr, fmt.c_str(), lits[0].c_str(), lits[1].c_str());

      switch (cond) {
      case AaB:
      case NAaB:
      case AaNB:
      case NAaNB:
        add_edge(a, NOT+a);
        add_edge(NOT+a, a);
        add_edge(b, NOT+b);
        add_edge(NOT+b, b);
        break;
      case AoB:
        add_edge(NOT+a, b);
        add_edge(NOT+b, a);
        break;
      case AoNB:
        add_edge(NOT+a, NOT+b);
        add_edge(b, a);
        break;
      case NAoB:
        add_edge(a, b);
        add_edge(NOT+b, NOT+a);
        break;
      case NAoNB:
        add_edge(a, NOT+b);
        add_edge(b, NOT+a);
        break;
      }
    }
  }

  scc();
  for (int i=0; i<NOT; ++i) {
    if (cmp[i] == cmp[NOT+i])
      return !printf("reject\n");
  }
  printf("accept\n");
  //printf("%s\n", satisfiable(g)? "accept":"reject");
}


Compiler output:
a.cc: In function 'int main()':
a.cc:198:49: error: expected ')' before ';' token
  198 |       add_edge(vars[lits[0]], NOT+vars[lits[0]]);
      |                                                 ^
      |                                                 )
a.cc:197:15: note: to match this '('
  197 |       add_edge(a,
      |               ^