Commit 2bcdcb30 authored by Daniel Le Berre's avatar Daniel Le Berre

ACLIB files for Sat4j

parent 4d2dea08
Pipeline #10266 passed with stages
in 88 minutes and 2 seconds
# Automated Configuration Library files for Sat4j
Those files were created to describe Sat4j during the [Configurable SAT Solver Challenge 2013](http://www.cs.ubc.ca/labs/beta/Projects/CSSC2013/).
They should be compatible with the more recent [Algorithm Configuration Library](http://www.aclib.net/).
def get_solver_callstring(instance_filename, seed, param_hashmap)
solver_callstring = "java -Xms1g -Xmx1g -jar sat4j-sat.jar -s Default -S "
params_string = "PARAMS=SearchParams"
param_hashmap.keys.each_with_index do |param_name, index|
param_value = param_hashmap[param_name]
if param_name == "CLADECAY"
params_string += "/claDecay:"+param_value
next
end
if param_name == "INITCONFLICTBOUND"
params_string += "/initConflictBound:"+param_value
next
end
if param_name == "VARDECAY"
params_string += "/varDecay:"+param_value
next
end
if param_name == "CONFLICTBOUNDINCFACTOR"
params_string += "/conflictBoundIncFactor:"+param_value
next
end
solver_callstring += "#{param_name}=#{param_value}"
if param_value == "LubyRestarts"
solver_callstring += "/factor:"+param_hashmap["LUBYFACTOR"]
end
if param_value == "FixedPeriodRestarts"
solver_callstring += "/period:"+param_hashmap["FIXEDPERIOD"]
end
solver_callstring += ","
end
solver_callstring += params_string
return solver_callstring + " #{instance_filename}"
end
RESTARTS {Glucose21Restarts,ArminRestarts,FixedPeriodRestarts,LubyRestarts,NoRestarts,MiniSATRestarts}[Glucose21Restarts]
LUBYFACTOR {16,32,64,100,128,256,512,1024,2048}[512]
LUBYFACTOR|RESTARTS in {LubyRestarts}
FIXEDPERIOD {1,10,100,1000,5000,10000,50000,100000}[100]
FIXEDPERIOD|RESTARTS in {FixedPeriodRestarts}
PHASE {NegativeLiteralSelectionStrategy,PositiveLiteralSelectionStrategy,RSATPhaseSelectionStrategy,UserFixedPhaseSelectionStrategy,RandomLiteralSelectionStrategy,RSATLastLearnedClausesPhaseSelectionStrategy,PhaseCachingAutoEraseStrategy,PhaseInLastLearnedClauseSelectionStrategy}[RSATPhaseSelectionStrategy]
CLADECAY {0.999,0.995,0.99,0.95,0.9, 0.7,0.5}[0.999]
INITCONFLICTBOUND {1,10,100,1000}[100]
INITCONFLICTBOUND|RESTARTS in {MiniSATRestarts,ArminRestarts}
VARDECAY {0.99,0.95,0.9, 0.7, 0.5}[0.95]
CONFLICTBOUNDINCFACTOR {1.5,2,3,4}[2]
CONFLICTBOUNDINCFACTOR|RESTARTS in {MiniSATRestarts}
SIMP {NO_SIMPLIFICATION,SIMPLE_SIMPLIFICATION,EXPENSIVE_SIMPLIFICATION}[EXPENSIVE_SIMPLIFICATION]
CLEANING {ACTIVITY,LBD,LBD2}[LBD2]
{RESTARTS=Glucose21Restarts,CLEANING=ACTIVITY}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment