|
|
|
|
@ -115,8 +115,8 @@ KCNF KCNF::generate_random(long n, long c, long k) {
|
|
|
|
|
long long estimated_bytes =
|
|
|
|
|
c * (sizeof(Clause) + k * sizeof(int));
|
|
|
|
|
|
|
|
|
|
if (estimated_bytes > 500 * 1024 * 1024) { // 500MB
|
|
|
|
|
throw std::runtime_error("Estimated memory too large");
|
|
|
|
|
if (estimated_bytes > 500 * 1024 * 1024) { // 500MB, you may change this line for yourself if you are happy using more memory.
|
|
|
|
|
throw std::runtime_error("Estimated memory too large.");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
auto indices = sample_indices(total, c);
|
|
|
|
|
@ -148,3 +148,65 @@ bool KCNF::write_dimacs(const std::string& filename) const {
|
|
|
|
|
|
|
|
|
|
return true;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
KCNF KCNF::read_dimacs(const std::string& filename) {
|
|
|
|
|
KCNF f;
|
|
|
|
|
|
|
|
|
|
std::ifstream in(filename);
|
|
|
|
|
if (!in) {
|
|
|
|
|
throw std::runtime_error("Could not open DIMACS file.");
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
std::string line;
|
|
|
|
|
long expected_clauses = 0;
|
|
|
|
|
|
|
|
|
|
while (std::getline(in, line)) {
|
|
|
|
|
if (line.empty()) continue;
|
|
|
|
|
|
|
|
|
|
if (line[0] == 'c') continue;
|
|
|
|
|
|
|
|
|
|
if (line[0] == 'p') {
|
|
|
|
|
std::istringstream iss(line);
|
|
|
|
|
std::string tmp, format;
|
|
|
|
|
iss >> tmp >> format >> f.n >> expected_clauses;
|
|
|
|
|
|
|
|
|
|
if (format != "cnf") {
|
|
|
|
|
throw std::runtime_error("Unsupported DIMACS format.");
|
|
|
|
|
}
|
|
|
|
|
continue;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
std::istringstream iss(line);
|
|
|
|
|
Clause cl;
|
|
|
|
|
int lit;
|
|
|
|
|
|
|
|
|
|
while (iss >> lit) {
|
|
|
|
|
if (lit == 0) break;
|
|
|
|
|
cl.push_back(lit);
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (!cl.empty()) {
|
|
|
|
|
f.clauses.push_back(cl);
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (expected_clauses != 0 &&
|
|
|
|
|
f.clauses.size() != (size_t)expected_clauses) {
|
|
|
|
|
std::cerr << "Warning: Clause count mismatch.\n";
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if (!f.clauses.empty()) {
|
|
|
|
|
f.k = f.clauses[0].size();
|
|
|
|
|
|
|
|
|
|
// check whether actually k-cnf
|
|
|
|
|
for (const auto& cl : f.clauses) {
|
|
|
|
|
if ((long)cl.size() != f.k) {
|
|
|
|
|
throw std::runtime_error("Input is not a k-CNF formula.");
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
} else {
|
|
|
|
|
f.k = 0;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
return f;
|
|
|
|
|
}
|
|
|
|
|
|