Skip to content

Commit 65330f1

Browse files
author
Muhammad
committed
fixed a bug in xor reasoning
1 parent 87c7337 commit 65330f1

8 files changed

Lines changed: 159 additions & 175 deletions

File tree

‎gpu/pfbve.cuh‎

Lines changed: 55 additions & 93 deletions
Original file line numberDiff line numberDiff line change
@@ -31,10 +31,11 @@ namespace pFROST {
3131
_PFROST_D_ void toblivion(const uint32& dx, const uint32& nSaved, CNF& cnf, OL& toSave, OL& other, cuVecU* resolved)
3232
{
3333
uint32* saved = resolved->jump(nSaved);
34+
const uint32 fx = FLIP(dx);
3435
#pragma unroll
3536
for (S_REF* i = toSave; i != toSave.end(); i++) {
3637
SCLAUSE& c = cnf[*i];
37-
if (c.original()) saveResolved(saved, c);
38+
if (c.original()) saveResolved(saved, c, fx);
3839
c.markDeleted();
3940
}
4041
saveResolved(saved, dx);
@@ -46,10 +47,11 @@ namespace pFROST {
4647
_PFROST_D_ void saveResolved(const uint32& dx, const uint32& nSaved, CNF& cnf, OL& toSave, cuVecU* resolved)
4748
{
4849
uint32* saved = resolved->jump(nSaved);
50+
const uint32 fx = FLIP(dx);
4951
#pragma unroll
5052
for (S_REF* i = toSave; i != toSave.end(); i++) {
5153
SCLAUSE& c = cnf[*i];
52-
if (c.original()) saveResolved(saved, c);
54+
if (c.original()) saveResolved(saved, c, fx);
5355
}
5456
saveResolved(saved, dx);
5557
}
@@ -328,60 +330,41 @@ namespace pFROST {
328330
_PFROST_D_ bool find_xor_gate(const uint32& dx, const uint32& nOrgCls, const int& xor_max_arity, CNF& cnf, OT& ot, cuVecU* units, cuVecU* resolved, uint32* out_c)
329331
{
330332
assert(dx > 1);
331-
assert(checkMolten(cnf, ot[dx], ot[FLIP(dx)]));
333+
assert(dx > 1);
334+
const uint32 fx = FLIP(dx), v = ABS(dx);
335+
assert(checkMolten(cnf, ot[dx], ot[fx]));
332336
OL& itarget = ot[dx];
337+
OL& otarget = ot[fx];
333338
for (S_REF* i = itarget; i != itarget.end(); i++) {
334339
SCLAUSE& ci = cnf[*i];
335340
int size = ci.size();
336341
int arity = size - 1; // XOR arity
337342
if (ci.learnt() || size < 3 || arity > xor_max_arity || arity > SH_MAX_BVE_OUT) continue;
338-
// share to out_c except dx
339-
shareXORClause(dx, ci, out_c);
343+
assert(arity <= SH_MAX_BVE_OUT1);
344+
// share to out_c
345+
shareXORClause(ci, out_c);
340346
// find arity clauses
341-
int itargets = 0;
342-
for (int j = 0; j < arity; j++) {
343-
S_REF r = find_fanin(dx, j, cnf, itarget, out_c, arity);
344-
if (r == GNOREF) break;
345-
cnf[r].melt(), itargets++;
346-
}
347-
if (itargets < arity) {
348-
freeze_arities(cnf, itarget);
349-
continue;
350-
}
351-
// find all +/-
352-
uint32 f_dx = FLIP(dx);
353-
S_REF r1 = find_all(f_dx, cnf, ot, out_c, arity);
354-
if (r1 == GNOREF) break;
355-
flip_all(out_c, arity);
356-
S_REF r2 = find_all(f_dx, cnf, ot, out_c, arity);
357-
if (r2 == GNOREF) break;
358-
assert(cnf[r1].original());
359-
assert(cnf[r2].original());
360-
cnf[r1].melt(), cnf[r2].melt();
361-
// check resolvability
362-
uint32 v = ABS(dx);
363-
OL& otarget = ot[f_dx];
364-
uint32 nAddedCls = 0, nAddedLits = 0;
365-
countSubstituted(v, cnf, itarget, otarget, nAddedCls, nAddedLits);
366-
if (nAddedCls > nOrgCls) {
367-
cnf[r1].freeze(), cnf[r2].freeze();
368-
break;
369-
}
370-
// can be substituted
371-
#if VE_DBG
372-
printf("c | Gate %d = XOR(", ABS(dx));
373-
for (int k = 0; k < arity; k++) {
374-
printf(" %d", ABS(out_c[k]));
375-
if (k < arity - 1) printf(",");
347+
uint32 parity = 0;
348+
int itargets = (1 << arity);
349+
while (--itargets && makeArity(cnf, ot, parity, out_c, size));
350+
assert(parity < (1UL << size)); // overflow check
351+
assert(itargets >= 0);
352+
if (itargets)
353+
freeze_arities(cnf, itarget, otarget);
354+
else {
355+
ci.melt();
356+
// check resolvability
357+
uint32 nAddedCls = 0, nAddedLits = 0;
358+
countSubstituted(v, cnf, itarget, otarget, nAddedCls, nAddedLits);
359+
if (nAddedCls > nOrgCls) {
360+
freeze_arities(cnf, itarget, otarget);
361+
break;
362+
}
363+
// can be substituted
364+
if (nAddedCls) substitute_x(v, nAddedCls, nAddedLits, cnf, itarget, otarget, units, out_c);
365+
return true;
376366
}
377-
printf(" ) found ==> added = %d, deleted = %d\f_dx", nAddedCls, itarget.size() + otarget.size());
378-
pClauseSet(cnf, itarget, otarget);
379-
#endif
380-
// substitute
381-
if (nAddedCls) substitute_x(v, nAddedCls, nAddedLits, cnf, itarget, otarget, units, out_c);
382-
return true;
383367
}
384-
freeze_arities(cnf, itarget);
385368
return false;
386369
}
387370

@@ -677,60 +660,39 @@ namespace pFROST {
677660
_PFROST_D_ bool find_xor_gate(const uint32& dx, const uint32& nOrgCls, const int& xor_max_arity, CNF& cnf, OT& ot, cuVecU* resolved, uint32* out_c, uint32& nAddedCls, uint32& nAddedLits)
678661
{
679662
assert(dx > 1);
680-
assert(checkMolten(cnf, ot[dx], ot[FLIP(dx)]));
663+
assert(dx > 1);
664+
const uint32 fx = FLIP(dx), v = ABS(dx);
665+
assert(checkMolten(cnf, ot[dx], ot[fx]));
681666
OL& itarget = ot[dx];
667+
OL& otarget = ot[fx];
682668
for (S_REF* i = itarget; i != itarget.end(); i++) {
683669
SCLAUSE& ci = cnf[*i];
684670
int size = ci.size();
685671
int arity = size - 1; // XOR arity
686-
if (ci.learnt() || size < 3 || arity > xor_max_arity || arity > SH_MAX_BVE_OUT1) continue;
687-
assert(ci.original());
688-
// share to out_c except dx
689-
shareXORClause(dx, ci, out_c);
672+
if (ci.learnt() || size < 3 || arity > xor_max_arity || arity > SH_MAX_BVE_OUT) continue;
673+
assert(arity <= SH_MAX_BVE_OUT1);
674+
// share to out_c
675+
shareXORClause(ci, out_c);
690676
// find arity clauses
691-
int itargets = 0;
692-
for (int j = 0; j < arity; j++) {
693-
S_REF r = find_fanin(dx, j, cnf, itarget, out_c, arity);
694-
if (r == GNOREF) break;
695-
assert(cnf[r].original());
696-
cnf[r].melt(), itargets++;
697-
}
698-
if (itargets < arity) {
699-
freeze_arities(cnf, itarget);
700-
continue;
701-
}
702-
// find all +/-
703-
uint32 f_dx = FLIP(dx);
704-
S_REF r1 = find_all(f_dx, cnf, ot, out_c, arity);
705-
if (r1 == GNOREF) break;
706-
flip_all(out_c, arity);
707-
S_REF r2 = find_all(f_dx, cnf, ot, out_c, arity);
708-
if (r2 == GNOREF) break;
709-
assert(cnf[r1].original());
710-
assert(cnf[r2].original());
711-
cnf[r1].melt(), cnf[r2].melt();
712-
// check resolvability
713-
uint32 v = ABS(dx);
714-
OL& otarget = ot[f_dx];
715-
nAddedCls = 0, nAddedLits = 0;
716-
countSubstituted(v, cnf, itarget, otarget, nAddedCls, nAddedLits);
717-
if (nAddedCls > nOrgCls) {
718-
cnf[r1].freeze(), cnf[r2].freeze();
719-
break;
720-
}
721-
// can be substituted
722-
#if VE_DBG
723-
printf("c | Gate %d = XOR(", ABS(dx));
724-
for (int k = 0; k < arity; k++) {
725-
printf(" %d", ABS(out_c[k]));
726-
if (k < arity - 1) printf(",");
677+
uint32 parity = 0;
678+
int itargets = (1 << arity);
679+
while (--itargets && makeArity(cnf, ot, parity, out_c, size));
680+
assert(parity < (1UL << size)); // overflow check
681+
assert(itargets >= 0);
682+
if (itargets)
683+
freeze_arities(cnf, itarget, otarget);
684+
else {
685+
ci.melt();
686+
// check resolvability
687+
nAddedCls = 0, nAddedLits = 0;
688+
countSubstituted(v, cnf, itarget, otarget, nAddedCls, nAddedLits);
689+
if (nAddedCls > nOrgCls) {
690+
freeze_arities(cnf, itarget, otarget);
691+
break;
692+
}
693+
return true;
727694
}
728-
printf(" ) found ==> added = %d, deleted = %d\f_dx", nAddedCls, itarget.size() + otarget.size());
729-
printGate(cnf, itarget, otarget);
730-
#endif
731-
return true;
732695
}
733-
freeze_arities(cnf, itarget);
734696
return false;
735697
}
736698

‎gpu/pfdevice.cuh‎

Lines changed: 15 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -442,12 +442,23 @@ namespace pFROST {
442442
*saved++ = lit, *saved++ = 1;
443443
}
444444

445-
_PFROST_D_ void saveResolved(uint32*& saved, SCLAUSE& c)
445+
_PFROST_D_ void saveResolved(uint32*& saved, SCLAUSE& c, const uint32& x)
446446
{
447+
uint32* first = saved, * witness = NULL;
447448
assert(c.original());
448-
uint32* lit = c, * cend = c.end();
449-
while (lit != cend)
450-
*saved++ = *lit++;
449+
uint32* k = c, * cend = c.end();
450+
while (k != cend) {
451+
const uint32 lit = *k++;
452+
if (lit == x) {
453+
witness = saved;
454+
}
455+
*saved++ = lit;
456+
}
457+
assert(witness >= first);
458+
if (witness != first)
459+
devSwap(*first, *witness);
460+
else
461+
assert(*witness == *first);
451462
*saved++ = c.size();
452463
}
453464

0 commit comments

Comments
 (0)