♻️ Added general CNF class that KCNF now inherits.
parent
849ed2761f
commit
2e31b44efa
@ -0,0 +1,84 @@
|
||||
#include "cnf.hpp"
|
||||
|
||||
#include <filesystem>
|
||||
#include <fstream>
|
||||
#include <iostream>
|
||||
#include <sstream>
|
||||
#include <stdexcept>
|
||||
|
||||
namespace fs = std::filesystem;
|
||||
|
||||
const fs::path CNF_DIR = "./CNF";
|
||||
|
||||
bool CNF::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 (int lit : cl) {
|
||||
out << lit << " ";
|
||||
}
|
||||
out << "0\n";
|
||||
}
|
||||
|
||||
return true;
|
||||
}
|
||||
|
||||
CNF CNF::read_dimacs(const std::string& filename) {
|
||||
CNF 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";
|
||||
}
|
||||
|
||||
return f;
|
||||
}
|
||||
@ -0,0 +1,17 @@
|
||||
#pragma once
|
||||
|
||||
#include <string>
|
||||
#include <vector>
|
||||
|
||||
using Clause = std::vector<int>;
|
||||
|
||||
class CNF {
|
||||
public:
|
||||
long n = 0;
|
||||
std::vector<Clause> clauses;
|
||||
|
||||
virtual ~CNF() = default;
|
||||
|
||||
virtual bool write_dimacs(const std::string& filename) const;
|
||||
static CNF read_dimacs(const std::string& filename);
|
||||
};
|
||||
@ -1,18 +1,13 @@
|
||||
#pragma once
|
||||
|
||||
#include <string>
|
||||
#include <vector>
|
||||
#include "cnf.hpp"
|
||||
|
||||
using Clause = std::vector<int>; // makes it nicer to read
|
||||
|
||||
class KCNF {
|
||||
class KCNF : public CNF {
|
||||
public:
|
||||
long n = 0;
|
||||
long k = 0;
|
||||
std::vector<Clause> clauses;
|
||||
|
||||
static KCNF generate_random(long n, long c, long k);
|
||||
|
||||
bool write_dimacs(const std::string& filename) const;
|
||||
bool write_dimacs(const std::string& filename) const override;
|
||||
static KCNF read_dimacs(const std::string& filename);
|
||||
};
|
||||
|
||||
Loading…
Reference in New Issue