cnf_sat.txt

此算法能在多项式时间里判定任一给定的2CNF公式是否可满足。是算法中的一个重要问题。

package CNF_SAT
import java.io.IOException;
import java.io.RandomAccessFile;
/**
 * @author yyzhao
 *
 * TODO To change the template for this generated type comment go to
 * Window - Preferences - Java - Code Style - Code Templates
 */
public class DFS {
	
	private int m;//表示变量数
	private int n;//表示布尔表达式数
	private int neighbor[][];//表示结点之间邻接关系的矩阵
	private int visited[];//记录深度优先搜索中结点被访问的次序的矩阵
	private int b[];
	private int grt[];//记录每一次深度优先搜索的连通分量
	int count = 1;
	
	DFS(String  file) {//读输入矩阵建造邻接矩阵
		try{
		RandomAccessFile ra1 = new RandomAccessFile(file, "r");
		String s = ra1.readLine() ;
		int k = s.indexOf(",");
		m = Integer.parseInt(s.substring(0,k));
		n = Integer.parseInt(s.substring(k+1,s.length()));
		
		neighbor = new int[2*m][2*m];
		visited = new int[2*m];
		grt = new int[2*m];
		for(int p = 0;p < 2*m;p++)//为邻接矩阵赋初值为-1
			for (int q = 0;q < 2*m;q++)
				neighbor[p][q]=-1;
		
		for(int r = 0;r < 2*m;r++)
			visited[r] = 0;
		
		b=new int[2*m];
		for(int i=0;i<2*m;i++)
			b[i]=i+1;
		
		for(int i=0;i<n;i++){
			s=ra1.readLine();
			k=s.indexOf(",");
			int x = Integer.parseInt(s.substring(0,k));
			int y = Integer.parseInt(s.substring(k+1,s.length()));
			//System.out.println(x);
			//System.out.println(y);
			x = -x;
			if(x<0&&y<0)
				neighbor[-2*x-1][-2*y-1]=1;
			else{
				if(x<0&&y>0)
					neighbor[-2*x-1][2*y-1-1]=1;
				else{
					if(x>0&&y<0)
						neighbor[2*x-1-1][-2*y-1]=1;
					else{
						if(x>0&&y>0)
							neighbor[2*x-1-1][2*y-1-1]=1;
					}	
				}
			}
			x = -x;
			y = -y;
			if(x<0&&y<0)
				neighbor[-2*y-1][-2*x-1]=1;
			else{
				if(y<0&&x>0)
					neighbor[-2*y-1][2*x-1-1]=1;
				else{
					if(y>0&&x<0)
						neighbor[2*y-1-1][-2*x-1]=1;
					else{
						if(x>0&&y>0)
							neighbor[2*y-1-1][2*x-1-1]=1;
					}
		}
				}
		}
		}catch (IOException e) {
			e.printStackTrace();
		}
		
	}
	
	public void display(){
		//System.out.println(m);
		//System.out.println(n);
		for(int p = 0;p < 2*m;p++){
			for (int q = 0;q < 2*m;q++)
				System.out.print(neighbor[p][q]+",");
			System.out.println();
		}
		//for(int r = 0;r < 2*m;r++)
			//System.out.print(visited[r]+",");
		
	}
	
	int GetFirstNeighbor(int v){
		for(int i=0;i<2*m;i++){
			if(neighbor[v-1][i]!=-1)
				return i+1;
		}
		return -1;
	}
	
	int GetNextNeighbor(int v,int w){
		for(int i=w+1;i<2*m;i++){
			if(neighbor[v-1][i-1]!=-1)
				return i;
		}
		return -1;
	}
	
	public int dfs(int v){//深度优先搜索
		for(int i=0;i<2*m;i++)
			grt[i]=0;
		visited[v-1]=count;
		grt[v-1]=count;
		count++;
		//System.out.println(v);
		int w = GetFirstNeighbor(v);
		while(w!=-1){
			if(visited[w-1]==0)
				dfs(w);
			w = GetNextNeighbor(v,w);			
		}
		return count;
		/*if(count<m){
			int next=0;
			for(int i=0;i<2*m;i++)
				{if(visited[i]!=0)
					next=i+1;
				  break;}
			dfs(next,count);
				
		}*/
		
	}

	void inverse()//求逆矩阵
	{
		int i,j,k;
		for(i=0;i<2*m;i++)
			for(j=i+1;j<2*m;j++)
			{
				k=neighbor[i][j];
				neighbor[i][j]=neighbor[j][i];
				neighbor[j][i]=k;
			}
	}

	public boolean CNF_SAT(){
		dfs(3);	//任选一个接点做深度优先搜索，本次实验取3
		for(int i=0;i<2*m;i++){//将深度优先搜索的顺序储存在b[]中
			int t=visited[i];
			b[t-1]=i+1;
		}
		
		for(int i=0;i<2*m;i++)//将记录结点是否被访问过的数组visited[]重新赋值为0
			visited[i]=0;	
		inverse();
		count=1;
		
		int sum=0;
		while(sum<2*m){
			int x=0;
			for(int j=2*m-1;j>=0;j--){
				//System.out.println(b[j]-1);
				if(visited[b[j]-1]==0)
				{x=b[j];
				break;
				}
			}
		sum=sum+dfs(x);
		
		for(int i=0;i<2*m;i++)//判断强连通分支中是否同时出现v2i-1和v21，若同时出现则不可满足
			if(grt[i]!=0)
			{if((i+1)%2==0&&grt[i-1]!=0)
				return false;
			if((i+1)%2!=0&&grt[i+1]!=0)
				return false;	
			}
			
			
		}
		return true;
	}
	
	public static void main(String[] args) {
		
		DFS d = new DFS("e:/input.txt");//读输入矩阵建造邻接矩阵
	    System.out.println(d.CNF_SAT());    
	}
}