LSTECH_MAPLE is a high-performance open source SAT solver which can solve SAT and UNSAT problems. It ranked the second of Main Track SAT in the 2021 SAT Competition. lstech_maple improves the Conflict Driven Clause Learning (CDCL) algorithm by relaxing the CDCL approach and adding local search to adjust the solution. lstech_maple is developed by C++ and supports reading and writing Conjunctive Normal Form (opens new window) (CNF) files.



Parameter Explanation Default
step-size Initial step size 0.40
step-size-dec Step size decrement 0.000001
min-step-size Minimal step size
var-decay The variable activity decay factor
cla-decay The clause activity decay factor 0.999
rnd-freq The frequency with which the decision heuristic tries to choose a random variable 0
rnd-seed Used by the random variable selection 91648253
ccmin-mode Controls conflict clause minimization (0=none, 1=basic, 2=deep) 2
phase-saving Controls the level of phase saving (0=none, 1=limited, 2=full) 2
rnd-init Randomize the initial activity false
rfirst The base restart interval 100
rinc Restart interval increase factor 2
gc-frac The fraction of wasted memory allowed before a garbage collection is triggered 0.20
chrono Controls if to perform chrono backtrack 100
confl-to-chrono Controls number of conflicts to perform chrono backtrack 4000


Parameter Explanation Default
lbd-limit specifies the maximum lbd of learnts to be screened for duplicates. 14
min-dup-app specifies the minimum number of learnts to be included into db. 2
dupdb-init specifies the initial maximal duplicates DB size. 1000000


Parameter Explanation Default
verb Verbosity level (0=silent, 1=some, 2=more) 1
pre Completely turn on/off any preprocessing. true
dimacs If given, stop after preprocessing and write the result to this file.
cpu-lim Limit on CPU time allowed in seconds. INT32_MAX = 2147483647
mem-lim Limit on memory usage in megabytes. INT32_MAX
drup Generate DRUP UNSAT proof. false
drup-file DRUP UNSAT proof ouput file. ""


Parameter Explanation Default
asymm Shrink clauses by asymmetric branching. false
elim Perform variable elimination. true
rcheck Check if a clause is already implied. (costly) false
simp-gc-frac The fraction of wasted memory allowed before a garbage collection is triggered during simplification. 0.5
grow Allow a variable elimination step to grow by a number of clauses. 0
cl-lim Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit 20
sub-lim Do not check if subsumption against a clause larger than this. -1 means no limit. 1000


Parameter Explanation
help Print help message.
help-verb Print verbose help message.

Examples of Usage

./lstech_maple [options] <input-file> <result-output-file>
./lstech_maple --help

Notice that we need to add -- before HELP OPTIONS and add - before other OPTIONS. When setting the parameter, there should be no space before or after =.

Solve CNF files

./lstech_maple ./input.cnf
./lstech_maple -cpu-lim=1000 ./input.cnf ./output.cnf
Last Updated: 05/16/2022