# RB2CNF - Editorial

Author & Editorialist: Alei Reyes
Tester: Istvan Nagy

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);
}
for(int v:gi[u]){
if(color[v]==-1){
color[v]=0;
color[v^1]=1;
dfs(v,din);
}
assert(color[v]==0);
}
}
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){
}
else{
}
}
}
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.

  #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 sumM =0;
forn(tc, T)
{
sumM+=M;
vector<int> C(N);
forn(i, N)
{
if (i + 1 == N)
else
}
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;
}
}
forn(i, N)

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