Benchmark Results #14

Activity

1. isPANN commented on Oct 29, 2025

   

   isPANN

   on Oct 29, 2025

   Last edited by isPANN

   CollaboratorAuthor

   More actions

   • 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
2. isPANN

   closed this as completedon Nov 3, 2025