Welcome to RegSTAB Home Page!

RegSTAB is a SAT-Solver able to deal with formulae patterns.

e.g. any SAT-Solver can tell you that each of the following formulae is unsatisfiable:

• P₁ ∧ (P₁ ⇒ P₂) ∧ ¬P₂
• P₁ ∧ (P₁ ⇒ P₂) ∧ (P₂ ⇒ P₃) ∧ ¬P₃
• P₁ ∧ (P₁ ⇒ P₂) ∧ (P₂ ⇒ P₃) ∧ (P₃ ⇒ P₄) ∧ ¬P₄
• …

P₁ ∧ (Λ_i=1..n P_i ⇒ P_i+1) ∧ ¬P_n+1

This may be useful e.g. to prove circuit specifications independently of the number of bits.

(if display is weird click here)


Download RegSTAB