I actually got accepted on most of these problems, but they're shown as "red", why is that?

# | User | Rating |
---|---|---|

1 | tourist | 3434 |

2 | OO0OOO00O0OOO0O0…O | 3280 |

3 | Syloviaely | 3274 |

4 | Petr | 3233 |

5 | Um_nik | 3213 |

6 | ko_osaga | 3124 |

7 | Benq | 3105 |

8 | Swistakk | 3092 |

9 | fjzzq2002 | 3055 |

10 | anta | 3053 |

# | User | Contrib. |
---|---|---|

1 | Radewoosh | 173 |

2 | rng_58 | 162 |

3 | tourist | 159 |

4 | Petr | 153 |

5 | Swistakk | 152 |

6 | csacademy | 151 |

7 | Vovuh | 145 |

7 | Um_nik | 145 |

9 | Errichto | 144 |

10 | PikMike | 143 |

I actually got accepted on most of these problems, but they're shown as "red", why is that?

Hi codeforces community.

I thought there is no good *2-SAT* tutorial in the internet, so I decided to write one.

*2-SAT* is a special case of boolean satisfiability.

Good question! Boolean satisfiability or just *SAT* determines whether we can give values (`TRUE` or `FALSE` only) to each boolean variable in such a way that the value of the formula become `TRUE` or not. If we can do so, we call formula *satisfiable*, otherwise we call it *unsatisfiable*. Look at the example below:

*f* = *A* ∧ ¬*B*, is *satisfiable*, cause A = `TRUE` and B = `FALSE` makes it `TRUE`.

but *g* = *A* ∧ ¬*A*, is *unsatisfiable*, look at this table:

A | ¬A | A ∧ ¬A |

TRUE | FALSE | FALSE |

FALSE | TRUE | FALSE |

As you can see *g* is *unsatisfiable* cause whatever values of its boolean variables are, *g* is `FALSE`.

**Note:** ¬ in ¬*X* is boolean *not* operation. ∧ in *X* ∧ *Y* is boolean *and* operation and finally ∨ in *X* ∨ *Y* is boolean *or* operation.

*SAT* is a `NP-Complete`

problem, though we can solve *1-SAT* and *2-SAT* problems in a polynomial time.

**Note:** This doesn't really exist, I define it cause it help understanding *2-SAT*.

Consider *f* = *x*_{1} ∧ *x*_{2} ∧ ... ∧ *x*_{n}.

**Problem:** Is *f* *satisfiable*?

**Solution:** Well *1-SAT* is an easy problem, if there aren't both of *x*_{i} and ¬*x*_{i} in *f*, then *f* is *satisfiable*, otherwise it's not.

Consider *f* = (*x*_{1} ∨ *y*_{1}) ∧ (*x*_{2} ∨ *y*_{2}) ∧ ... ∧ (*x*_{n} ∨ *y*_{n}).

**Problem:** Is *f* *satisfiable*?

But how to solve this problem? *x*_{i} ∨ *y*_{i} and and are all equivalent. So we convert each of (*x*_{i} ∨ *y*_{i}) s into those two statements.

Now consider a graph with 2*n* vertices; For each of (*x*_{i} ∨ *y*_{i}) s we add two directed edges

From ¬

*x*_{i}to*y*_{i}From ¬

*y*_{i}to*x*_{i}

*f* is not *satisfiable* if both ¬*x*_{i} and *x*_{i} are in the same SCC (Strongly Connected Component) (Why?) Checking this can be done with a simple Kosaraju's Algorithm.

Assume that *f* is *satisfiable*. Now we want to give values to each variable in order to satisfy *f*. It can be done with a topological sort of vertices of the graph we made. If ¬*x*_{i} is after *x*_{i} in topological sort, *x*_{i} should be `FALSE`. It should be `TRUE` otherwise.

Some problems:

- SPOJ — BUGLIFE
- SPOJ — TORNJEVI
- UVa — Manhattan
- UVa — Wedding
- CF — The Road to Berland is Paved With Good Intentions
- CF — Ring Road 2
- CF — TROY Query
- CEOI — Birthday party — Solution

```
func dfsFirst(vertex v):
marked[v] = true
for each vertex u adjacent to v do:
if not marked[u]:
dfsFirst(u)
stack.push(v)
func dfsSecond(vertex v):
marked[v] = true
for each vertex u adjacent to v do:
if not marked[u]:
dfsSecond(u)
component[v] = counter
for i = 1 to n do:
addEdge(not x[i], y[i])
addEdge(not y[i], x[i])
for i = 1 to n do:
if not marked[x[i]]:
dfsFirst(x[i])
if not marked[y[i]]:
dfsFirst(y[i])
if not marked[not x[i]]:
dfsFirst(not x[i])
if not marked[not y[i]]:
dfsFirst(not y[i])
set all marked values false
counter = 0
flip directions of edges // change v -> u to u -> v
while stack is not empty do:
v = stack.pop
if not marked[v]
counter = counter + 1
dfsSecond(v)
for i = 1 to n do:
if component[x[i]] == component[not x[i]]:
it is unsatisfiable
exit
if component[y[i]] == component[not y[i]]:
it is unsatisfiable
exit
it is satisfiable
exit
```

WARNING: Many of these things belong to C++11 so use C++11 in order to test anything here :)

I just write a short version for this article, because it's now in the main page. I recommend you to click on "Read more »" and read more :) Here is a short trick for the short version:

I see lots of programmers write code like this one:

```
pair<int, int> p;
vector<int> v;
// ...
p = make_pair(3, 4);
v.push_back(4); v.push_back(5);
```

while you can just do this:

```
pair<int, int> p;
vector<int> v;
// ...
p = {3, 4};
v = {4, 5};
```

Discussion of Delete2

Codeforces (c) Copyright 2010-2018 Mike Mirzayanov

The only programming contests Web 2.0 platform

Server time: Aug/21/2018 21:30:28 (f2).

Desktop version, switch to mobile version.

User lists

Name |
---|