帮助Tabu搜索布尔可满足性 [英] Help with Tabu Search for Boolean Satisfiability

问题描述

你好，我是这个整个坐着解决者的新手。我的任务是读入带有子句的CNF文件，然后解决或提出文字的真值。我读取CNF文件并将其复制到2D阵列。怎么办？如何使用数组进行禁忌搜索。我想用禁忌搜索来解决它。我从哪里开始？任何帮助都非常感谢。这是读取CNF文件的类。我有一个发送cnf文件的演示类和一个什么都没有的解算器类。

Hello, I am new to this whole sat solver thing. My assignment is to read in a CNF file with clauses and then solve or come up with the truth values for the literals. I read the CNF file and copied it to the 2D array. Now what? How do I use the array for tabu search. I want to solve it using tabu search. Where do I start? Any help is highly appreciated. This the class that reads the CNF file. I have a demo class that sends in the cnf file and a solver class that has nothing.

import java.util.ArrayList;
import java.util.Arrays;
import java.util.Scanner;
import java.util.regex.MatchResult;
import java.io.*;

public class FileRead {
	
	int[][] data;
	public FileRead(String filename) throws  FileNotFoundException, IOException {
		int numVar=0;
//		int width = 91;
//		int height = 3;
		int rows=0;
		int cols=0;
		//int numClau = rows;
		File file = new File(filename);
		Scanner inputFile = new Scanner(file);
		

		
		
	     

		

		while (inputFile.hasNext())
		{
			String num=inputFile.nextLine();
			if(num.startsWith("p"))
			{
				Scanner s = new Scanner(num).useDelimiter("[^0-9]+");
				numVar=s.nextInt();
				rows=s.nextInt();				
			     s.close();
			     //System.out.println(rows);
			     data = new int[rows][cols];

			     
			}
			if(num.contains("clause length"))
			{
				Scanner s = new Scanner(num).useDelimiter("[^0-9]+");
				cols=s.nextInt();				
			     s.close();
			     //System.out.println(cols);


			}

			if(!num.startsWith("c"))
			{
				int test=inputFile.nextInt();
				
					//System.out.println(test);
					for(int x=0; x<rows; x++)
					{
						for(int y=0; y<cols; y++)
						{
							if((test!=0))
							{
								//System.out.println(test);
								data[x][y]=test;
								//System.out.print((data[x][y] + " "));

								test=inputFile.nextInt();
							}
							else if(test==0)
							{
								test=inputFile.nextInt();
								//System.out.println(test);

								data[x][y]=test;
								//System.out.print(data[x][y] + " ");

								test=inputFile.nextInt();


							}
						}
						//System.out.println();
					}	
					break;		
				
			}			
			
		}
		     
		inputFile.close();
		
		solver sol = new solver();
		sol.solve(data);
		
		
	}
	
	public int[][] getClauses() {
			return data;
	    }
}

推荐答案

这里有详细解释：http://en.wikipedia.org/wiki/Tabu_search [ ^ ]。



伪代码可用，只需看一下。

-SA

This is explained in detail here: http://en.wikipedia.org/wiki/Tabu_search[^].

Pseudo-code is available, just look at it.

—SA

这篇关于帮助Tabu搜索布尔可满足性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！