PLRS

PLRS (pronounced "polaris") is a general-purpose reasoning system that combines many of the research areas currently being investigated at CIRL. It works with a Pseudo-Boolean ("P") and Lifted ("L") representation of domain knowledge, and also uses dynamic backtracking as in RELSAT to avoid reexamining portions of the search space that are similar to one another. PLRS is a production tool. The intention is that it be comparable in speed to existing engines such as NTAB and RELSAT, but working with a far more expressive and flexible representation language.

Pointers

Techniques used:
Pseudo-Boolean
Quantified propositional logic

Application area:
Satisfiability

Back to the CIRL Overview Page.