From 8e346754080c24db699a4e8ff9989d75378c2a9d Mon Sep 17 00:00:00 2001 From: gothictomato Date: Thu, 21 Jul 2022 10:56:05 -0400 Subject: [PATCH] Initial progress on subsumption DFA. Why is this branch called subsumption-tree? --- CMakeLists.txt | 4 +- main.c | 11 ++ ncnf.c | 304 +++++++++++++++++++++++++++++++++++++++++++++++++ ncnf.h | 22 ++++ subtree.c | 20 ++++ subtree.h | 89 +++++++++++++++ 6 files changed, 448 insertions(+), 2 deletions(-) create mode 100644 ncnf.c create mode 100644 ncnf.h create mode 100644 subtree.c create mode 100644 subtree.h diff --git a/CMakeLists.txt b/CMakeLists.txt index de2aef4..2e25f8a 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -2,8 +2,8 @@ cmake_minimum_required(VERSION 3.22) project(psat C) set(CMAKE_C_STANDARD 99) -# set(CMAKE_C_FLAGS "-O3") +set(CMAKE_C_FLAGS "-g") -add_executable(psat main.c cnf.c cnf.h time.c time.h types.h gpusolver.c gpusolver.h cpusolver.c cpusolver.h tests/masterTest.c tests/masterTest.h) +add_executable(psat main.c cnf.c cnf.h time.c time.h types.h gpusolver.c gpusolver.h cpusolver.c cpusolver.h tests/masterTest.c tests/masterTest.h subtree.c subtree.h ncnf.c ncnf.h) target_link_libraries(psat -lOpenCL) \ No newline at end of file diff --git a/main.c b/main.c index 9b3e030..354797a 100644 --- a/main.c +++ b/main.c @@ -3,8 +3,19 @@ #include "gpusolver.h" #include "time.h" #include "tests/masterTest.h" +#include "ncnf.h" int main() { + ncnf* c2 = nreadDIMACS("/home/lev/Downloads/uf20/uf20-02.cnf"); + nprintcnf(c2); + + printf("\n\n\n\n"); + nprintcnf2(c2); + nsortlastnum(c2); + printf("\n\n\n\n"); + nprintcnf2(c2); + printf("the balcony is to your left\n"); + return 0; /* srand( utime()); u32 cnt = 4096; diff --git a/ncnf.c b/ncnf.c new file mode 100644 index 0000000..c99f21f --- /dev/null +++ b/ncnf.c @@ -0,0 +1,304 @@ +#include "ncnf.h" +#include +#include +#include + +#define CHECK(X, Y) if (X == NULL) { \ + printf(Y); \ + return NULL; \ +} + + +ncnf* nreadDIMACS(char* path) { + ncnf* c = malloc(sizeof(ncnf)); + CHECK(c, "Failed to alloc CNF struct\n") + + FILE* f = fopen(path, "r"); + CHECK(f, "Failed to open file\n") + + u32 bufsize = 1000; + char* buf = malloc(sizeof(char) * bufsize); + CHECK(buf, "Failed to alloc read buffer\n") + + CHECK(fgets(buf, sizeof(char) * bufsize, f), "Failed to read file\n") + + while (buf[0] == 'c') { + CHECK(fgets(buf, sizeof(char) * bufsize, f), "Failed to read file\n"); + } + + char* temp = buf; + while (*temp == ' ' || *temp == 'p' || *temp == 'c' || *temp == 'n' || *temp == 'f') temp++; + + c->varcnt = 0; + while (((u8) (*temp - '0')) < 10) { + c->varcnt *= 10; + c->varcnt += (*temp - '0'); + temp++; + } + + // Skip any trailing whitespace + while (*temp == ' ') temp++; + + // Read in clausecnt + c->clausecnt = 0; + while (((u8) (*temp - '0')) < 10) { + c->clausecnt *= 10; + c->clausecnt += (*temp - '0'); + temp++; + } + + u32 nsize = sizeof(char) * (c->varcnt * 12LU) + 10; + char* nbuf = realloc(buf, nsize); + CHECK(nbuf, "Failed to realloc read buffer\n"); + + buf = nbuf; + + u32 cap = 32; + c->totcnt = 0; + + c->cptrs = malloc(sizeof(u32) * c->clausecnt); + CHECK(c->cptrs, "Failed to allocate clause offsets\n") + c->clens = malloc(sizeof(u32) * c->clausecnt); + CHECK(c->clens, "Failed to allocate clause lens\n") + c->lvars = malloc(sizeof(u32) * c->clausecnt); + CHECK(c->lvars, "Failed to alloc clause lvars\n") + + c->varbak = calloc(cap, sizeof(u32)); + CHECK(c->varbak, "Failed to allocate variable backing array\n") + c->parbak = malloc(sizeof(u8) * cap); + CHECK(c->parbak, "Failed to allocate parity backing array\n"); + + for (u32 i = 0; i < c->clausecnt; ++i) { + CHECK(fgets(buf, nsize, f), "Failed to read clause\n") + c->clens[i] = 0; + c->cptrs[i] = c->totcnt; + + temp = buf; + while (*temp == ' ') temp++; + + bool empty = true; + bool pos = true; + while (*temp != '\n' && *temp != '\0') { + if (c->totcnt == cap) { + u32 ncap = cap << 1U; + c->varbak = realloc(c->varbak, sizeof(u32) * ncap); + CHECK(c->varbak, "Failed to realloc variable backing array\n") + memset(c->varbak + cap, 0, sizeof(u32) * cap); + c->parbak = realloc(c->parbak, sizeof(u8) * ncap); + CHECK(c->parbak, "Failed to realloc parity backing array\n") + cap = ncap; + } + + if (*temp == '-') { + pos = false; + } else if (((u8) (*temp - '0')) < 10) { + if (*temp == '0' && c->clens[i] == 0 && c->varbak[c->totcnt] == 0) { + break; + } + c->varbak[c->totcnt] *= 10; + c->varbak[c->totcnt] += (*temp - '0'); + + } else { + while (temp[1] == ' ') temp++; + c->parbak[c->totcnt] = pos; + c->clens[i]++; + c->varbak[c->totcnt] -= 1; + if (c->lvars[i] < c->varbak[c->totcnt]) c->lvars[i] = c->varbak[c->totcnt]; + empty = false; + pos = true; + (c->totcnt)++; + if (temp[1] == '0') { + break; + } + } + temp++; + } + + if (empty) { + printf("UNSAT: Empty clause %u\n", i); + return NULL; + } + } + + for (u32 i = 0; i < c->clausecnt; ++i) { + c->lvars[i] += 1; + c->lvars[i] = c->varcnt - c->lvars[i]; + } + + c->varbak = realloc(c->varbak, sizeof(u32) * c->totcnt); + CHECK(c->varbak, "Failed to do final resize on variable backing array\n") + c->parbak = realloc(c->parbak, sizeof(u8) * c->totcnt); + CHECK(c->parbak, "Failed to do final resize on parity backing array\n") + free(buf); + if (fclose(f)) { + printf("Failed to close file\n"); + return NULL; + } + return c; +} + +void nprintcnf(ncnf* c) { + printf("p cnf %u %u\n", c->varcnt, c->clausecnt); + for (u32 i = 0; i < c->clausecnt; ++i) { + for (u32 j = 0; j < c->clens[i]; ++j) { + printf("%s%u ", (c->parbak[c->cptrs[i] + j]) ? ("") : ("-"), c->varbak[c->cptrs[i] + j] + 1); + } + printf("0\n"); + } + printf("\n"); +} + +void nprintcnf2(ncnf* c) { + printf("p cnf %u %u\n", c->varcnt, c->clausecnt); + for (u32 i = 0; i < c->clausecnt; ++i) { + printf("lvr: %u - ", c->lvars[i]); + for (u32 j = 0; j < c->clens[i]; ++j) { + printf("%s%u ", (c->parbak[c->cptrs[i] + j]) ? ("") : ("-"), c->varbak[c->cptrs[i] + j] + 1); + } + printf("0\n"); + } + printf("\n"); +} + +void nfreecnf(ncnf* c) { + free(c->varbak); + free(c->parbak); + free(c->cptrs); + free(c->clens); + free(c->lvars); + free(c); +} + +const u32 RBITS2 = 8; +const u32 RSIZE2 = 1U << RBITS2; +const u32 RLVLS2 = (31U / RBITS2) + 1; +const u32 RMASK2 = RSIZE2 - 1; + +void nsortlastnum(ncnf* c) { + // Radix sort on the clauses based on their lvars + bool v = false; + u32* d = malloc(sizeof(u32) * c->clausecnt); + u32* d2 = malloc(sizeof(u32) * c->clausecnt); + u32* d22 = malloc(sizeof(u32) * c->clausecnt); + + + + u32 qb[RLVLS2 * RSIZE2]; + u32 qe[RLVLS2 * RSIZE2]; + memset(qb, 0, sizeof(u32) * RLVLS2 * RSIZE2); + memset(qe, 0, sizeof(u32) * RLVLS2 * RSIZE2); + + for (u32 pass = 0; pass < RLVLS2; ++pass) { + u32 shift = pass * RBITS2; + + for (u32 i = 0; i < c->clausecnt; ++i) { + u32 val = UINT32_MAX - c->lvars[i]; + u32 ind = (val >> shift) & RMASK2; + qe[pass * RSIZE2 + ind]++; + } + + u32 uc = 0; + for (u32 i = 0; i < RSIZE2; ++i) uc += (qe[pass * RSIZE2 + i] != 0); + if (uc == 1) continue; + + qb[pass * RSIZE2] = 0; + for (u32 i = 1; i < RSIZE2; ++i) { + qb[pass * RSIZE2 + i] = qb[pass * RSIZE2 + i - 1] + qe[pass * RSIZE2 + i - 1]; + } + + for (u32 i = 0; i < c->clausecnt; ++i) { + u32 val = UINT32_MAX - c->lvars[i]; + u32 ind = (val >> shift) & RMASK2; + d[qb[pass * RSIZE2 + ind]] = c->cptrs[i]; + d2[qb[pass * RSIZE2 + ind]] = c->clens[i]; + d22[qb[pass * RSIZE2 + ind]] = c->lvars[i]; + qb[pass * RSIZE2 + ind]++; + __builtin_prefetch(d2 + qb[pass * RSIZE2 + ind] + 1); + __builtin_prefetch(d + qb[pass * RSIZE2 + ind] + 1); + } + + u32* tptr = c->cptrs; + c->cptrs = d; + d = tptr; + tptr = c->clens; + c->clens = d2; + d2 = tptr; + tptr = c->lvars; + c->lvars = d22; + d22 = tptr; + v = !v; + } + + if (v) { + u32* tptr = c->cptrs; + c->cptrs = d; + d = tptr; + tptr = c->clens; + c->clens = d2; + d2 = tptr; + tptr = c->lvars; + c->lvars = d22; + d22 = tptr; + v = !v; + memcpy(c->cptrs, d, c->clausecnt * sizeof(u32)); + memcpy(c->clens, d2, c->clausecnt * sizeof(u32)); + memcpy(c->lvars, d22, c->clausecnt * sizeof(u32)); + } + free(d2); + free(d22); + + u8* d3 = malloc(sizeof(u8) * c->clausecnt); + // Radix sort the literals of each clause (for reasons, TM) + u32 dlen = c->clausecnt; + + for (u32 k = 0; k < c->clausecnt; ++k) { + if (c->clens[k] > dlen) { + d = realloc(d, sizeof(u32) * c->clens[k]); + d3 = realloc(d3, sizeof(u8) * c->clens[k]); + if (d == NULL || d3 == NULL) { + printf("I'm giving up\n"); + } + dlen = c->clens[k]; + } + + memset(qb, 0, sizeof(u32) * RLVLS2 * RSIZE2); + memset(qe, 0, sizeof(u32) * RLVLS2 * RSIZE2); + + for (u32 pass = 0; pass < RLVLS2; ++pass) { + u32 shift = pass * RBITS2; + + for (u32 i = 0; i < c->clens[k]; ++i) { + u32 val = c->varbak[c->cptrs[k] + i]; + u32 ind = (val >> shift) & RMASK2; + qe[pass * RSIZE2 + ind]++; + } + + u32 uc = 0; + for (u32 i = 0; i < RSIZE2; ++i) uc += (qe[pass * RSIZE2 + i] != 0); + if (uc == 1) continue; + + qb[pass * RSIZE2] = 0; + for (u32 i = 1; i < RSIZE2; ++i) { + qb[pass * RSIZE2 + i] = qb[pass * RSIZE2 + i - 1] + qe[pass * RSIZE2 + i - 1]; + } + + for (u32 i = 0; i < c->clens[k]; ++i) { + u32 val = c->varbak[c->cptrs[k] + i]; + u32 ind = (val >> shift) & RMASK2; + d[qb[pass * RSIZE2 + ind]] = c->varbak[c->cptrs[k] + i]; + d3[qb[pass * RSIZE2 + ind]] = c->parbak[c->cptrs[k] + i]; + qb[pass * RSIZE2 + ind]++; + __builtin_prefetch(d + qb[pass * RSIZE2 + ind] + 1); + __builtin_prefetch(d3 + qb[pass * RSIZE2 + ind] + 1); + } + + memcpy(c->varbak + c->cptrs[k], d, sizeof(u32) * c->clens[k]); + memcpy(c->parbak + c->cptrs[k], d3, sizeof(u8) * c->clens[k]); + } + } + + free(d); + free(d3); + + +} \ No newline at end of file diff --git a/ncnf.h b/ncnf.h new file mode 100644 index 0000000..03b26fc --- /dev/null +++ b/ncnf.h @@ -0,0 +1,22 @@ +#pragma once +#include "types.h" + +typedef struct { + u32 varcnt; + u32 clausecnt; + u32* lvars; + u32* clens; + u32* cptrs; + u32 totcnt; + u32* varbak; + u8* parbak; +} ncnf; + +ncnf* nreadDIMACS(char* path); + +void nprintcnf(ncnf* c); +void nprintcnf2(ncnf* c); + +void nsortlastnum(ncnf* c); + +void nfreecnf(ncnf* c); \ No newline at end of file diff --git a/subtree.c b/subtree.c new file mode 100644 index 0000000..0c509b9 --- /dev/null +++ b/subtree.c @@ -0,0 +1,20 @@ +#include "subtree.h" + + + +void gendfa() { + u32 varcnt = 4; + char* clauses[4] = { + "0121", + "0122", + "2122", + "2222" + }; + + // Order the clauses + // Make nodes for each clause + // Combine 2 nodes into 1 if their next prefix is identical + // If their next prefix is 1, create 2 combinations + + +} \ No newline at end of file diff --git a/subtree.h b/subtree.h new file mode 100644 index 0000000..b6e817f --- /dev/null +++ b/subtree.h @@ -0,0 +1,89 @@ +#pragma once +#include "types.h" +#include + + + +/* +void sortstrings(char** list, u32 len, u32 cnt) { + bool v = false; + u32* d = malloc(sizeof(u32) * c->litcnt); + u32* d2 = malloc(sizeof(u32) * c->litcnt); + u8* d3 = malloc(sizeof(u8) * c->litcnt); + + u64 qb[RLVLS * RSIZE]; + u64 qe[RLVLS * RSIZE]; + memset(qb, 0, sizeof(u64) * RLVLS * RSIZE); + memset(qe, 0, sizeof(u64) * RLVLS * RSIZE); + + for (u64 pass = 0; pass < RLVLS; ++pass) { + u64 shift = pass * RBITS; + + for (u64 i = 0; i < N; ++i) { + // U32MAX - because we want to sort highest to lowest, not lowest to highest + u32 val = UINT32_MAX - c->lastvars[c->clauses[i]]; + u64 ind = (val >> shift) & RMASK; + qe[pass * RSIZE + ind]++; + } + + u64 uc = 0; + for (u64 i = 0; i < RSIZE; ++i) if (qe[pass * RSIZE + i]) uc++; + if (uc == 1) continue; + + qb[pass * RSIZE] = 0; + for (u64 i = 1; i < RSIZE; ++i) { + qb[pass * RSIZE + i] = qb[pass * RSIZE + i - 1] + qe[pass * RSIZE + i - 1]; + } + + for (u64 i = 0; i < N; ++i) { + u32 val = UINT32_MAX - c->lastvars[c->clauses[i]]; + u64 ind = (val >> shift) & RMASK; + d[qb[pass * RSIZE + ind]] = c->variables[i]; + d2[qb[pass * RSIZE + ind]] = c->clauses[i]; + d3[qb[pass * RSIZE + ind]] = c->pars[i]; + qb[pass * RSIZE + ind]++; + __builtin_prefetch(d + qb[pass * RSIZE + ind] + 1); + __builtin_prefetch(d2 + qb[pass * RSIZE + ind] + 1); + __builtin_prefetch(d3 + qb[pass * RSIZE + ind] + 1); + } + + // Every iteration we swap pointers to avoid doing a memcpy + u32* tptr = c->variables; + c->variables = d; + d = tptr; + tptr = c->clauses; + c->clauses = d2; + d2 = tptr; + u8* tptr2 = c->pars; + c->pars = d3; + d3 = tptr2; + v = !v; + } + + // If the pointers are still swapped at the end, we swap them to their original locations and + // copy over the result + if (v) { + u32* tptr = c->variables; + c->variables = d; + d = tptr; + tptr = c->clauses; + c->clauses = d2; + d2 = tptr; + u8* tptr2 = c->pars; + c->pars = d3; + d3 = tptr2; + memcpy(c->variables, d, N * sizeof(u32)); + memcpy(c->clauses, d2, N * sizeof(u32)); + memcpy(c->pars, d3, N * sizeof(u8)); + } + free(d); + free(d2); + free(d3); + + // Initialize an array with all the clause indices in their current order + u32* swaparr = malloc(sizeof(u32) * c->clausecnt); + for (u32 i = 0; i < c->clausecnt; ++i) { + swaparr[i] = i; + } +} + */ \ No newline at end of file