Template clauses based sat techniques

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, the template SAT problem comprises a plurality of clauses and 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;
• and
• 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;
• 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.

A method to solve a template SAT problem associated with a model that is modeled checked, said method is performed by a computerized device, said method comprising:

• receiving the template SAT problem, the template SAT problem comprising a plurality of clauses and 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;
• determining a value of the literal in a cycle based on the template clause and a temporal shift, said determining the value of the literal comprises:
• determining a concrete clause of the plurality of concrete clauses based on the template clause and the temporal shift;
• and
• determining a deduced clause based on at least the value of the literal in the cycle;
• deducing a solution to the template SAT problem, the solution is selected from the group consisting of a satisfying assignment and a proof of unsatisfiability;
• and
• outputting the solution.

A computer program product comprising a non-transitory computer readable medium retaining program instructions, which instructions when read by a processor, cause the processor to perform the steps of:

• receiving the template SAT problem, the template SAT problem comprising a plurality of clauses and 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;
• determining a value of the literal in a cycle based on the template clause and a temporal shift, said determining the value of the literal comprises:
• determining a concrete clause of the plurality of concrete clauses based on the template clause and the temporal shift;
• and
• determining a deduced clause based on at least the value of the literal in the cycle;
• and
• deducing a solution to the template SAT problem, the solution is selected from the group consisting of a satisfying assignment and a proof of unsatisfiability.