c++ - SAT 的哈密顿路径疑难解答
问题描述
我不确定是否应该在这里问这个问题，但这是我最后的手段，也是第一次在 Stackoverflow 上。我几乎没有编码经验，我目前正在 Coursera 做算法专业。该练习是，给定一张图，将哈密顿路径问题简化为 SAT 问题，然后他们使用 minisat 求解器 ( http://minisat.se/ ) 对其进行评估。下面的代码（大约 95% 我，他们提供了一个启动文件）通过了他们的一些测试，但最终失败了（注意：此代码实际上运行 minisat，我提交打印到终端的那个）。他们没有为失败的测试用例或预期的答案提供输入，它只是说错误答案。
我已经用一些图表进行了测试，它可以工作。我还尝试针对在线找到的非 SAT 实现（https://cppsecrets.com/users/22319897989712197103975756505164103109971051084699111109/Hamiltonian-Path.php）对我的解决方案进行压力测试，但到目前为止他们始终同意。如果需要，我可以为此添加代码。
有没有我应该考虑的边缘测试用例？我错过了什么？我知道这不是一个一般性的编程问题，但我要疯了，除非我通过练习，否则我无法前进。
谢谢
#include <ios>
#include <iostream>
#include <fstream>
#include <vector>
#include <string>
/*
Converts a graph G with n vertices and m edges into a series of booleans to evaluate whether a Hamiltonian
path exists. It then uses minisat solver (http://minisat.se/) to evaluate the clauses and return either SAT
if there is a path or UNSAT if no path exists.
This is part of a coursera assigment with the description below. The only difference is that instead of printing
the clauses to the terminal, I'm actually running minisat.
Input Format. The first line contains two integers and — the number of rooms and the number of corridors
connecting the rooms respectively. Each of the next lines contains two integers and describing the corridor
going from room to room . The corridors are two-way, that is, you can go both from to and from to . No
two corridors have a common part, that is, every corridor only allows you to go from one room to one other room.
Of course, no corridor connects a room to itself. Note that a corridor from to can be listed several times, and
there can be listed both a corridor from to and a corridor from to .
Constraints. 1 ≤ ≤ 30;0 ≤ ≤ (−1);1 ≤ , ≤ .
Output Format. You need to output a boolean formula in the CNF form in a specific format. If it is possible to go
through all the rooms and visit each one exactly once to clean it, the formula must be satisfiable. Otherwise, the
formula must be unsatisfiable. The sum of the numbers of variables used in each clause of the formula must not exceed
120 000.
*/
using namespace std;
typedef vector<vector<int>> Matrix;
string FILE_IN = "apartment_cnf.txt";
string FILE_OUT = "apartment_out.txt";
struct ConvertHampathToSat {
int numVertices;
int numEdges;
int repeatedEdges;
Matrix adj_matrix;
ConvertHampathToSat(int n, int m) : numVertices(n), numEdges(m) {
repeatedEdges = 0;
adj_matrix.resize(n, vector<int>(n));
}
int numeric_Sum(const int n) {
/*
Helper function returns the sum of numbers from 0 to n-1.
*/
int sum = 0;
for (int i = 0; i < n; i++) {
sum += i;
}
return sum;
}
void add_NotEdges(ofstream &cnf, const int f, const vector<int> &t, int &count) {
/*
Adds the clauses for pair of vertices without an edge between them.
For each pair, it adds one clause for when the from vertex is at the start of path, one clause
for when it is at the end of path, and two clauses for each position in the middle of path.
*/
if (t.empty()) { return; }
/* Converting from vertex number to variable */
int from = (f - 1) * numVertices + 1;
vector<int> not_edges;
for (int to : t) {
not_edges.push_back((to - 1) * numVertices + 1);
}
for (int path_pos = 0; path_pos < numVertices; path_pos++) {
for (int to : not_edges) {
if (path_pos == 0) {
/* from vertex is at start of path */
cnf << -(from + path_pos) << ' ' << -(to + path_pos + 1) << ' ' << 0 << endl;
} else if (path_pos == numVertices - 1) {
/* from vertex is at end of path */
cnf << -(from + path_pos) << ' ' << -(to + path_pos - 1) << ' ' << 0 << endl;
} else {
/* from vertex is in middle of path */
cnf << -(from + path_pos) << ' ' << -(to + path_pos + 1) << ' ' << 0 << endl;
cnf << -(from + path_pos) << ' ' << -(to + path_pos - 1) << ' ' << 0 << endl;
count++;
}
count++;
}
}
}
void write_ToFile() {
/*
Calculates number of variables and clauses, then writes it out in the format: p cnf variables clauses
Writes all the clauses in the format required by minisat: 1 -2 -4 0 (1 OR -2 OR -4). All clauses use OR.
Example: for a graph with 3 edges, variables 1, 2, and 3 represent vertex 1 in path position 1, 2, and 3.
Variables 1, 4, and 7 represent position 1 occupied by vertex 1, 2, and 3.
*/
/* Count was added to keep track of the number of clauses when I needed to figure out an equation */
int count = 0;
int numberVariables = numVertices * numVertices;
/* Calculation of total number of clauses
First term = Each vertex is in path + each path position has a vertex
Second term = Each vertex appears only once in path + each path has only one vertex
Third term = All possible non edges. */
int maxEdges = numeric_Sum(numVertices);
int actual_Edges = numEdges - repeatedEdges;
int clauses = (2 * numVertices) // First term
+ (2 * numVertices * numeric_Sum(numVertices)) // Second term
+ 2 * (numVertices - 1) * (maxEdges - actual_Edges); // Third term
/* Creating the file */
ofstream cnf{FILE_IN};
/* Print out number of variables and number of clauses */
cnf << "p cnf " << numberVariables << ' ' << clauses << endl;
/* Special case that there's only one vertex */
if (numVertices == 1) {
cnf << 1 << ' ' << 0 << endl;
cnf << -1 << ' ' << 0 << endl;
return;
}
/* Each vertex must have a position in the path */
for (int vertex = 1; vertex <= numberVariables; vertex += numVertices) {
for (int path_pos = 0; path_pos < numVertices; path_pos++) {
cnf << vertex + path_pos << ' ';
}
cnf << 0 << endl;
count++;
}
/* Each vertex must appear just once in the path */
for (int vertex = 1; vertex <= numberVariables; vertex += numVertices) {
for (int vertex_path = vertex; vertex_path < numVertices + vertex; vertex_path++) {
for (int path_pos = 1; path_pos < vertex + numVertices - vertex_path; path_pos++) {
cnf << -(vertex_path) << ' ' << -(vertex_path + path_pos) << ' ' << 0 << endl;
count++;
}
}
}
/* Each position must have a vertex */
for (int path_pos = 0; path_pos < numVertices; path_pos++) {
for (int vertex = 1; vertex <= numberVariables; vertex += numVertices) {
cnf << vertex + path_pos << ' ';
}
cnf << 0 << endl;
count++;
}
/* Each position can have only one vertex */
for (int path_pos = 1; path_pos <= numVertices; path_pos++) {
for (int vertex_path = path_pos; vertex_path < numberVariables; vertex_path += numVertices) {
for (int vertex = numVertices; vertex <= numberVariables - vertex_path; vertex += numVertices) {
cnf << -(vertex_path) << ' ' << -(vertex_path + vertex) << ' ' << 0 << endl;
count++;
}
}
}
/* Contiguos vertices in the path must have an edge */
Matrix edges_PlusAdded = adj_matrix; // Could do without this new matrix
for (int from = 1; from <= numVertices; from++) {
vector<int> not_edges;
for (int to = 1; to <= numVertices; to++) {
if (from != to && !edges_PlusAdded[from - 1][to - 1]) {
not_edges.push_back(to);
// To avoid duplicating clauses
edges_PlusAdded[from - 1][to - 1] = 1;
edges_PlusAdded[to - 1][from - 1] = 1;
}
}
add_NotEdges(cnf, from, not_edges, count);
}
}
string read_File() {
/*
Reads the first line from minisat output file FILE_OUT
*/
/* Opening the file */
ifstream ist{FILE_OUT};
/* Only care about the first line, which contains SAT or UNSAT */
string result;
ist >> result;
return result;
}
string printEquisatisfiableSatFormula() {
/*
Writes the input to a .txt file, runs minisat then outputs the answer
*/
/* Creating and writing the input to the file */
write_ToFile();
/* Calling minisat (http://minisat.se/) on the terminal */
string s = "minisat " + FILE_IN + " " + FILE_OUT;
const char *command = s.c_str();
system(command);
/* Reading the answer from minisat output file */
return read_File();
}
};
int main() {
ios::sync_with_stdio(false);
/* n = number of vertices, m = number of edges*/
int n, m;
cin >> n >> m;
ConvertHampathToSat converter(n, m);
vector<int> vertices(n);
for (int i = 0; i < m; i++) {
int from, to;
cin >> from >> to;
/* Input can have repeated edges, which need to be substracted for the
calculation of number of clauses */
if (converter.adj_matrix[from - 1][to - 1]) {
converter.repeatedEdges++;
}
/* Adding edges to adjacency list */
converter.adj_matrix[from - 1][to - 1] = 1;
converter.adj_matrix[to - 1][from - 1] = 1;
}
string answer = converter.printEquisatisfiableSatFormula();
cout << answer << endl;
return 0;
}
解决方案
推荐阅读
- angular - 当最终结果为真时，Angular Router Guard 无法解析
- sql - sqlite FTS5 表上的删除触发器有问题
- c# - 与 Singleton 相关的唤醒功能问题
- java - 使用 @webservice 将 wsdl 文件/工件导入 SOAP 初学者/测试客户端的 netbeans
- c# - 如何避免 Caliburn 微事件聚合器 HandleAsync 方法名称的警告？
- ios - 如何更改 SwiftUI swipeAction 按钮的文本颜色？
- c++ - 如何获取已安装的内存信息？
- android - 在颤动中语音到文本的语音识别
- ms-access - 如何使文本框显示表格大小的差异
- blazor - Blazor 页面 - 递归菜单