lev/psat
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Progress on early subsumption

Browse Source 
Signed-off-by: gothictomato <gothictomato@pm.me>
This commit is contained in:
gothictomato
2022-08-18 22:04:52 -04:00
parent 1d938273f3
commit a1b6cdaea9
10 changed files with 679 additions and 13 deletions
Download Patch File Download Diff File Expand all files Collapse all files

293
main.c
View File

@@ -1,10 +1,256 @@
#include <stdio.h>
#include "cnf.h"
#include "gpusolver.h"
// #include "gpusolver.h"
#include "time.h"
#include "tests/masterTest.h"
// #include "tests/masterTest.h"
#include "gmp.h"
#include "rng.h"
#include "ncnf.h"
#define ADD (0)
#define CMP (1)
#define CHK (2)
void ctrthings2(cnf* c, u32* state, u32* ctr, u32* max) {
u32 wcnt = 1U + (c->cnts[0] / 32U);
u32* mode = state;
u32* index = state + 1;
u32* addval = state + 2;
u32 varcnt = c->cnts[0] - 1;
u32 chkmsk = 0xFFFFFFFFU * (*mode == CHK);
u32 chkcls = *index & chkmsk;
u32 chkind = c->clausedat[3 * chkcls] + (*addval & chkmsk);
u32 var = c->variables[chkind];
u8 par = c->parities[chkind];
u32 vword = (varcnt - var) >> 5U;
u32 vbit = (varcnt - var) & 0b11111U;
u8 corpar = (ctr[vword] >> vbit) & 1U;
u8 isvalid = (par == corpar);
u8 islvar = ((*addval + 1) == c->clausedat[3 * chkcls + 1]);
if (*mode == CHK) {
// printf("> %u %u\n", *index, *addval);
// printf("%u %u %u\n", var, par, corpar);
// printf("%u %u\n", chkcls, chkind);
// printf("%u %u %u\n", islvar, isvalid, c->clausedat[3 * chkcls + 1]);
/*
* if last var
* if valid, add
* if invalid, iterate clause
* else
* if valid, iterate addval up to len
* if invalid, iterate claus
* If current var is valid:
* if last var:
*
*/
if (isvalid) {
if (islvar) {
u32 j = c->clausedat[3 * chkcls + 2];
*mode -= 2;
printf("j: %u\n", j);
*index = j >> 5U;
*addval = 1U << (j & 0b11111U);
} else {
*addval += 1U;
}
} else {
*addval = 0;
*index += 1U;
if (*index == c->cnts[1]) {
printf("SAT\n");
*mode = 4;
return;
}
}
} /* else {
//printf("YEET\n");
if (*index >= wcnt) printf("FUCK\n");
u32 nval = ctr[*index] + *addval; // Find the result of the current step if it was addition
*addval = (nval < ctr[*index]) * (*mode == ADD); // If in add mode, set addval to carry, else set 0
ctr[*index] = nval * (*mode == ADD) + ctr[*index] * (*mode != ADD); // If in add mode, set new ctr val, otherwise leave unchanged
*addval -= (ctr[*index] < max[*index]) * (*mode == CMP); // If in comparison mode, decrement addval if less than
*addval += (ctr[*index] > max[*index]) * (*mode == CMP); // If in comparison mode, increment addval if greater than
bool addcond = (*addval == 0) | (*index == (wcnt - 1)); // Exit condition for the ADD state: If addval is zero (no carry) or we're at the last word
bool cmpcond = (*addval != 0) | (*index == 0); // Exit condition for the CMP state: if addval is nonzero (lt or gt) or we're at the least significant word
if (*mode == CMP && cmpcond && *addval != -1) { // If in cmpmode and the comparison result is not less than, unsat
printf("UNSAT\n");
*mode = 4;
return;
}
bool cmpdone = cmpcond * (*mode == CMP); // if comparison completion conditions are satisfied and in CMP mode
u32 addindex = (*index + 1) * !addcond + (wcnt - 1) * addcond; // if add completion is satisfied, set index to most significant word, else increment by 1
*index = addindex * (*mode == ADD) + (*index - 1) * (*mode == CMP); // If in add mode, use addindex; if in cmp mode, decrement index by 1
*index *= !cmpdone;
// Leave adval alone if:
// not in add mode
// add mode isn't done
// not in cmp mode
// cmp mode isn't done
//
*addval *= !(((addcond) & (*mode != ADD)) & cmpdone); // If add is complete, zero addval, else leave unchanged
*mode += addcond * (*mode == ADD) + cmpdone; // If in add mode and add completion is reached, increment mode. If in cmp mode and cmp completion reached, increment mode.
}
*/
u32 cmpaddind = *index * (*mode != CHK);
if (cmpaddind >= wcnt) printf("FUCK\n");
u32 nval = ctr[cmpaddind] + *addval; // Find the result of the current step if it was addition
*addval = (nval < ctr[cmpaddind]) * (*mode == ADD) + (*addval) * (*mode == CHK); // If in add mode, set addval to carry. If in cmp mode, set to 0. If in check mode, leave alone.
ctr[cmpaddind] = nval * (*mode == ADD) + ctr[cmpaddind] * (*mode != ADD); // If in add mode, set new ctr val, otherwise leave unchanged
*addval -= (ctr[cmpaddind] < max[cmpaddind]) * (*mode == CMP); // If in comparison mode, decrement addval if less than
*addval += (ctr[cmpaddind] > max[cmpaddind]) * (*mode == CMP); // If in comparison mode, increment addval if greater than
bool addcond = (*addval == 0) | (cmpaddind == (wcnt - 1)); // Exit condition for the ADD state: If addval is zero (no carry) or we're at the last word
bool cmpcond = (*addval != 0) | (cmpaddind == 0); // Exit condition for the CMP state: if addval is nonzero (lt or gt) or we're at the least significant word
if (*mode == CMP && cmpcond && *addval != -1) { // If in cmpmode and the comparison result is not less than, unsat
printf("UNSAT\n");
*mode = 4;
return;
}
bool cmpdone = cmpcond & (*mode == CMP); // if comparison completion conditions are satisfied and in CMP mode
u32 addindex = (cmpaddind + 1) * !addcond + (wcnt - 1) * addcond; // if add completion is satisfied, set index to most significant word, else increment by 1
*index = addindex * (*mode == ADD) + (*index - (*mode == CMP)) * (*mode != ADD); // If in add mode, use addindex; if in cmp mode, decrement index by 1
*index *= !cmpdone;
// Leave adval alone if:
// not in add mode
// add mode isn't done
// not in cmp mode
// cmp mode isn't done
//
*addval *= !(((addcond) & (*mode == ADD)) | cmpdone); // If add is complete, or cmp is complete, zero. Else leave unchanged.
*mode += addcond * (*mode == ADD) + cmpdone; // If in add mode and add completion is reached, increment mode. If in cmp mode and cmp completion reached, increment mode.
}
void printbits(unsigned a) {
for (unsigned i = 0; i < 32; ++i) {
unsigned ind = 31 - i;
printf("%u", (a >> ind) & 1U);
}
}
#define TESTS (274877906944LU >> 10U)
#define CSZE (83LU)
#define eqprob (0.01f)
int main() {
/*
printf("Tests: %lu\n", TESTS);
rngstate rng;
u64 rseed = utime();
seed(&rng, rseed);
printf("Seed: %lu\n", rseed);
mpz_t a, b, c, d, e;
mpz_inits(a, b, c, d, e, NULL);
u32 ctrp[CSZE];
u32 maxp[CSZE];
u32* ctr = ctrp;
u32* max = maxp;
u32 state[3];
u32 hdr[2];
char buf[4096];
for (u64 i = 0; i < TESTS; ++i) {
memset(ctr, 0, sizeof(u32) * CSZE);
memset(max, 0, sizeof(u32) * CSZE);
//u32 lenval = ru32(&rng) % CSZE;
u32 lenval = CSZE;
if (lenval < 2) lenval = 2;
u32 jval = ru32(&rng) % ((lenval - 1) * 32);
for (u32 j = 0; j < lenval - 2; ++j) {
ctr[j] = ru32(&rng);
max[j] = ru32(&rng);
}
mpz_import(a, lenval, -1, sizeof(u32), 0, 0, ctr);
mpz_import(b, lenval, -1, sizeof(u32), 0, 0, max);
state[1] = jval >> 5U;
state[2] = jval & 0b11111U;
state[2] = 1U << state[2];
mpz_ui_pow_ui(c, 2, jval);
if (rf32(&rng) < eqprob && mpz_cmp) {
mpz_sub(a, b, c);
if (mpz_sgn(a) != -1) {
mpz_export(ctr, NULL, -1, sizeof(u32), 0, 0, a);
} else {
mpz_import(a, lenval, -1, sizeof(u32), 0, 0, ctr);
}
}
mpz_add(d, a, c);
state[0] = 0;
while (state[0] < 2U) {
ctrthings2(hdr, lenval, state, ctr, max);
}
mpz_import(c, lenval, -1, sizeof(u32), 0, 0, ctr);
i32 res = mpz_cmp(d, b);
if (res == -1) {
if (state[2] != -1) {
printf("Fuck2 %lu\n", i);
printf("d: ");
mpz_out_str(stdout, 10, d);
printf("\nb: ");
mpz_out_str(stdout, 10, b);
printf("\n");
printf("mode: %u\n", state[2]);
exit(0);
}
} else {
if (state[2] != 2) {
printf("Fuck3 %lu\n", i);
printf("d: ");
mpz_out_str(stdout, 10, d);
printf("\nc: ");
mpz_out_str(stdout, 10, c);
printf("\nb: ");
mpz_out_str(stdout, 10, b);
printf("\n");
printf("mode: %u\n", state[2]);
exit(0);
}
}
res = mpz_cmp(d, c);
if (res != 0) {
printf("Fuck %lu\na: ", i);
mpz_out_str(stdout, 10, a);
printf("\nd: ");
mpz_out_str(stdout, 10, d);
printf("\nc: ");
mpz_out_str(stdout, 10, c);
printf("\n%u %u\n", lenval, jval);
exit(0);
}
}
mpz_clears(a, b, c, d, e, NULL);
*/
/*
srand( utime());
u32 cnt = 4096;
@@ -28,7 +274,43 @@ int main() {
*/
/* Expects a path to a DIMACS file */
cnf* c = readDIMACS("/home/lev/Downloads/uf50/uf50-088.cnf");
cnf* c = readDIMACS("/home/lev/Downloads/uf20/uf20-022.cnf");
sortlastnum(c);
// printcnf(c);
u32 wcnt = 1U + (c->cnts[0] / 32U);
u32* ctr = calloc(wcnt, sizeof(u32));
u32* max = calloc(wcnt, sizeof(u32));
max[c->cnts[0] >> 5U] = 1U << (c->cnts[0] & 0b11111U);
u32 state[3];
state[0] = 2;
state[1] = state[2] = 0;
u32 mtr = 0;
while (state[0] < 3U) {
u32 cmd = state[0];
ctrthings2(c, state, ctr, max);
if (state[0] != 2 && cmd == 2) {
//printf("\n");
//for (unsigned i = wcnt - 1; i < wcnt; --i) printbits(ctr[i]);
//printf("\n");
//mtr++;
//if (mtr == 10) exit(15);
// printf("%u %u %u\n", state[0], state[1], state[2]);
}
}
return 0;
/*
// printf("%u\n", c->litcnt);
// for (u32 i = 0; i < c->clausecnt; ++i) printf("%u ", c->lastvars[i]);
@@ -46,5 +328,6 @@ int main() {
// if (res == 1) break;
freecnf(c);
return 0;
return 0;*/
}