Main options:

-h [ --help ]

Print simple help

--hhelp

Print extensive help

-v [ --version ]

Print version info

--verb arg (=1)

[0-10] Verbosity of solver. 0 = only solution

-r [ --random ] arg (=0)

[0..] Random seed

-t [ --threads ] arg (=1)

Number of threads

--maxtime arg

Stop solving after this much time (s)

--maxconfl arg

Stop solving after this many conflicts

-m [ --mult ] arg (=3)

Time multiplier for all simplification cutoffs

--nextm arg (=1)

Global multiplier when the next inprocessing should take place

--memoutmult arg (=1)

Multiplier for memory-out checks on inprocessing functions. It limits things such as clause-link-in. Useful when you have limited memory but still want to do some inprocessing