Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure1 论文
2007Journal on Satisfiability Boolean Modeling and Computation引用 311
Constraint Satisfaction and OptimizationFormal Methods in VerificationLogic, Reasoning, and Knowledge
摘要
In order to facilitate automated reasoning about large Boolean combinations of non-linear arithmetic constraints involving transcendental functions, we provide a tight integration of recent SAT solving techniques with interval-based arithmetic constr