We currently have implementations of 2 heuristics in v1: BO (available in the shai branch) and Marabou (in the marabou branch).
For the v2-API, we might want to integrate both as well. This issue is here to find out whether it is a good idea to amend the current v2 redesign in order for workers to incorporate those heuristics (and thereby returning not just sat, unsat or unknown back to the server, but also marabou-sat, etc., and bo-sat), or to take a different approach.
bo-sat may not be needed if we take the same approach as the v1 implementation, which uses Z3 to verify BO's suggestions.
We currently have implementations of 2 heuristics in v1: BO (available in the
shaibranch) and Marabou (in themaraboubranch).For the v2-API, we might want to integrate both as well. This issue is here to find out whether it is a good idea to amend the current v2 redesign in order for workers to incorporate those heuristics (and thereby returning not just
sat,unsatorunknownback to the server, but alsomarabou-sat, etc., andbo-sat), or to take a different approach.bo-satmay not be needed if we take the same approach as the v1 implementation, which uses Z3 to verify BO's suggestions.