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
TrueandFalse. - Add an edge from Y_i to Z_i with infinite capacity.
- Add an edge from
Trueto 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
Trueto P means changing the value of P to false. But since P is now false should we add an edge from P toFalse? it turns out that even if we add such edge,TrueandFalsewill be still disconnected, because if there is another path fromTruetoP, 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
Falsemeans 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!