For the moment Status contains a variant Unknown(Vec<Branch<Space>>) but what if we separate the branches from the status? It would mean that even in case of satisfiability or unsatisfiability a branch queue would still exist. Does it make any sense?

For unsatisfiability, could it be used for fuzzy constraints? Meaning that we still want to explore the tree even if some constraints are failed. For example in case a problem has no solution we want to minimize the number of constraints violated.