Conclusions

Discussed current state-of-the-art in propositional

reasoning and search.

Shift to 10,000+ variables and 10^6 clauses has

opened up new applications.

Methodology: Find compact SAT encoding;

Use off-the-shelf SAT Solver.

Analogous to LP and MIP approaches.

Previous slide

Next slide

Back to first slide

View graphic version