|
|
|
@ -126,79 +126,25 @@ KCNF KCNF::generate_random(long n, long c, long k) {
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
bool KCNF::write_dimacs(const std::string& filename) const {
|
|
|
|
bool KCNF::write_dimacs(const std::string& filename) const {
|
|
|
|
fs::create_directories(CNF_DIR);
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
fs::path path = CNF_DIR / filename;
|
|
|
|
|
|
|
|
path = path.lexically_normal();
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
std::ofstream out(path);
|
|
|
|
|
|
|
|
if (!out) {
|
|
|
|
|
|
|
|
std::cerr << "Error: Could not open file " << path << "\n";
|
|
|
|
|
|
|
|
return false;
|
|
|
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
out << "p cnf " << n << " " << clauses.size() << "\n";
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
for (const auto& cl : clauses) {
|
|
|
|
for (const auto& cl : clauses) {
|
|
|
|
for (int lit : cl) {
|
|
|
|
if ((long)cl.size() != k) {
|
|
|
|
out << lit << " ";
|
|
|
|
throw std::runtime_error("Not a k-CNF formula.");
|
|
|
|
}
|
|
|
|
}
|
|
|
|
out << "0\n";
|
|
|
|
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
return true;
|
|
|
|
return CNF::write_dimacs(filename);
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
|
|
KCNF KCNF::read_dimacs(const std::string& filename) {
|
|
|
|
KCNF KCNF::read_dimacs(const std::string& filename) {
|
|
|
|
KCNF f;
|
|
|
|
CNF base = CNF::read_dimacs(filename);
|
|
|
|
|
|
|
|
|
|
|
|
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") {
|
|
|
|
KCNF f;
|
|
|
|
throw std::runtime_error("Unsupported DIMACS format.");
|
|
|
|
f.n = base.n;
|
|
|
|
}
|
|
|
|
f.clauses = std::move(base.clauses);
|
|
|
|
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()) {
|
|
|
|
if (!f.clauses.empty()) {
|
|
|
|
f.k = f.clauses[0].size();
|
|
|
|
f.k = f.clauses[0].size();
|
|
|
|
|
|
|
|
|
|
|
|
// check whether actually k-cnf
|
|
|
|
|
|
|
|
for (const auto& cl : f.clauses) {
|
|
|
|
for (const auto& cl : f.clauses) {
|
|
|
|
if ((long)cl.size() != f.k) {
|
|
|
|
if ((long)cl.size() != f.k) {
|
|
|
|
throw std::runtime_error("Input is not a k-CNF formula.");
|
|
|
|
throw std::runtime_error("Input is not a k-CNF formula.");
|
|
|
|
|