an actual SAT solver

[guyvdbroeck]

Currently we have functionality to determine satisfiability and model counts, but we don't actually have a SAT solver that can output a satisfying assignment. It's not hard to implement: it could look similar to the MAP inference code in https://github.com/Juice-jl/ProbabilisticCircuits.jl/blob/master/src/queries/map.jl. It could even be a 'conditional' SAT solver where you fix some of the variables and ask for a satisfying assignment to the others. It could even be done in batch, just like the MAP code, and parallelized on the GPU!