Lower and Upper bound approximation that gives sound and complete results.
Slicing, Unrolling ....
KodKod (minimize the search space LB, UB)
SMT (UF, preprocessing)
SAT (Benchmark used in Opium, debian apt-get)
DL fragment
Implement using queries against Neo4j graph db
many-sorted