LSTECH_MAPLE

Introduction

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.

Parameters

CORE OPTIONS

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

DUP-LEARNTS OPTIONS

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

MAIN OPTIONS

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.	""

SIMP OPTIONS

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

HELP OPTIONS

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