From d7ad78b6da34c5f696c99aea4a6d3cc2487fd51d Mon Sep 17 00:00:00 2001 From: Isabell Pflug Date: Fri, 17 Apr 2026 16:03:15 +0200 Subject: [PATCH] :sparkles: Created KCNF class and wrote random KCNF generation project. --- lib/kcnf.cpp | 148 ++++++++++++++++++++++++++++++++ lib/kcnf.hpp | 17 ++++ src/random_kcnf/random_kcnf.cpp | 29 +++++++ 3 files changed, 194 insertions(+) create mode 100644 lib/kcnf.cpp create mode 100644 lib/kcnf.hpp create mode 100644 src/random_kcnf/random_kcnf.cpp diff --git a/lib/kcnf.cpp b/lib/kcnf.cpp new file mode 100644 index 0000000..259e059 --- /dev/null +++ b/lib/kcnf.cpp @@ -0,0 +1,148 @@ +#include "kcnf.hpp" + +#include +#include +#include +#include +#include +#include +#include + +#ifdef _OPENMP +#include +#endif + +namespace fs = std::filesystem; + +const fs::path CNF_DIR = "./CNF"; + +long binom(long n, long k) { + return (k > n) ? 0 : + (k == 0 || k == n) ? 1 : + (k == 1 || k == n - 1) ? n : + (k + k < n) ? + (binom(n - 1, k - 1) * n) / k : + (binom(n - 1, k) * n) / (n - k); +} + +// get the (n choose k) possible variable choices at index idx +// example: +std::vector unrank_combination(long n, long k, long long idx) { + std::vector comb; + comb.reserve(k); + long start = 1; + for (long i = 0; i < k; ++i) { + for (long v = start; v <= n; ++v) { + long long count = binom(n - v, k - i - 1); + if (idx < count) { + comb.push_back((int)v); + start = v + 1; + break; + } else { + idx -= count; + } + } + } + return comb; +} + +// sample c indices in [0,total] for our c = # of clauses +// this is the heart of the program as we are flattening the problem with our sampled indices and the unrank function! +std::vector sample_indices(long long total, long c) { + std::vector idx; + idx.reserve(c); + + std::random_device rd; + std::mt19937 gen(rd()); + std::uniform_int_distribution dist(0, total - 1); + + for (long i = 0; i < c; ++i) { + idx.push_back(dist(gen)); + } + + return idx; +} + +// decode one clause from global index (think of it like a hash function for better understanding!) +// idx = combo_id * 2^k + mask +Clause decode_clause(long n, long k, long long idx) { + long long combo_id = idx >> k; + int mask = idx & ((1 << k) - 1); + + std::vector comb = unrank_combination(n, k, combo_id); + + Clause cl; + cl.reserve(k); + + for (int i = 0; i < k; ++i) { + int lit = comb[i]; + cl.push_back((mask & (1 << i)) ? lit : -lit); + } + + return cl; +} + +// parallel iteration to build clauses from indices +std::vector build_clauses_parallel( + long n, + long k, + const std::vector& indices) { + + std::vector result(indices.size()); + + #pragma omp parallel for schedule(dynamic) + for (long i = 0; i < (long)indices.size(); ++i) { + result[i] = decode_clause(n, k, indices[i]); + } + + return result; +} + +KCNF KCNF::generate_random(long n, long c, long k) { + KCNF f; + f.n = n; + f.k = k; + + // test for logical limits + long long total = binom(n,k) * (1LL << k); + if (c > total) { + throw std::runtime_error("Too many clauses requested."); + } + + // test for hardware limits + 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"); + } + + auto indices = sample_indices(total, c); + f.clauses = build_clauses_parallel(n, k, indices); + + return f; +} + +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 (int lit : cl) { + out << lit << " "; + } + out << "0\n"; + } + + return true; +} diff --git a/lib/kcnf.hpp b/lib/kcnf.hpp new file mode 100644 index 0000000..c256125 --- /dev/null +++ b/lib/kcnf.hpp @@ -0,0 +1,17 @@ +#pragma once + +#include +#include + +using Clause = std::vector; // makes it nicer to read + +class KCNF { +public: + long n = 0; + long k = 0; + std::vector clauses; + + static KCNF generate_random(long n, long c, long k); + + bool write_dimacs(const std::string& filename) const; +}; diff --git a/src/random_kcnf/random_kcnf.cpp b/src/random_kcnf/random_kcnf.cpp new file mode 100644 index 0000000..a063b86 --- /dev/null +++ b/src/random_kcnf/random_kcnf.cpp @@ -0,0 +1,29 @@ +#include "kcnf.hpp" + +#include +#include + +int main(int argc, char* argv[]) { + if (argc != 5) { + std::cerr << "Usage: " << argv[0] << " n c k output.cnf\n"; + return 1; + } + + long n = strtol(argv[1], NULL, 10); + long c = strtol(argv[2], NULL, 10); + long k = strtol(argv[3], NULL, 10); + + try { + KCNF f = KCNF::generate_random(n, c, k); + + if (!f.write_dimacs(argv[4])) { + return 1; + } + + } catch (const std::exception& e) { + std::cerr << e.what() << "\n"; + return 1; + } + + return 0; +}