2013-05-27 21:45:11Morris

[UVA][2SAT] 10319 - Manhattan

Problem H

Manhattan

Input: standard input

Output:  standard output

Time Limit: 1 second

Memory Limit: 32 MB

 

 

You are the mayor of a city with severe traffic problems.To deal with the situation, you have decided to make a new plan for the street grid.As it is impossible to make the streets wider, your approach is to make themone-way (only traffic in one direction is allowed on a street), thus creating amore efficient flow of traffic.

 

The streets in the city form an orthogonal grid - like on Manhattanavenues run in north-south-direction, while streets run in east-west-direction.Your mission is to make all the streets and avenues one-way, i.e. fix thedirection in which traffic is allowed, while maintaining a short drivingdistance between some ordered pairs of locations. More specifically, a route inthe city is defined by two street-avenue crossings, the start and goallocation. On a one-way street grid, a route has a legal path if it is possibleto drive from the start location to the goal location along the path passingstreets and avenues in their prescribed direction only. A route does not definea specific path between the two locations - there may be many possible pathsfor each route. A legal path in a one-way street grid is considered simple ifit requires at most one turn, i.e. a maximum of one street and one avenue needto be used for the path.

 

When traveling by car from one location to another, asimple path will be preferred over a non-simple one, since it is faster.However, as each street in the grid is one-way, there may always be routes forwhich no simple path exists. On your desk lies a list of important routes whichyou want to have simple paths after the re-design of the street grid.

 

Your task is to write a program that determines if it ispossible to fix the directions of the one-way streets and avenues in such a waythat each route in the list has at least one simple path.

 

Input

On the first line of the input, there is a single integer n, telling how many city descriptionsthat follows. Each city description begins with a line containing threeintegers: the number of streets 0<S<=30and avenues 0<A<=30 in thestreet grid, and the number of routes 0<m<=200that should have at least one simple path. The next m lines define these routes, one on each line. Each routedefinition consists of four integers, s1,a1, s2, a2, where the startlocation of the route is at the crossing of street s1 and avenue a1, andthe goal location is at the crossing of street s2 and avenue a2. Obviously,0<s1, s2<=S and 0<a1, a2<=A.

 

Output

For each city, your program should output 'Yes' on a single line if it ispossible to make the streets and avenues one-way, so that each route has atleast one simple path. Otherwise the text 'No'should be printed on a line of its own.

 

SampleInput

3

6 6 2

1 1 6 6

6 6 1 1

7 7 4

1 1 1 6

6 1 6 6

6 6 1 1

4 3 5 1

9 8 6

2 2 4 4

4 5 3 2

3 4 2 2

3 2 4 4

4 5 2 2

2 1 3 4

 

Sample Output

Yes

No

No


(The Decider Contest, Problem Source: Swedish National ProgrammingContest, arranged by department of Computer Science at Lund Institute ofTechnology.)

題目描述://這題稍微麻煩了點

現在是一個網格的路徑,每條路徑都是單行道,身為市長你,要求幾個起點到終點都要有一個簡單路徑,
這個簡單路徑的定義:最多只能轉彎一次。(即要碼一條道路到達,不然就經過兩條道路抵達。)

題目解法:2-SAT

設想每條橫向(←→)道路,向左向右表示成 False or True // 順序自己定奪

同理每條縱向(↑↓)道路,向上向下表示成 False or True // 順序自己定奪

當要求 (s1,a1)->(s2,a2)

即 (s1 and a2) or (s2 and a1), 但 2-SAT 的模型是先個別 or 然後 and.

因此將其藉由布林轉換成
2-SAT model: (s1 or a1) and (s2 or a2) and (a1 or a2) and (s1 or s2)

然後建圖,利用 SCC 將點縮起來,形成 DAG 圖。

如果 val 與 !val 被縮在同一個點,即為矛盾。
當關係為 (a or b) and (c or !d) and ...

建圖方式如下:
!a -> b // 為滿足 a or b = true, a = false 時,推論 b = true
!b -> a // 為滿足 a or b = true, b = false 時,推論 a = true
d -> c // 為滿足 c or !d = true, d = true 時,推論 c = true
!c -> !d // 為滿足 c or !d = true, c = false 時,推論 d = false
....

#include <stdio.h>
#include <vector>
#include <algorithm>
#include <string.h>
using namespace std;
vector<int> g[1005];
int vfind[1005], findIdx;
int stk[1005], stkIdx;
int in_stk[1005], visited[1005];
int contract[1005];
int scc_cnt;
int scc(int nd) {
    in_stk[nd] = visited[nd] = 1;
    stk[++stkIdx] = nd;
    vfind[nd] = ++findIdx;
    int mn = vfind[nd];
    for(int i = 0; i < g[nd].size(); i++) {
        if(!visited[g[nd][i]])
            mn = min(mn, scc(g[nd][i]));
        if(in_stk[g[nd][i]])
            mn = min(mn, vfind[g[nd][i]]);
    }
    if(mn == vfind[nd]) {
        do {
            in_stk[stk[stkIdx]] = 0;
            contract[stk[stkIdx]] = nd;
        } while(stk[stkIdx--] != nd);
        scc_cnt++;
    }
    return mn;
}
int main() {
    int testcase, S, A, m, i, j;
    int s1, s2, a1, a2;
    scanf("%d", &testcase);
    while(testcase--) {
        scanf("%d %d %d", &S, &A, &m);
        int n = (S+A)*2;
        for(i = 0; i < n; i++)
            g[i].clear();
        // 2*node: false, 2*node+1: true
        while(m--) {
            scanf("%d %d %d %d", &s1, &a1, &s2, &a2);
            s1--, a1--, s2--, a2--;
            s1 <<= 1, a1 <<= 1;
            s2 <<= 1, a2 <<= 1;
            a1 += 2*S, a2 += 2*S;
            if(a1 > a2) s1 ^= 1, s2 ^= 1;
            if(s1 > s2) a1 ^= 1, a2 ^= 1;
            if(s1 == s2) {
                g[s1^1].push_back(s2);
                continue;
            }
            if(a1 == a2) {
                g[a1^1].push_back(a2);
                continue;
            }
            //(s1,a1)->(s2,a2)
            //transform: (s1 and a2) or (s2 and a1)
            //to 2-SAT model: (s1 or a1) and (s2 or a2) and (a1 or a2) and (s1 or s2)
            g[s1^1].push_back(a1);
            g[a1^1].push_back(s1);

            g[s2^1].push_back(a2);
            g[a2^1].push_back(s2);

            g[a1^1].push_back(a2);
            g[a2^1].push_back(a1);

            g[s2^1].push_back(s1);
            g[s1^1].push_back(s2);
        }
        //SCC
        memset(visited, 0, sizeof(visited));
        memset(in_stk, 0, sizeof(in_stk));
        scc_cnt = 1;
        for(i = 0; i < n; i++) {
            if(!visited[i]) {
                stkIdx = 0;
                findIdx = 0;
                scc(i);
            }
        }
        //2-SAT check
        int hasSol = 1;
        for(i = 0; i < n && hasSol; i+=2)
            if(contract[i] == contract[i^1])
                hasSol = 0;
        puts(hasSol ? "Yes" : "No");
    }
    return 0;
}