$ cutsat --help

cutsat is a solver for feasibiliy problems in linear integer arithmetic. as input formats, it supports the smt, mps, and opb formats. developement is still underway, but you can check out the developement packages from our launchpad page. for any questions or discussion please see the google group.

$ cutsat --show-benchmarks

these are the benchmarks we used in our cade 2011 paper. you can download the binary (64bit linux, early prototype) we used, and all benchmarks (tar.bz [122mb]), or one of the individual problem sets:

• miplib2003 (tar.bz [27mb])
  pure integer problems from the miplib2003 library with the optimization constraints removed;
• pb2010 (tar.bz [84mb])
  problems from the 2010 pseudo-boolean competition that were submitted and selected in 2010;
• dillig (tar.bz [259kb])
  problems from the 'cuts from proofs' paper;
• slacks (tar.bz [402kb])
  problems from the 'cuts from proofs' paper with slack variables introduced to bound the variables from below;
• pigeons (tar.bz [24kb])
  problems encoding the pigeonhole principle;
• primes (tar.bz [9kb])
  problems encoding a tight cone around a n-dimensional point of the first n prime numbers.

$ cutsat --science

• slides from deduction at scale 2011 seminar.