RB2CNF - Editorial

PROBLEM LINK:

Practice
Div-2 Contest
Div-1 Contest

Author & Editorialist: Alei Reyes
Tester: Istvan Nagy

DIFFICULTY:

Medium

PREREQUISITES:

Max flow - min cut

PROBLEM:

Let S=\{X_1, X_2, ..., X_N, \neg X_1, \neg X_2, ..., \neg X_N \} be a set of boolean variables. Initially some of the variables are true and others false. The cost to change the value of variable X_i is C_i

You are given a 2-CNF boolean expression B using the variables of S. Each variable can be painted in either red or black, such that the following conditions are satisfied:

  • X_i and \neg X_i have distinct colours.
  • Each clause contains variables of distinct colour.

Find the minimum cost to change the values of the variables and make B evaluate to true.

Quick Explanation

The expression can be transformed to the form B=(Y_1 \rightarrow Z_1) \wedge (Y_2 \rightarrow Z_2) \wedge ... \wedge (Y_M \rightarrow Z_M), where Y_i, Z_i \in S, such that either the variable or its negation (but not both) is present in the expression. B evaluates to false when there is a path that goes from a True variable to a False variable. Is possible to construct a graph where the minimum cut finds the minimum cost to remove all such paths.

Explanation

Let R denote a red variable and B a black variable, R \lor B = \neg B \rightarrow R. Note that \neg B is painted in red, therefore the expression can be written as a conjunction of conditionals, B=(Y_1 \rightarrow Z_1) \wedge (Y_2 \rightarrow Z_2) \wedge ... \wedge (Y_M \rightarrow Z_M) such that each clause contains variables painted in red. Since X_i and \neg X_i have distinct colours, then only one of them is present in the new expression.

In the problem we are not given the colours of the vertices, however we can find a valid colouring with dfs. Let’s suppose that u is red, if there is a clause of the form u \lor v = \neg v \rightarrow u, then v must be black. On the other hand if there is a clause of the form \neg u \lor v = u \rightarrow v, then v must be red.

Let’s construct a graph G as follows:

  • Create one vertex for each variable of the expression Y_i, Z_i and two special vertices True and False.
  • Add an edge from Y_i to Z_i with infinite capacity.
  • Add an edge from True to all variables with value true, with capacity equal to the cost of changing the cost of each variable.
  • Add an edge from each variable with value false to the node False, with capacity equal to the cost of changing the cost of each variable.

The expression evaluates to true if there is no path connecting True with False, the problem of removing the edges with minimum cost to disconnect a pair of vertices is called minimum cut. We assigned infinite capacity to the edges of the form Y_i \rightarrow Z_i, because is not allowed to remove a clause. Let’s analyze in this model the meaning of removing each type of edge.

  • Remove an edge an edge E from True to P means changing the value of P to false. But since P is now false should we add an edge from P to False? it turns out that even if we add such edge, True and False will be still disconnected, because if there is another path from True to P, then it was not necessary to remove the edge E in the first place, and that is a contradiction because we have a minimum cut.
  • Similarly removing an edge from P to False means changing the value of P to true.

SOLUTIONS:

Setter's Solution (c++)
  const int mx=520;
  vector<int>gi[mx],go[mx];
  int c[mx];
  int color[mx];
  void dfs(int u, Dinic &din){
    for(int v:go[u]){
      if(color[v]==-1){
        color[v]=0;
        color[v^1]=1;
        dfs(v,din);
      }
      assert(color[v]==0);
      din.AddEdge(u,v,INF);
    }
    for(int v:gi[u]){
      if(color[v]==-1){
        color[v]=0;
        color[v^1]=1;
        dfs(v,din);
      }
      assert(color[v]==0);
      din.AddEdge(v,u,INF);
    }
  }
  int main(){
    int t=rint('\n');
    int sm=0;
    for(int tt=1;tt<=t;tt++){
      cerr<<"tc"<<tt<<endl;
      int n=rint(' ');
      assert(1<=n && n<=256);
      int m=rint('\n');
      sm+=m;
      assert(1<=sm&&sm<=43210);
      string s=rword('\n');
      assert(s.size()==n);
      for(char ch:s)assert(ch=='0' || ch=='1');
      for(int i=0;i<n;i++){
        c[i]=rint(i==n-1?'\n':' ');
        assert(1<=c[i] && c[i]<=256);
      }

      for(int i=0;i<n+n;i++){
        gi[i].clear();
        go[i].clear();
        color[i]=-1;
      }
      for(int i=0;i<m;i++){
        int p=rint(' ');
        int q=rint('\n');
        assert(-n<=p && p<=n && p!=0);
        assert(-n<=q && q<=n && q!=0);
        p=normalize(p);
        q=normalize(q);
        p^=1;
        //p -> q
        go[p].push_back(q);
        gi[q].push_back(p);
        //-q -> -p
        go[q^1].push_back(p^1);
        gi[p^1].push_back(q^1);
      }
      Dinic din(n+n+2);    
      for(int i=0;i<n+n;i++){
        if(color[i]==-1){
          color[i]=0;
          color[i^1]=1;
          dfs(i,din);
        }
      }
      int src=n+n;
      int snk=src+1;
      for(int i=0;i<n+n;i++){
        if(color[i]==0){
          int val=s[i/2]-'0';
          int cost=c[i/2];
          if(i%2==1)val^=1;
          if(val==1){
            din.AddEdge(src,i,cost);
          }
          else{
            din.AddEdge(i,snk,cost);
          }
        }
      }
      int ans=din.MaxFlow(src,snk);
      printf("%d\n",ans);
    }
    return 0;
  }

Note that there are at most N^2 different clauses, so the first subtask can be solved by trying all possible values of the variables, and check which of them satisfy the expression.

Setter's solution, first subtask
  #include<bits/stdc++.h>
  using namespace std;
  typedef long long int uli;
  const int mx=520;
  char s0[mx];
  int val0[mx],val[mx];

  int c[mx];
  int normalize(int x){
    int b=0;
    if(x<0)x=-x,b=1;
    return ((x-1)*2)^b;
  }

  int main(){
    int t;
    scanf("%d",&t);
    while(t--){
      int n,m;
      scanf("%d %d %s",&n,&m,s0);
      for(int i=0;i<n;i++){
        val0[i+i]=s0[i]-'0';
        val0[i+i+1]=(val0[i+i]^1);
      }
      for(int i=0;i<n;i++)scanf("%d",c+i);
      set<pair<int,int> >e;
      for(int i=0;i<m;i++){
        int u,v;
        scanf("%d %d",&u,&v);
        u=normalize(u);      
        v=normalize(v);
        e.insert({u,v});
      }
      int ans=1e9;
      for(int b=0;b<(1<<n);b++){
        for(int i=0;i<n;i++){
          val[i+i]=0;
          if(b&(1<<i))val[i+i]=1;
          val[i+i+1]=(val[i+i]^1);
        }
        int x=1;
        for(auto par:e){
          int u=par.first;
          int v=par.second;
          x&=(val[u]|val[v]);
        }
        if(x){
          int cost=0;
          for(int i=0;i<n;i++){
            if(val[i+i]!=val0[i+i]){
              cost+=c[i];
            }
          }
          ans=min(ans,cost);
        }
      }
      printf("%d\n",ans);
    }
    return 0;
  }
Tester's solution
  int main(int argc, char** argv) 
  {
    int T = readIntLn(1, 100'000);
    int sumM =0;
    forn(tc, T)
    {
      int N = readIntSp(1, 256);
      int M = readIntLn(1, 43210);
      sumM+=M;
      string S = readStringLn(N, N);
      vector<int> C(N);
      forn(i, N)
      {
        if (i + 1 == N)
          C[i] = readIntLn(1, 256);
        else
          C[i] = readIntSp(1, 256);
      }
      vector<pair<int, int> > expr(M);
      forn(i, M)
      {
        expr[i].first = readIntSp(-1 * N, N);
        expr[i].second = readIntLn(-1 * N, N);
      }
      //assign colour
      vector<vector<bool>> same(N, vector<bool>(N));
      vector<vector<bool>> opp(N, vector<bool>(N));
      for (auto e : expr)
      {
        int a = abs(e.first)-1;
        int b = abs(e.second)-1;
        if ((e.first < 0) != (e.second < 0))
        {
          same[a][b] = true;
          same[b][a] = true;
        }
        else
        {
          opp[a][b] = true;
          opp[b][a] = true;
        }
      }

      vector<bool> color(N);
      vector<bool> visited(N);
      forn(i, N)
      {
        if (!visited[i])
        {
          visited[i] = true;
          vector<int> q(1, i+1);
          forn(j, q.size())
          {
            int act = abs(q[j])-1;
            bool d = q[j] < 0;
            const auto& sa = same[act];
            const auto& op = opp[act];

            forn(k, N)
            {
              if ((sa[k] || op[k]) && !visited[k])
              {
                visited[k] = true;
                color[k] = d ^ op[k];
                q.push_back((k+1)*(color[k]?-1:1));
              }
            }
          }
        }
      }
      
      //build graph from one of the colors
      vector<vector<int>> g(N + 2, vector<int> (N+2));
      const uint32_t INF = 1 << 18;

      for (auto e : expr)
      {
        int a = abs(e.first) - 1;
        int b = abs(e.second) - 1;
        bool d = e.first < 0;
        if (color[a] ^ d)
          g[b][a] = INF;
        else
          g[a][b] = INF;
      }

      forn(i, N)
      {
        int val = S[i] - '0';
        assert(val == 0 || val == 1);
        if (val == color[i])
        {
          g[N][i] = C[i];
        }
        else
        {
          g[i][N + 1] = C[i];
        }
      }

      //calc
      vector<vector<int> > res = g;
      
      vector<vector<int> > preflow(N+2, vector<int>(N+2));
      
      vector<int> e(N + 2);
      vector<int> h(N+2);
      h[N] = N+2;
      
      forn(i, N)
      {
        if (res[N][i] > 0)
        {
          res[N][i] = 0;
          res[i][N] = g[N][i];
          preflow[N][i] = g[N][i];
          e[i] += g[N][i];
        }
      }
        
      int ctr = 1;
      while (ctr)
      {
        ctr = 0;
        forn(i,N) if (e[i])
        {
          ++ctr;
          bool found = false;
          int mir = 2 * N + 2;
          forn(j, N+2)
          {
            if (res[i][j] && h[i] == h[j] + 1)
            {
              int mi = min(res[i][j], e[i]);
              if (preflow[j][i] == 0)
                preflow[i][j] += mi;
              else
                preflow[j][i] -= mi;
              res[i][j] -= mi;
              res[j][i] += mi;
              e[i] -= mi;
              e[j] += mi;
              found = true;
            }
            if (res[i][j])
            {
              mir = min(mir, h[j] + 1);
            }
          }
          if (!found)
            h[i] = mir;
        }
      }
      int answer = 0;
      forn(i, N)
        answer += preflow[N][i];

      printf("%d\n", answer);

    }
    assert(getchar() == -1);
    assert(sumM<=43210);
    return 0;
  }

About RB2CNF

A long long ago, I sent an approximate problem based in the fact that in general there is no polynomial algorithm to find the minimum cost to change variables and make a 2CNF expression evaluate to true. In the original problem the boolean expression was constructed from a geometrical setting, and there was no colours red-black. However the graph had similar properties, and our super admin Alexey found the described mincut solution!

VIDEO EDITORIAL:

3 Likes