next up previous contents
Next: BDD WalkSAT solver options Up: Reference - Command line Previous: General solver options   Contents

SMURF Solver options

-lemma-out-file <string> - File to dump lemmas to [default='''']
-lemma-in-file <string> - File to read lemmas from [default='''']
-csv-trace-file <string> - File to save execution trace in
    CSV format [default='''']
-var-stat-file <string> - File to save var stats [default='''']
-cvs-depth-breadth-file <string> - Save depth/breadth statistic [default='''']
-backjumping <number> - Enable/Disable backjumping (1/0)
    [default=1]
-max-cached-lemmas <number>, - Set the maximum # of lemmas
       -L <number>   [default=5000]
-autarky-smurfs <number> - Use Autarky Smurfs in the solver (1/0)
    [default=0]
-autarky-lemmas <number> - Use Autarky Lemmas in the solver (Currently Unavailiable) (1/0)
    [default=0]
-sbj <number> - Super backjumping [default=0]
-max-vbles-per-smurf <number>, - set the maximum number variables per
       -S <number>   smurf [default=8]
-backtracks-per-report <number> - set the number of backtracks per report
    [default=10000]
-max-brancher-cp <number> - set the choice point limit (0=no limit)
    [default=0]
-brancher-trace-start <number> - number of backtracks to start the trace
    (when debug=9) [default=0]
-heuristic <string>, - Choose heuristic j=LSGB, l=Chaff-like
       -H <string>   lemma based, i=Interactive [default="j"]
-jheuristic-k <number>, - set the value of K [default=3.000000]
      -K <number>    
-jheuristic-k-true <number> - set the value of True state [default=0.000000]
-jheuristic-k-inf <number> - set the value of the inference multiplier
    [default=1.000000]


next up previous contents
Next: BDD WalkSAT solver options Up: Reference - Command line Previous: General solver options   Contents
John Franco 2011-09-15