331 lines
7.7 KiB
C
331 lines
7.7 KiB
C
#include "eliminate.h"
|
|
#include "gates.h"
|
|
#include "inline.h"
|
|
#include "resolve.h"
|
|
|
|
#include <inttypes.h>
|
|
|
|
static unsigned
|
|
occurrences_literal (kissat * solver, unsigned lit, bool * update)
|
|
{
|
|
assert (!solver->watching);
|
|
|
|
watches *watches = &WATCHES (lit);
|
|
LOG ("literal %s has %u watches", LOGLIT (lit), watches->size);
|
|
|
|
const unsigned clslim = solver->bounds.eliminate.clause_size;
|
|
|
|
watch *begin = BEGIN_WATCHES (*watches), *q = begin;
|
|
const watch *end = END_WATCHES (*watches), *p = q;
|
|
|
|
const value *values = solver->values;
|
|
const word *arena = BEGIN_STACK (solver->arena);
|
|
|
|
bool failed = false;
|
|
unsigned res = 0;
|
|
|
|
while (p != end)
|
|
{
|
|
watch head = *q++ = *p++;
|
|
if (head.type.binary)
|
|
{
|
|
const unsigned other = head.binary.lit;
|
|
const value value = values[other];
|
|
assert (value >= 0);
|
|
if (value > 0)
|
|
{
|
|
kissat_eliminate_binary (solver, lit, other);
|
|
q--;
|
|
}
|
|
else
|
|
res++;
|
|
}
|
|
else
|
|
{
|
|
const reference ref = head.large.ref;
|
|
assert (ref < SIZE_STACK (solver->arena));
|
|
clause *c = (struct clause *) (arena + ref);
|
|
if (c->garbage)
|
|
q--;
|
|
else if (c->size > clslim)
|
|
{
|
|
LOG ("literal %s watches too long clause of size %u",
|
|
LOGLIT (lit), c->size);
|
|
failed = true;
|
|
break;
|
|
}
|
|
else
|
|
res++;
|
|
}
|
|
}
|
|
while (p != end)
|
|
*q++ = *p++;
|
|
SET_END_OF_WATCHES (*watches, q);
|
|
if (failed)
|
|
return UINT_MAX;
|
|
if (res != watches->size)
|
|
{
|
|
*update = true;
|
|
LOG ("literal %s actually occurs only %u times", LOGLIT (lit), res);
|
|
}
|
|
return res;
|
|
}
|
|
|
|
static inline clause *
|
|
watch_to_clause (kissat * solver,
|
|
const value * values, const word * arena,
|
|
clause * tmp, unsigned lit, watch watch)
|
|
{
|
|
clause *res;
|
|
if (watch.type.binary)
|
|
{
|
|
const unsigned other = watch.binary.lit;
|
|
assert (!values[other]);
|
|
tmp->lits[0] = lit;
|
|
tmp->lits[1] = other;
|
|
res = tmp;
|
|
}
|
|
else
|
|
{
|
|
const reference ref = watch.large.ref;
|
|
assert (ref < SIZE_STACK (solver->arena));
|
|
res = (struct clause *) (arena + ref);
|
|
assert (!res->garbage);
|
|
}
|
|
#ifdef NDEBUG
|
|
(void) solver;
|
|
(void) values;
|
|
#endif
|
|
return res;
|
|
}
|
|
|
|
static bool
|
|
generate_resolvents (kissat * solver, unsigned lit,
|
|
statches * watches0, statches * watches1,
|
|
uint64_t * resolved_ptr, uint64_t limit)
|
|
{
|
|
const unsigned not_lit = NOT (lit);
|
|
unsigned resolved = *resolved_ptr;
|
|
bool failed = false;
|
|
|
|
clause tmp0, tmp1;
|
|
memset (&tmp0, 0, sizeof tmp0);
|
|
memset (&tmp1, 0, sizeof tmp1);
|
|
tmp0.size = tmp1.size = 2;
|
|
|
|
const word *arena = BEGIN_STACK (solver->arena);
|
|
const value *values = solver->values;
|
|
value *marks = solver->marks;
|
|
|
|
const unsigned clslim = solver->bounds.eliminate.clause_size;
|
|
|
|
for (all_stack (watch, watch0, *watches0))
|
|
{
|
|
clause *c = watch_to_clause (solver, values, arena, &tmp0, lit, watch0);
|
|
|
|
for (all_literals_in_clause (other, c))
|
|
{
|
|
if (other == lit)
|
|
continue;
|
|
assert (!marks[other]);
|
|
marks[other] = 1;
|
|
}
|
|
|
|
for (all_stack (watch, watch1, *watches1))
|
|
{
|
|
clause *d =
|
|
watch_to_clause (solver, values, arena, &tmp1, not_lit, watch1);
|
|
|
|
LOGCLS (c, "first %s antecedent", LOGLIT (lit));
|
|
LOGCLS (d, "second %s antecedent", LOGLIT (not_lit));
|
|
|
|
bool satisfied_or_tautological = false;
|
|
size_t saved = SIZE_STACK (solver->resolvents);
|
|
|
|
INC (resolutions);
|
|
|
|
for (all_literals_in_clause (other, d))
|
|
{
|
|
if (other == not_lit)
|
|
continue;
|
|
if (marks[other])
|
|
{
|
|
LOG2 ("dropping repeated %s literal", LOGLIT (other));
|
|
continue;
|
|
}
|
|
const unsigned not_other = NOT (other);
|
|
if (marks[not_other])
|
|
{
|
|
LOG ("resolvent tautological on %s and %s "
|
|
"with second %s antecedent",
|
|
LOGLIT (NOT (other)), LOGLIT (other),
|
|
LOGLIT (not_lit));
|
|
satisfied_or_tautological = true;
|
|
break;
|
|
}
|
|
const value value = values[other];
|
|
if (value < 0)
|
|
{
|
|
LOG2 ("dropping falsified literal %s", LOGLIT (other));
|
|
continue;
|
|
}
|
|
assert (!value);
|
|
LOG2 ("including unassigned literal %s", LOGLIT (other));
|
|
PUSH_STACK (solver->resolvents, other);
|
|
}
|
|
|
|
if (satisfied_or_tautological)
|
|
{
|
|
RESIZE_STACK (solver->resolvents, saved);
|
|
continue;
|
|
}
|
|
|
|
if (++resolved > limit)
|
|
{
|
|
LOG ("limit of %u resolvent exceeded", limit);
|
|
failed = true;
|
|
break;
|
|
}
|
|
|
|
for (all_literals_in_clause (other, c))
|
|
{
|
|
if (other == lit)
|
|
continue;
|
|
const value value = values[lit];
|
|
assert (value <= 0);
|
|
if (value < 0)
|
|
{
|
|
LOG2 ("dropping falsified literal %s", LOGLIT (other));
|
|
continue;
|
|
}
|
|
PUSH_STACK (solver->resolvents, other);
|
|
}
|
|
|
|
size_t size_resolvent = SIZE_STACK (solver->resolvents) - saved;
|
|
LOGLITS (size_resolvent,
|
|
BEGIN_STACK (solver->resolvents) + saved, "resolvent");
|
|
|
|
if (size_resolvent > clslim)
|
|
{
|
|
LOG ("resolvent size limit exceeded");
|
|
failed = true;
|
|
break;
|
|
}
|
|
|
|
PUSH_STACK (solver->resolvents, INVALID_LIT);
|
|
}
|
|
|
|
for (all_literals_in_clause (other, c))
|
|
{
|
|
if (other == lit)
|
|
continue;
|
|
assert (marks[other] == 1);
|
|
marks[other] = 0;
|
|
}
|
|
|
|
if (failed)
|
|
break;
|
|
}
|
|
|
|
*resolved_ptr = resolved;
|
|
|
|
return !failed;
|
|
}
|
|
|
|
bool
|
|
kissat_generate_resolvents (kissat * solver, unsigned idx, unsigned *lit_ptr)
|
|
{
|
|
unsigned lit = LIT (idx);
|
|
unsigned not_lit = NOT (lit);
|
|
|
|
bool update = false;
|
|
uint64_t limit;
|
|
|
|
{
|
|
unsigned pos_count = occurrences_literal (solver, lit, &update);
|
|
unsigned neg_count = occurrences_literal (solver, not_lit, &update);
|
|
|
|
if (pos_count > neg_count)
|
|
{
|
|
SWAP (unsigned, lit, not_lit);
|
|
SWAP (size_t, pos_count, neg_count);
|
|
}
|
|
|
|
const unsigned occlim = solver->bounds.eliminate.occurrences;
|
|
if (pos_count && neg_count > occlim)
|
|
{
|
|
LOG ("not elimination of variable %u since limit hit", idx);
|
|
return false;
|
|
}
|
|
|
|
limit = pos_count + (uint64_t) neg_count;
|
|
if (pos_count)
|
|
{
|
|
limit += solver->bounds.eliminate.additional_clauses;
|
|
LOG ("trying elimination of variable %u limit %" PRIu64, idx, limit);
|
|
}
|
|
else
|
|
LOG ("eliminating pure literal %u (variable %u)", lit, idx);
|
|
}
|
|
|
|
const bool gates = kissat_find_gates (solver, lit);
|
|
kissat_get_antecedents (solver, lit);
|
|
|
|
uint64_t resolved = 0;
|
|
bool failed = false;
|
|
|
|
statches *gates0 = &solver->gates[0];
|
|
statches *gates1 = &solver->gates[1];
|
|
statches *antecedents0 = &solver->antecedents[0];
|
|
statches *antecedents1 = &solver->antecedents[1];
|
|
|
|
if (gates)
|
|
{
|
|
LOG ("resolving gates[0] against antecedents[1] clauses");
|
|
if (!generate_resolvents (solver, lit,
|
|
gates0, antecedents1, &resolved, limit))
|
|
failed = true;
|
|
else
|
|
{
|
|
LOG ("resolving gates[1] against antecedents[0] clauses");
|
|
if (!generate_resolvents (solver, not_lit,
|
|
gates1, antecedents0, &resolved, limit))
|
|
failed = true;
|
|
else if (solver->resolve_gate)
|
|
{
|
|
LOG ("need to resolved gates[0] against gates[1] too");
|
|
if (!generate_resolvents (solver, lit,
|
|
gates0, gates1, &resolved, limit))
|
|
failed = true;
|
|
}
|
|
}
|
|
}
|
|
else
|
|
{
|
|
LOG ("no gate extracted thus resolving all clauses");
|
|
if (!generate_resolvents (solver, lit,
|
|
antecedents0, antecedents1, &resolved, limit))
|
|
failed = true;
|
|
}
|
|
|
|
CLEAR_STACK (*gates0);
|
|
CLEAR_STACK (*gates1);
|
|
CLEAR_STACK (*antecedents0);
|
|
CLEAR_STACK (*antecedents1);
|
|
|
|
if (failed)
|
|
{
|
|
const unsigned idx = IDX (lit);
|
|
LOG ("elimination of variable %u failed", idx);
|
|
CLEAR_STACK (solver->resolvents);
|
|
if (update)
|
|
kissat_update_variable_score (solver, &solver->schedule, idx);
|
|
return false;
|
|
}
|
|
|
|
LOG ("resolved %" PRIu64 " resolvents", resolved);
|
|
*lit_ptr = lit;
|
|
|
|
return true;
|
|
}
|