Я пытаюсь решить проблему SAT с 12000+ логических переменных с использованием Z3. Я ожидаю, что большинство переменных будет иметь значение false в решении. Есть ли способ направить или намекнуть Z3 как SAT-решатель, чтобы сначала попробовать «полярность ложная»? Я попробовал это с cryptominisat 2 и получил хорошие результаты.