timsat2 Only accepts CNF python interpret.py tests/pigeonhole/pigeon-1.cnf Uses the Conflict Driven Clause Learning model (with watched literals) as presented in: http://satassociation.org/articles/FAIA185-0131.pdf