Rethink the scheduling process so as to avoid restarting the search at root level.
The problem is related to creating constraints and flaws at a deeper level than root level.
As regards constraints, they can be created preventively at root level between couples of atoms.
Creating flaws is a bit more complex, since it requires the introduction of causal constraints.
Investigate whether it is possible to introduce such constraints through the void record(const std::vector<lit> &lits) procedure of the sat_core.
Rethink the scheduling process so as to avoid restarting the search at root level.
The problem is related to creating constraints and flaws at a deeper level than root level.
As regards constraints, they can be created preventively at root level between couples of atoms. Creating flaws is a bit more complex, since it requires the introduction of causal constraints. Investigate whether it is possible to introduce such constraints through the
void record(const std::vector<lit> &lits)procedure of thesat_core.