Patent ID: 8407175

Claim:
A SAT solving apparatus having a processor, the SAT solving apparatus comprising: a receiver configured to receive a template SAT problem associated with a model that is modeled checked, wherein the model is a bounded model, the template SAT problem comprises a plurality of clauses, the plurality of clauses comprises a template clause, the template clause represents a plurality of concrete clauses each associated with a different temporal shift, the template clause is associated with a literal; a literal value determinator configured to determine a value of the literal in a cycle based on the template clause and a temporal shift, said literal value determinator comprising: a temporal shifter configured to determine a concrete clause of the plurality of concrete clauses based on the template clause and the temporal shift; a clauses deducer configured to determine a deduced clause, said clauses deducer is configured to utilize said literal value determinator; and a clauses repository configured to retain the plurality of clauses and the deducted clause; a template clause constructor configured to determine a new template clause based on at least two clauses; and wherein said SAT solving apparatus is configured to deduce a solution to the template SAT problem, the solution is selected from the group consisting of a satisfying assignment and a proof of unsatisfiability.