Skip to content

Commit

Permalink
activity,initialization: order by variable
Browse files Browse the repository at this point in the history
Instead of using the search order 1, N, N-1, N-2, ..., have the solver
use the order 1, 2, 3, 4, ... by default. This order maps better to the
way formulas are typically generated. The first variables correspond to
the variables of the input problem, which empirically results in a
quicker exploration of the input search space.

Signed-off-by: Norbert Manthey <[email protected]>
  • Loading branch information
conp-solutions committed May 11, 2022
1 parent 384de59 commit d2c2b66
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion minisat/core/Solver.cc
Original file line number Diff line number Diff line change
Expand Up @@ -94,7 +94,7 @@ static IntOption opt_ccmin_mode(_cat,
IntRange(0, 3));
static IntOption
opt_phase_saving(_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
static IntOption opt_init_act(_cat, "rnd-init", "Initial activity is 0:0, 1:random, 2:1000/v, 3:v", 0, IntRange(0, 3));
static IntOption opt_init_act(_cat, "rnd-init", "Initial activity is 0:0, 1:random, 2:1000/v, 3:v", 2, IntRange(0, 3));
static IntOption opt_init_act_init(_cat, "rnd-init-init", "Initial activity for rnd-init=2", 1000, IntRange(1, INT32_MAX));
static IntOption opt_restart_first(_cat, "rfirst", "The base restart interval", 100, IntRange(1, INT32_MAX));
static IntOption opt_restart_strategy(_cat, "restart", "How to schedule restarts (split,luby,dynamic)", 1, IntRange(1, 3));
Expand Down

0 comments on commit d2c2b66

Please sign in to comment.