fork download
copy 
  1. #include <iostream>
  2. #include <vector>
  3. #include <string>
  4. #include <stack>
  5. #include <cstring>
  6. #include <cassert>
  7.  
  8. using namespace std;
  9.  
  10. const int MAXV = 200; // max 99 zmiennych * 2
  11.  
  12. vector<int> graph[MAXV], graphRev[MAXV];
  13. bool visited[MAXV];
  14. stack<int> order;
  15. int comp[MAXV];
  16.  
  17. int litToIndex(int lit) {
  18.     int var = abs(lit) - 1;
  19.     assert(var >= 0 && var < 99);
  20.     return (lit > 0) ? 2 * var : 2 * var + 1;
  21. }
  22.  
  23. int neg(int x) {
  24.     return x ^ 1;
  25. }
  26.  
  27. void dfs1(int v) {
  28.     visited[v] = true;
  29.     for (int u : graph[v]) {
  30.         if (!visited[u]) dfs1(u);
  31.     }
  32.     order.push(v);
  33. }
  34.  
  35. void dfs2(int v, int c) {
  36.     comp[v] = c;
  37.     for (int u : graphRev[v]) {
  38.         if (comp[u] == -1) dfs2(u, c);
  39.     }
  40. }
  41.  
  42. void addImplication(int a, int b) {
  43.     graph[a].push_back(b);
  44.     graphRev[b].push_back(a);
  45. }
  46.  
  47. bool solve2SAT(int vars) {
  48.     memset(comp, -1, sizeof(comp));
  49.     memset(visited, 0, sizeof(visited));
  50.     while (!order.empty()) order.pop();
  51.  
  52.     for (int i = 0; i < 2 * vars; i++)
  53.         if (!visited[i]) dfs1(i);
  54.  
  55.     int c = 0;
  56.     while (!order.empty()) {
  57.         int v = order.top();
  58.         order.pop();
  59.         if (comp[v] == -1) dfs2(v, c++);
  60.     }
  61.  
  62.     for (int i = 0; i < vars; i++) {
  63.         if (comp[2*i] == comp[2*i + 1]) return false;
  64.     }
  65.     return true;
  66. }
  67.  
  68. int main() {
  69.     ios::sync_with_stdio(false);
  70.     cin.tie(nullptr);
  71.  
  72.     string line;
  73.     string result;
  74.  
  75.     while (getline(cin, line)) {
  76.         if (line.empty()) continue;
  77.  
  78.         for (int i = 0; i < MAXV; i++) {
  79.             graph[i].clear();
  80.             graphRev[i].clear();
  81.         }
  82.  
  83.         int len = (int)line.size();
  84.         int vars = 0;
  85.  
  86.         if (len % 8 != 0) {
  87.             cerr << "Błędny format wejścia: " << line << "\n";
  88.             exit(1);
  89.         }
  90.  
  91.         for (int i = 0; i < len; i += 8) {
  92.             if (line[i] != '(' || line[i+7] != ')') {
  93.                 cerr << "Błędny format klauzuli: " << line.substr(i,8) << "\n";
  94.                 exit(1);
  95.             }
  96.  
  97.             int lit1Sign = (line[i+1] == '+') ? 1 : (line[i+1] == '-') ? -1 : 0;
  98.             int lit1Num = (line[i+2]-'0')*10 + (line[i+3]-'0');
  99.             int lit2Sign = (line[i+4] == '+') ? 1 : (line[i+4] == '-') ? -1 : 0;
  100.             int lit2Num = (line[i+5]-'0')*10 + (line[i+6]-'0');
  101.  
  102.             if (lit1Sign == 0 || lit2Sign == 0) {
  103.                 cerr << "Nieprawidłowy znak +/- w klauzuli: " << line.substr(i,8) << "\n";
  104.                 exit(1);
  105.             }
  106.             if (lit1Num < 1 || lit1Num > 99 || lit2Num < 1 || lit2Num > 99) {
  107.                 cerr << "Nieprawidłowy numer zmiennej: " << lit1Num << " lub " << lit2Num << "\n";
  108.                 exit(1);
  109.             }
  110.  
  111.             int a = litToIndex(lit1Sign * lit1Num);
  112.             int b = litToIndex(lit2Sign * lit2Num);
  113.  
  114.             vars = max(vars, max(lit1Num, lit2Num));
  115.  
  116.             addImplication(neg(a), b);
  117.             addImplication(neg(b), a);
  118.         }
  119.  
  120.         bool sat = solve2SAT(vars);
  121.         result += sat ? '1' : '0';
  122.     }
  123.  
  124.     cout << result << '\n';
  125.  
  126.     return 0;
  127. }
Success #stdin #stdout 0.01s 5288KB
comments (?)
stdin
copy 
(+01-02)(+01+02)(-01+02)(-01-02)
(+05-03)(-20-70)
(+05+05)(+06-06)(+10-11)
stdout
copy 
011
https://ideone.com/3YPxfg
language:
C++ (gcc 8.3)
created:
1 day ago
visibility:
public

Share or Embed source code

Discover > Sphere Engine API

The brand new service which powers Ideone!

Discover > IDE Widget

Widget for compiling and running the source code in a web browser!