1. A system comprising: a single instruction, multiple data (SIMD) machine configured to: execute a plurality of threads in parallel, the plurality of threads divided among a plurality of blocks; and perform satisfiability checking of a formula including a plurality of parts, the satisfiability checking comprising: assigning one or more of the parts to one or more threads of the plurality of threads of a first block of the plurality of blocks; processing the assigned one or more parts in the first block such that first results are calculated based on a first proposition; and synchronizing the results among the one or more threads of the first block.