Function synthesis for maximizing model counting

Thomas Vigouroux, Marius Bozga, Cristian Ene +1

Given a boolean formula $\Phi$(X, Y, Z), the Max\#SAT problem asks for finding a partial model on the set of variables X, maximizing its number of projected models over the set of var…