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!
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!