我试图使用Z3解决12000+布尔变量的SAT问题.我希望大多数变量在解决方案中评估为false.有没有办法引导或提示Z3作为SAT求解器首先尝试"极性假"？我已经尝试使用cryptominisat 2并取得了良好的效果.
z3
z3 ×1