| 摘要 |
Systems and methods are disclosed for deciding a satisfiability problem with linear and non-linear operations by: encoding non-linear integer operations into encoded linear operations with Boolean constraints by Booleaning and linearizing, combining the linear and encoded linear operations into a formula, solving the satisifiability of the formula using a solver, wherein the encoding and solving includes at least one of following: a. Booleanizing one of the non-linear operands by bit-wise structural decomposition b. Linearizing a non-linear operator by selectively choosing one of the operands for Booleanization c. Solving using an incremental lazy bounding refinement (LBR) procedure without re-encoding formula, and verifying the linear and non-linear operations in a computer software.
|
