Lifted WSAT
We have implemented a version of WSAT
that works directly on QPROP expressions.
The implementation also does the standard Polytime Simplification of propagating
the effects of facts (unit resolution).
The QPROP expressions are not expanded to the usual propositional SAT
form. This means that problems can be solved that would expand to
millions of ground clauses and would be far too large to be handled by
previous WSAT implementations.
Pointers
- Techniques used:
- QPROP
- WSAT
- Polytime Simplification
- Application Areas:
- Satisfiability
Back to the CIRL Overview Page.