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