2 - sat 의 건설 방법 및 해결 방안

2 - sat 의 건설 방법 및 해결 방안
이 글 은 오리지널 이 아니 라 오리지널 에 경 의 를 표 한다.전달 하 다https://blog.csdn.net/qq_24451605/article/details/47126143
2 - sat 문제 에 대한 설명
하나의 서열 을 제시 합 니 다. 모든 수 는 하나의 bool 값 이 고 제한 관 계 를 제시 합 니 다. 최종 적 으로 풀 수 있 는 문 제 를 적응성 문제 라 고 합 니 다. 즉, sat 문제 입 니 다. 2 - sat 문 제 는 제 시 된 제한 이 가장 많은 두 요소 간 의 제한 입 니 다.이런 적응성 문제 의 해결 역시 우리 가 이미 알 고 있 는 도 론 모델 로 추상 화 할 수 있다.
2 - sat 문제 의 건설 방법
1. 우 리 는 방향 이 있 는 쪽 을 이용한다.

(1）    A B     ，A B     ，(A and B)||(!A and !B )==true    A   B，      

 (2）    A B     ， A   B，  (A && !B)||(!A && B )==true,   

(3）     A,  A==true,  

(4）  A     ，  !A==true.  

이렇게 그림 을 만 든 후에 방향 그림 이 나타 날 것 이다. 이 방향 그림 은 하나의 연결 고 리 를 초래 하고 특정한 점 을 선택 하면 이 체인 의 모든 점 이 선택 된다.만약 에 우리 가 강 한 연결 분량 을 찾 으 면 이 강 한 연결 분량 중의 점 을 선택 할 때 반드시 모두 선택해 야 한다. 선택 하지 않 으 면 모두 선택 하지 않 을 것 이다. 그래서 이 그림 에 연 결 된 점 을 만족 시 키 면 i 와 i 가 동시에 선택 되 지 않 을 것 이다. 만약 에 갈등 이 존재 하지 않 는 다 면 현재 문 제 는 해결 할 수 있다.그러나 구 해 과정 에서 우리 가 요구 하 는 해 는 일부 성질 을 요구 하기 때문에 다음 과 같은 몇 가지 해결 방안 을 제공한다.
2 - sat 문제 해결 방안
1. 사전 순 서 를 최소 화 하 는 방법: 폭력 dfs 풀이 (복잡 도 O (N * M)
2. 현재 의 2 - sa 문제 t 가 풀 렸 는 지 판단: tarjan 강 한 연결 점, 판단 추가 (복잡 도 O (N + M)
3. 현재 의 2 - sat 문제 의 임의의 그룹 해 를 구하 십시오: tarjan 강 연통 축소 점 + 토폴로지 정렬 + 구축 그룹 해 (복잡 도 O (N + M)
사전 순 서 를 최소 화 하 는 폭력 적 인 방법 을 구하 다.
알고리즘 사상:
1. 먼저 우리 가 필요 로 하 는 배열 을 정의 합 니 다. mark 배열 은 특정한 점 이 선택 되 었 는 지 여 부 를 표시 하 는 데 사 용 됩 니 다. 서열 중의 한 수 에 대해 우 리 는 두 개의 점 i 와 i 로 분해 할 것 입 니 다. 그래서 우 리 는 mark 배열 을 이용 하여 표 시 를 할 때 다음 과 같은 표기 방법 을 사용 합 니 다.
mark [i < 1] 은 i 를 나타 내 고 mark [1 | 1] 은 i 를 나타 낸다.
이번 표 시 된 점 을 저장 하기 위 한 대기 열 s
2. 각 점 을 매 거 한 다음 에 현재 점 에서 분 리 된 두 점 중 하나 가 선택 되 었 는 지 판단 합 니 다. 있 으 면 다음 점 을 계속 매 거 합 니 다. 표시 되 지 않 으 면 조작 3 으로 이동 합 니 다.
3. 만약 에 어떤 점 에서 떼 어 낸 두 점 이 모두 표시 되 지 않 았 다 면 우 리 는 먼저 첫 번 째 점 을 표시 하려 고 합 니 다. 만약 에 첫 번 째 점 을 표시 하면 일부 점 이 반드시 표시 되 어야 하기 때문에 dfs 를 한 다음 에 과정 에서 갈등 이 발생 하 는 지 판단 해 야 합 니 다. 만약 에 발생 하면 이번 표 시 된 점 을 모두 복원 한 다음 에 두 번 째 점 과 한 가지 상황 이 남 습 니 다. 그래서 저 는...두 번 째 상황 을 살 펴 보고 갈등 이 생기 면 문제 가 풀 리 지 않 습 니 다. 끝 알고리즘 이 현재 성공 적 으로 표시 되면 모든 점 알고리즘 이 끝 날 때 까지 2 처럼 매 거 집 니 다.
4. 매번 dfs 의 과정 에서 현재 점 이 도달 할 수 있 는 점 을 모두 표시 하기 때문에 그 다음 에 표 시 를 하 는 과정 에서 표 시 된 점 이 하나 있 기 때문에 선택 하지 않 으 면 모든 점 이 선택 되 지 않 고 그 점 과 같은 기원 을 가 진 점 이 반드시 선택 되 기 때문에 일단 선택 되 었 을 때 풀 리 는 상황 이 발생 하지 않 으 면 현재 상황 은 반드시 풀 리 지 않 습 니 다.매번 하 는 작업 은 그림 의 점 이 변 하지 않 거나 전체적인 색 이 반전 할 수 있 기 때문에 새로운 염색 의 점 두 가지 선택 만 하면 된다. 얻 은 결 과 는 두 가지 뿐 이 고 반전 작업 을 동시에 하 는 것 은 하지 않 은 효과 와 같 기 때문이다.
5. 깊 은 검색 순서 에 따라 만 들 었 기 때문에 해 를 얻 는 것 은 사전 순서 가 가장 작은 것 이 분명 합 니 다.
코드 는 다음 과 같 습 니 다:

struct TwoSat  
{  
    int n;  
    vector<int> e[MAX<<1];  
    int s[MAX<<1],c;  
    bool mark[MAX<<1];  
    //mark[i<<1]    1，   i     
    //mark[i<<1|1]    1，   i       
    bool dfs ( int x )  
    //                       
    {  
        //                 
        if ( mark[x^1] ) return false;  
        //           ，            
        //        
        if ( mark[x] ) return true;  
        //         ，     ，      
        mark[x] = true;  
        //               
        s[c++] = x;  
        //         ，         
        for ( int i = 0 ; i if ( !dfs( e[x][i] ))  
                return false;  
        return true;  
    }  

    void init ( int n )  
    {  
        this->n = n;  
        for ( int i = 0 ; i < 2*n ; i++ )  
            e[i].clear();  
        memset ( mark , 0 , sizeof ( mark ));  
    }  

    void add ( int x , int y )  
    {  
        e[x].push_back ( y^1 ); //            
        e[y].push_back ( x^1 );  
    }  

    bool solve ( )  
    {  
        for ( int i = 0 ; i < 2*n ; i += 2 )  
            if ( !mark[i] && !mark[i+1] )  
            {  
                c = 0;  
                if ( !dfs(i) )  
                {  
                    //    ，                 
                    //    
                    while ( c > 0 ) mark[s[--c]]= false;  
                    if ( !dfs(i+1) )  return false;  
                }  
            }  
        return true;  
    }  

강 한 연결 점 을 이용 하여 2 - sat 문제 가 풀 렸 는 지 판단 합 니 다.
알고리즘 사상:
1. 강 한 연결 점 을 이용 하여 DAG (방향 무 환 도) 를 얻 을 수 있 습 니 다.
2. 그 다음 에 모든 강 한 연결 분량 중에서 모든 점 을 선택 하면 같이 선택 하고 선택 하지 않 으 면 같이 선택 하지 않 기 때문에 i 와 i '가 하나의 강 한 연결 분량 에 동시에 존재 한다 면 반드시 풀 리 지 않 을 것 이다.
3. 만약 에 강연 통 분량 내부 에 모순 이 생기 지 않 는 다 면 나머지 는 바로 이 유향 무 환 도 입 니 다. 유향 무 환 도가 있 기 때문에 토폴로지 순 서 를 매 길 수 있 기 때문에 서로 다른 색 을 번갈아 염색 하면 하나의 해 를 얻 을 수 있 습 니 다. 그래서 강연 통 분량 내부 에 모순 이 나타 나 지 않 는 다 면 반드시 해 가 있 을 것 입 니 다.
주 코드 는 다음 과 같 습 니 다.

 for ( int i = 0 ; i < 2*n ; i++ )  
        if ( !mark[i] ) tarjan ( i );  

    for ( int i = 0 ; i < n ; i++ )  
        if ( belong[i<<1] == belong[i<<1|1] )  
            return false;  
    return true;  

tarjan 강 연통 축소 점 재발 급:

void tarjan ( int u )  
{  
    dfn[u] = low[u] = ++times;  
    mark[u] = 1;  
    s.push ( u );  
    int len = e[u].size();  
    for ( int i= 0 ; i < len ; i++ )  
    {  
        int v = e[u][i];  
        if ( !mark[v] )  
        {  
            tarjan ( v );  
            low[u] = min ( low[u] , low[v] );  
        }  
        if ( mark[v] == 1 )  
            low[u] = min ( low[u] , dfn[v] );  
    }  
    if ( dfn[u] == low[u] )  
    {  
        int temp;  
        do  
        {  
            temp = s.top();  
            belong[temp] = cnt;  
            mark[temp] = 2;  
            s.pop();  
        }while ( temp != u );  
        cnt++;  
    }  
}  

토폴로지 순서에 따라 임의의 조 해 를 구하 다.
1. 우선 강 한 연결 점 을 진행 해 야 합 니 다. DAG 를 얻 을 수 있 습 니 다.
2. 그리고 우 리 는 새로 얻 은 그림 속 의 모순 관 계 를 얻어 야 한다. 즉, i 와 i 가 있 는 강 한 연결 분량 은 모순 이다.
3. 그 다음 에 우 리 는 DAG 를 염색 하고 토폴로지 순 서 를 매 기 는 과정 에서 염색 을 한다. 만약 에 어떤 점 이 염색 되 지 않 았 다 면 1 로 염색 하고 그 와 모순 되 는 점 을 2 로 염색한다. 모순 관 계 는 두 개의 관계 이기 때문에 다른 점 과 갈등 이 생기 지 않 는 다.
4. 그러면 토폴로지 정렬 이 끝 난 후에 모든 점 을 염색 합 니 다. 토폴로지 는 무 환 도 에 있 는 좋 은 옮 겨 다 니 는 방식 일 뿐 입 니 다.
코드 는 다음 과 같 습 니 다:

void topsort ( )  
{  
    int i,j;  
    queue<int> q;  
    for ( int i = 1 ; i < t ; i++ )  
    {  
        if (!in[i])  
            q.push ( i );  
    }  
    while (!q.empty())  
    {  
        int u = q.front();  
        q.pop();  
        if ( !col[u] )  
        {  
            col[u] = 1;  
            col[conflict[u]] = 2;  
        }  
        for ( int i = 0 ; i < g[u].size(); i++ )  
        {  
            int v = g[u][i];  
            in[v]--;  
            if ( !in[v] ) q.push ( v );  
        }  
    }  
}