| 摘要 |
A satisfiability checking system may include a single instruction, multiple data (SIMD) machine configured to execute multiple threads in parallel. The multiple threads may be divided among multiple blocks. The SIMD machine may be further configured to perform satisfiability checking of a formula including multiple parts. The satisfiability checking may include assigning one or more of the parts to one or more threads of the multiple threads of a first block of the multiple blocks. The satisfiability checking may further include processing the assigned one or more parts in the first block such that first results are calculated based on a first proposition. The satisfiability checking may further include synchronizing the results among the one or more threads of the first block. |
