Benchmark Results

[isPANN]

Config	BooleanInference	IP-Gurobi.Optimizer	X-SAT
10x10	125.7 ms	67.5 ms	65.0 ms
12x12	416.9 ms	797.7 ms	106.9 ms
14x14	1.73 s	1.63 s	183.2 ms
16x16	7.96 s	7.6 s	337.5 ms
18x18	/	/	1.42 s
20x20	/	/	2.53 s
22x22	/	/	7.28 s

[isPANN]

• Use different baselines

Category	Representative Solvers / Methods	Branching Strategy	Reference / Repo
Classic CDCL	MiniSAT, Glucose, Kissat, CaDiCaL	Single-variable EVSIDS-based branching	Kissat
Structure-aware SAT	CryptoMiniSat, MapleLCMDist, Lingeling	XOR-aware and local-structure heuristics	CryptoMiniSat
Block / Cube Branching	Blocked Clause Decomposition, Cube-and-Conquer	Branch on variable blocks or sub-formulas	Cube & Conquer
VSIDS Variants	MapleSAT, Glucose-syrup	Activity-based heuristics with adaptive decay	MapleSAT
Neural-guided SAT	NeuroSAT, NeuroGlucose, NeuroCore	NN predicts sets of important variables	NeuroSAT
Parallel / Portfolio	ManySAT, PaInleSS, Treengeling	Parallel exploration of disjoint branch sets	PaInleSS
Local Search	WalkSAT, probSAT	Multi-variable flips (non-CDCL local search)	/

• Test on more diffrent instances (problem structure?) - Later

Type	Examples	Link
Arithmetic (Add/Mul)	c6288, mult16, adder32	ISCAS-85/89
Equivalence Checking	eq_check_mult32, crc32_eq	EPFL Benchmarks
Cryptographic Circuits	AES4, SHA1_round, DES	CryptoSAT / Bristol Fashion
Control Logic	s9234, s13207, s38584	ISCAS-89 / ITC-99
Random 3-SAT	300v_4.26r.cnf	SATLIB
Industrial / Model Checking	bmc_3, vis_elevator	HWMCC