Relaxed_LCMDCBDL_newTech解读中目前不清楚的地方2021-5-18

#ifdef BIN_DRUP

static int buf_len;
static unsigned char drup_buf[];
static unsigned char* buf_ptr;

static inline void byteDRUP(Lit l){

unsigned int u = 2 * (var(l) + 1) + sign(l);
do{
    *buf_ptr++ = u & 0x7f | 0x80; buf_len++;
    u = u >> 7;
}while (u);
*(buf_ptr - 1) &= 0x7f; // End marker of this unsigned number.

}

template<class V>
static inline void binDRUP(unsigned char op, const V& c, FILE* drup_file){

assert(op == ‘a‘ || op == ‘d‘);
*buf_ptr++ = op; buf_len++;
for (int i = 0; i < c.size(); i++) byteDRUP(c[i]);
*buf_ptr++ = 0; buf_len++;
if (buf_len > 1048576) binDRUP_flush(drup_file);

}

static inline void binDRUP_strengthen(const Clause& c, Lit l, FILE* drup_file){

*buf_ptr++ = ‘a‘; buf_len++;
for (int i = 0; i < c.size(); i++)
if (c[i] != l) byteDRUP(c[i]);
*buf_ptr++ = 0; buf_len++;
if (buf_len > 1048576) binDRUP_flush(drup_file);

}

static inline void binDRUP_flush(FILE* drup_file){

fwrite(drup_buf, sizeof(unsigned char), buf_len, drup_file);
//fwrite_unlocked(drup_buf, sizeof(unsigned char), buf_len, drup_file);
buf_ptr = drup_buf; buf_len = 0;

}

#endif

bool Solver::addClause_(vec<Lit>& ps)
{

assert(decisionLevel() == 0);
if (!ok) return false;

// Check if clause is satisfied and remove false/duplicate literals:
sort(ps);
Lit p; int i, j;

if (drup_file){

add_oc.clear();
for (int i = 0; i < ps.size(); i++) add_oc.push(ps[i]); }

for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
if (value(ps[i]) == l_True || ps[i] == ~p)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
ps.shrink(i - j);

if (drup_file && i != j){
#ifdef BIN_DRUP
binDRUP(‘a‘, ps, drup_file);
binDRUP(‘d‘, add_oc, drup_file);
#else
for (int i = 0; i < ps.size(); i++)
fprintf(drup_file, "%i ", (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1));
fprintf(drup_file, "0\n");

fprintf(drup_file, "d ");
for (int i = 0; i < add_oc.size(); i++)
fprintf(drup_file, "%i ", (var(add_oc[i]) + 1) * (-2 * sign(add_oc[i]) + 1));
fprintf(drup_file, "0\n");
#endif
}

if (ps.size() == 0)
return ok = false;
else if (ps.size() == 1){
uncheckedEnqueue(ps[0]);
return ok = (propagate() == CRef_Undef);
}else{
CRef cr = ca.alloc(ps, false);
clauses.push(cr);
attachClause(cr);
}

return true;

}

void Solver::removeClause(CRef cr) {
Clause& c = ca[cr];

if (drup_file){
if (c.mark() != 1){
#ifdef BIN_DRUP
binDRUP(‘d‘, c, drup_file);
#else
fprintf(drup_file, "d ");
for (int i = 0; i < c.size(); i++)
fprintf(drup_file, "%i ", (var(c[i]) + 1) * (-2 * sign(c[i]) + 1));
fprintf(drup_file, "0\n");
#endif
}else
printf("c Bug. I don‘t expect this to happen.\n");
}

detachClause(cr);
// Don‘t leave pointers to free‘d memory!
if (locked(c)){
Lit implied = c.size() != 2 ? c[0] : (value(c[0]) == l_True ? c[0] : c[1]);
vardata[var(implied)].reason = CRef_Undef; }
c.mark(1);
ca.free(cr);
}

search函数传播遇到冲突代码段中有以下相关代码：

if (drup_file){
#ifdef BIN_DRUP
binDRUP(‘a‘, learnt_clause, drup_file);
#else
for (int i = 0; i < learnt_clause.size(); i++)
fprintf(drup_file, "%i ", (var(learnt_clause[i]) + 1) * (-2 * sign(learnt_clause[i]) + 1));
fprintf(drup_file, "0\n");
#endif
}

solve_最后也有相关代码段

#ifdef BIN_DRUP
if (drup_file && status == l_False) binDRUP_flush(drup_file);
#endif