| 011984fd82d62d609e776fbf5de75440 |
65eddad5cb79d158786b1bb8cc8a9156 |
p-center |
shuolin |
unsat |
empty |
no |
73f8011e3e38b3b7 |
arles_thres20_p10_r7533.cnf.xz |
main_2026,submissions_2025 |
| 01d6fa8efd18ebfecd06af408958477b |
89e6c0dfaac4291b05f6fab6cdb1bcb6 |
lights-out |
biere |
sat |
empty |
no |
c4904e76974e686d |
lightsout_sat_25_unbounded_direct_planted250_4_sat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 02a46668243d6dabab4cf74d3811f6b6 |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
d7d517c9d65b5b00 |
1x1x13_1x3x6_pair_4_2_0_2_5_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0359596347daa117da50950748bc06d1 |
0299f78d487106626abeef0ee0d999d9 |
scheduling |
shuolinli |
unknown |
http://hdl.handle.net/10138/359079 |
no |
0b1965d81933b901 |
j3037_9_rggt_bm1.cnf.xz |
main_2026,submissions_2022 |
| 03e49a528251af9a7b7e1ca03c33b162 |
34f302703c3dac7ed1d0f1780d055582 |
school-timetabling |
schreiber |
unknown |
empty |
no |
da265b63d5860785 |
schooltt-5-5-8-2-4-5-10-0.1-0.2-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 042cdc726a92bf0a2195b3b426f35bce |
0c3a50a05d6d290991939bf3ff4cdd05 |
independent-set-reconfiguration |
froleyks |
unknown |
http://hdl.handle.net/10138/359079 |
no |
93795ec2bc2036a5 |
reconf20_50_grid10_1_6141.cnf.xz |
main_2026,submissions_2022 |
| 043c91001968a1fbd1ef419540fcb396 |
7181a8834f7825a8c9eb0b22a01f16dd |
graph-coloring |
anders |
unsat |
empty |
no |
05e25e715866eed0 |
miles1500.72.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 04d0ae28e10d4a35ebab62f42f0200e8 |
17a18abdeb1394a6a74285cdb992e0a9 |
bitvector |
preiner |
unknown |
empty |
no |
e91d8d41899c4e67 |
168.smt2.cnf.xz |
main_2026 |
| 0757e47d262b75171c0040987e6d20ce |
2b3b2968688d2970c32f4be5d3978673 |
van-der-waerden |
gopalan |
unknown |
empty |
no |
360cda9975668ef6 |
vdwb_k6_n400.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 07df5e6f674201e2bf31bcaa8866ba75 |
b34d1a02feba23dd191c6de7cccbd14c |
cyclic-anti-bandwidth |
hieu |
unknown |
empty |
no |
be115844391d8456 |
cabp-V-nos6.mtx.rnd-k331.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 08cf53ca00dce11f5bfc02121c9bcd33 |
d21a4e8bc43efe0a7c22e8b2c401f0c4 |
greentao |
kullmann |
unsat |
empty |
no |
6f9c963fdddee738 |
GreenTao_2-3-5_528.cnf.xz |
anni_2022,crafted_2011,crafted_2012,main_2026 |
| 0922feab75c35d04d9b8df69013a6df0 |
c2a7f53d7d5730b48d1731b67384b937 |
prime-factoring |
bebel |
sat |
empty |
no |
00ee5450db843129 |
toughsat_22bits_0.cnf.xz |
main_2019,main_2026 |
| 09637d3bd641b4d733666a862e8918ea |
32ce26bb0c99d6817686fb5e331fc228 |
planning |
surynek |
sat |
empty |
no |
a81a17c0f8d2c869 |
mrpp_8x8#20_14.cnf.xz |
anni_2022,crafted_2013,main_2026 |
| 09e0775d2b51c49ec1ec4d214ee7c8c8 |
85fe5afbbb1517b269e8e83fd958ce93 |
ntil |
heule |
sat |
empty |
no |
96442fdb8fd349a3 |
ntil-90d-37.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0aea4286a11d91ee8fa356d5db046373 |
99895d52decdd3d43f743fe29387a060 |
cryptography |
md5gen |
unsat |
empty |
no |
66d62276382b25ba |
gus-md5-08.cnf.xz |
anni_2022,application_2012,application_2013,main_2026,portfolio_2012 |
| 0be1e12a8e7282d1a4e389bb90f6dbc7 |
e00905575ce250f56ba9b1a7fcf2c281 |
or_randxor |
yldirimoglu |
unsat |
http://hdl.handle.net/10138/563824 |
no |
c6db7912fbb278c5 |
or_randxor_k3_n600_m600.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 0c9da400944b002f90fd385d4fdab385 |
f1b7072876c4dacb6484714b5221c75c |
subsumptiontest |
nuttall |
sat |
http://hdl.handle.net/10138/563824 |
no |
c94c0b159a77a2a6 |
DivS_568_11.cnf.sanitized.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 0cab9100cdd8505069301d658d085899 |
464b73040b2ce7e256f6e4c808c95a3e |
termination-analysis |
fuhs |
unsat |
empty |
no |
83dfe77c4df5ab1f |
AProVE07-01.cnf.xz |
anni_2022,application_2009,application_2011,application_2014,industrial_2007,main_2026 |
| 0d082b8fa36f662217bee5524cd24d3a |
322afaef8f765de58baa9eb6152e4675 |
exam-scheduling |
zheng |
unsat |
empty |
no |
f908d0437f5ec99c |
mexam_23_20_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0d0fabe0fbca67a8740ebe8b8621d465 |
99b04239cfda61ddd0b44a1f89f839f9 |
allowable-seqence |
heule |
sat |
empty |
no |
9b38ac0f93da6e30 |
as-p147-l51-o0-rot-rfl-68-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0e06895600b5cd0b6fadb87e17bf8145 |
1a8ce89dd9b2a5b02dec155ad84ab2d4 |
ntil |
heule |
sat |
empty |
no |
d23de10f5ace6b94 |
ntil-90d-39.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0ec6bf97a96b9840ae84f1d1da4c4dcd |
c59fc0dab623a36b4fd0e16ec48cda2e |
count |
oertel |
unsat |
empty |
no |
8288c54c5c272eda |
count_p3_M19.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0efcbd10294eb001b16b4d126923372f |
81deeef64dce494fe5a20b648a0e140d |
lights-out |
biere |
unsat |
empty |
no |
41513af34f7ecb69 |
lightsout_sat_23_unbounded_direct_random50_2_unsat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 0f1070ba60b55aa62d3a98798a14700e |
812618b7377fad194c7d1ac3b4cee066 |
graph-coloring |
anders |
unsat |
empty |
no |
8efc2a3c70e9e052 |
mulsol.i.2.30.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 117b99ffa16d21cb4ccb1c66829b0c7e |
81add823efaa83e4c753b15f6fd9f893 |
graph-coloring |
reeves |
unsat |
empty |
no |
057ff55e702f5519 |
adv_gc_n50_k14_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 1236c1406a2749b8022b5196e93de589 |
f7832cc6c4564a762af37b6f4a1cb1ca |
ntil |
heule |
sat |
empty |
no |
1243d7e994c43a78 |
ntil-90d-33.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 123c397f55eeae78c45e8d973b8e9dce |
b25181ae33f318f3374db277a5a41950 |
bioinformatics |
bonet |
unsat |
empty |
no |
7e451837c9536fa6 |
rpoc_xits_09_UNSAT.cnf.xz |
anni_2022,application_2009,application_2011,application_2016,main_2026 |
| 12535b3264a9c88bac14522171b497ef |
b67a00e14edc4d87d1c5ecb42225902d |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
733824752318013c |
sbdp4_138.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 129162378e8ad29b5485a9c53feee4b7 |
8eda2752f413faeb338312ba814d9cc7 |
algebra |
gardam |
sat |
http://hdl.handle.net/10138/359079 |
no |
5057c7a882738f54 |
hantzsche_wendt_unit_93.cnf.xz |
main_2022,main_2026,submissions_2022 |
| 12ac1c71ff0405cc150c2a2db6c4a255 |
67939dae2642ce8e5ae9fc59a8d7c742 |
exam-scheduling |
zheng |
unsat |
empty |
no |
7b10681094e8793f |
exam_75_65.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 12cd0c3196589ac8105653cbfe613fc6 |
812467ff995bb34b702762f38ce6032b |
hardware-verification |
marques-silva |
unsat |
empty |
no |
866257e1d513dd73 |
4pipe.cnf.xz |
main_2026 |
| 1397d1d4d8d831069a2cdf911321da07 |
831a3e5f5eb93a4ca5ac39ed29cfcb9a |
graph-coloring |
reeves |
unsat |
empty |
no |
674a9f140dd1ee2f |
adv_gc_n300_k10_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 147ae051ca727d5b2af87223b2299fbe |
78d24678f7be51d9f1082aef016ade3d |
boxfolding |
heule |
sat |
empty |
no |
22c7142333397368 |
1x1x13_1x3x6_pair_0_0_0_2_2_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 15456f0d13b26f0b4b21525ef7d0d711 |
c00ee14b5d56a64003f84c8ac416ea21 |
clique-formulas |
oertel |
unsat |
http://hdl.handle.net/10138/584822 |
no |
98b98e084cb95c0e |
clique_n5_k10.sanitized.cnf.xz |
main_2026,submissions_2024 |
| 15e666a42158e3304fc3979de28a5e44 |
5832d6019891b4af8e79c97117e9ef92 |
graph-coloring |
reeves |
unsat |
empty |
no |
17109520c4462fd1 |
adv_gc_n200_k12_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 166e1e5a9f63fcf94ddae8533fa2a090 |
79d9710ca788de0238cabb0a348e0c66 |
cardinality-constraints |
wynn |
unsat |
empty |
no |
07fd74c85192de66 |
mp1-squ_any_s09x07_c27_abix_UNS.cnf.xz |
anni_2022,main_2017,main_2021,main_2026 |
| 1680176921bab3f01c4f7c33791c8c23 |
7145498183658b4da121605e0d18b2ec |
school-timetabling |
schreiber |
unknown |
empty |
no |
1f0563961d647180 |
schooltt-5-5-9-2-4-5-10-0.1-0.2-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 16ca57f2cdffd5b0260fc771017e1f04 |
4d5387c5d6c4b839a238696c69800b08 |
minimum-disagreement-parity |
bryant |
unknown |
http://hdl.handle.net/10138/359079 |
no |
ffb09d7954c44efe |
mdp-36-10-unsat.cnf.xz |
main_2024,main_2026,submissions_2022 |
| 16f8b291c8cdedb5ca7210fa0eeb34d9 |
0cc7ef4e465a2a973d8cdf4e3554704e |
graph-coloring |
anders |
unsat |
empty |
no |
3af6daf2a7d55e71 |
zeroin.i.3.29.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 1707c4c24e66b2cfe6c03955b638bebf |
4065616992b4a6583ebbf182c8c43907 |
xor-shifting |
zhenwei |
sat |
empty |
no |
89ae720e3d601d95 |
xorshift_r16_119.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 180e6d8b61fe6bab26126b78591e324e |
fdbcc286cb60a162b54145bba0a47cc3 |
baseball-lineup |
hickey |
sat |
http://hdl.handle.net/10138/318754 |
no |
f7a846c95bc1f0ce |
baseballcover11with22_and2positions.cnf.xz |
anni_2022,main_2020,main_2026 |
| 1890f49a43a94b97828528b68c32b78e |
9108c03884869c20344bca9cfeeb0784 |
fpga-routing |
aloul |
unsat |
empty |
no |
53148e09ac9a22b5 |
homer11.shuffled.cnf.xz |
anni_2022,industrial_2002,main_2025,main_2026 |
| 1a3bef9e03bab1ed4e9e34506d72a451 |
fa13c2a03e2de11cd662f91eed4345bf |
coloring |
devriendt |
unsat |
https://helda.helsinki.fi/bitstream/handle/10138/237063/sc2018_proceedings.pdf#page=65 |
no |
274ad90c459c427d |
le450_25b.col.25.cnf.xz |
anni_2022,main_2018,main_2026 |
| 1b9c308123cb2b48d1894fc6d1848f1e |
b3a4fe739824689763824109bba49601 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
ecf2443f45a82f36 |
cabp-M-bcsstk06.mtx.rnd-k33.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 1bb9fe12b4fb50e98903ee87a51d6472 |
fe59a4053ee685c47d184e96b2694b22 |
miter |
goldberg |
unsat |
empty |
no |
eab06ae35b6f567d |
goldb-heqc-k2mul.cnf.xz |
anni_2022,main_2020,main_2026 |
| 1c0fe2ac410f3942e374ea72ec005d76 |
3f0f5b7cc4baa9054178c8fcb64e2203 |
syndrome-decoding |
liang |
sat |
empty |
no |
6da5d2777d7affb1 |
SDP_120_17_1675.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 1eea3d913d346b900252d77fc0cb25c8 |
c0c913442dcbb100ed1fb39cf075590f |
minimal-disagreement-parity |
simon |
sat |
empty |
no |
414c4f7244f07d9f |
par32-4.shuffled.cnf.xz |
anni_2022,handmade_2002,main_2023,main_2026 |
| 1f81f7e009f501014cb23a8c2d41836f |
3ec02a4d537f8354d1cfd79b2a0172b5 |
diagnosis |
anbulagan |
sat |
empty |
no |
ac38d89f66b81ebd |
ACG-20-10p1.cnf.xz,g2-ACG-20-10p1.cnf.xz |
anni_2022,application_2009,application_2012,application_2014,main_2010,main_2015,main_2017,main_2026,parallel_2015 |
| 1fac905143027e3bf0932c09f427aa15 |
b514e8eb30a5b3a280d0b58fc420d9b1 |
graph-coloring |
reeves |
unsat |
empty |
no |
9b4c6d55b06965a1 |
adv_gc_n100_k10_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 1fb646d2657b6dd5f0106dbec9fd6c27 |
fd1372c980617f47f7a258f8f7a57c07 |
chnl |
oertel |
unsat |
empty |
no |
3965e539d33bd6d4 |
chnl-040x041.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2027301e88cb029e4b47b747da8a180a |
13f792c997de5a8667e262dfd79279a5 |
chnl |
oertel |
unsat |
empty |
no |
f767f8deb6bc3a9d |
chnl-050x051.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 20ae1404784ed226a1e3e4c9b2d61a41 |
23d20f39cc0c681d99783cc8dab84f79 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
30df29bdd115fb64 |
bwoadm_28_5.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 211b0708454f7901054f5f92f525972e |
e60a2573220bec2dfe525bf616a279db |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
8066d1463c0c29a8 |
sbdp4_65.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 218f0eccbff400e06c9736bd759c1d3a |
73bea510a4b740705d9aa9cc1d808164 |
argumentation |
ding |
sat |
empty |
no |
1d9057de10084db9 |
scc_9630_26_0.3_0.1_17.af_76.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 22465e251284b8f3e48bf9a06a94855c |
b5ffb4c06038262c25d8f120c9ab6450 |
allowable-seqence |
heule |
sat |
empty |
no |
833a571bab367a3d |
as-p81-l27-o6-rot-568.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 22c8d6aa86d51e15ef5ab37479eda22b |
b67f5c82d57605a83da4a5e1fa6d1da9 |
ordering-principle-xor |
oertel |
unsat |
http://hdl.handle.net/10138/359079 |
no |
710931f17428cf9f |
xor_op_n40_d3.cnf.xz |
main_2025,main_2026,submissions_2022 |
| 231f3a169120d3cda9f8feea88a20d85 |
a402c5255ee808050afc8d1ddc279181 |
xor-shifting |
zhenwei |
sat |
empty |
no |
612e34b764ee2775 |
xorshift_r14_42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 23daec2c71ce3c1e346e6042f3dc42eb |
b68b3e649de688a06028424f7a1558ce |
minimum-disagreement-parity |
bryant |
unsat |
http://hdl.handle.net/10138/359079 |
no |
255e953585c8ee56 |
mdp-32-14-unsat.cnf.xz |
main_2024,main_2026,submissions_2022 |
| 247e42e46495f1c4b8707e497af8c93e |
98052371e31f1fb5acc56b1440a815f7 |
linear-equations |
green |
sat |
empty |
no |
e22862b92fd5a2d0 |
16.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2563ea83d8508d635cc034d80014cd72 |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
70a2de7537571394 |
1x1x13_1x3x6_pair_2_1_1_4_2_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 262a226a47330987f038128579967405 |
9f42e4010b6535c7f2bb778270a84b49 |
unknown |
unknown |
unsat |
empty |
no |
1b35101486e98a12 |
ais8.cnf.mis-97.debugged.cnf.xz |
anni_2022,crafted_2012,main_2026 |
| 266e890b706cf336378bf148bbda1aff |
34fe7e62b48f5bea1d804cbb65dea9e1 |
exam-scheduling |
zheng |
unsat |
empty |
no |
5ce190758ea7cbc1 |
mexam_15_12_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 27495ba0093076d2e39a9b218e521ee2 |
67de32ac2713e897f494c0d409c1bcc7 |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
b6722d547004b7f7 |
sbdp4_61_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 276c46723eeb15ec37be224fbbd67574 |
13b0cc3b05e82fff232dd316a8c9eee1 |
cryptography |
gocht |
sat |
http://hdl.handle.net/10138/333647 |
no |
3977c642f475785f |
sha1__zeroOut_18__freeIn_22__seed_0.cnf.xz |
main_2026 |
| 284dec9d0d0404c8b80d8bd8064e4c68 |
972b001ebb3553a57cc80bf6e85824b1 |
quasigroup-completion |
heule |
unsat |
empty |
no |
16b9aeec13ad4e33 |
gensys-ukn004.shuffled-as.sat05-3844.cnf.xz |
anni_2022,crafted_2005,crafted_2011,crafted_2012,main_2026,portfolio_2012 |
| 28dcc4119e1bbb5fbd3fdd8f4140f28d |
a92d74c02e8541a3ee3badaf3a2a50a8 |
lights-out |
biere |
sat |
empty |
no |
34471efb31944a96 |
lightsout_sat_25_unbounded_totalizer_planted150_3_sat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 29a27e97790bda6c34808f631dd0418e |
69e335c257554ae9934e1e344918fee5 |
linvrinv |
unknown |
unsat |
empty |
no |
70258e61db124b10 |
linvrinv5.shuffled-as.sat05-564.cnf.xz |
crafted_2005,main_2026 |
| 2a38c5d48846ee1c35c4c40938082a16 |
4ed5a0975197231b68afd8f35bc68739 |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
753ff97e5c3113c7 |
sbdp4_138_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2ae678a4f0b8097615160a440efbe08e |
821a7f1681175c606de88a91a95f6287 |
allowable-seqence |
heule |
sat |
empty |
no |
d8880b654600cef0 |
as-p111-l36-o3-rot-II-5680-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2b35377a7b95f24449a3b607b61fff05 |
4a481d3cade5aee896799f4695d0de53 |
agile |
unknown |
sat |
empty |
no |
5b74fa5533c876ba |
bench_1277.smt2.cnf.xz,bench_1278.smt2.cnf.xz |
agile_2016,agile_2017,main_2026 |
| 2b7e863462991fd008f9898eca63ebf4 |
abfec0d10bf833bd1cfb73c418224d10 |
school-timetabling |
tchinda |
sat |
http://hdl.handle.net/10138/563824 |
no |
f05029efe4b187b5 |
SC23_Timetable_C_481_E_50_Cl_32_D_6_T_50.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 2b8cac8e1f5cad04696004e7fbf5cf2e |
6e78cae496b8b2a2617427678ceac72c |
ntil |
heule |
sat |
empty |
no |
144ef4485146b891 |
ntil-90d-34.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2bb63853a9b8b9b9327a142210a9f437 |
08732fe4c8e06f11625c5497cd14d0b4 |
argumentation |
ding |
sat |
empty |
no |
f013056e334839a5 |
Medium-result_b30.af_61.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2bbc3327d89b59591b89b5d5a486f037 |
f928f2f5dd7345cbbc849f00e24e8add |
cryptography |
nossum |
sat |
empty |
no |
45fe5f972b0581c0 |
001.cnf.xz |
anni_2022,application_2013,main_2026 |
| 2c4491c50d4df86e7c1838083cedc703 |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
0938821b2790966a |
1x1x14_1x2x9_pair_4_3_0_2_3_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2c458ef30d7b670f143d6c6e175e3ee9 |
c6fbfc5b5401a93bcbdddc903eac7a86 |
oddball-weighing |
mihal |
sat |
empty |
no |
aef174b833627715 |
oddball_70_5_tto_zp.normalised.cnf.xz |
main_2026,submissions_2025 |
| 2ca47af4ab7a817725138b8b66e9af7f |
517fbcb285be0df1fd1fbac53f0cfa74 |
stable-semantics |
hangjiang |
sat |
empty |
no |
a3eb0f8c45c44c4c |
st_540_25_12_12_9.af.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2d261a19d2754d92da3ddff04fda23c8 |
35e1b5a3ec2388d3f7d775da80097577 |
ntil |
heule |
sat |
empty |
no |
6c9bff16e436df2c |
ntil-90d-44.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2d89fda1bd6a761ca5e2f4bb89202681 |
7376c5f917587c7fd53b46c116a776a4 |
linear-equations |
green |
sat |
empty |
no |
847636de1bcdebf8 |
2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 2fcd8533eba981967292f1b6e41f7433 |
688dc5a2bf6c490d99504775299fcdcb |
cryptography-simon |
yuhangqian |
sat |
http://hdl.handle.net/10138/584822 |
no |
5aa75bcee5fb68cc |
simon-r20-0.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| 3005623c4df6f5056a41a26d0f173e70 |
14e4a99fa77fc8f662da2ff2e865dd37 |
influence-maximization |
kochemazov |
unsat |
http://hdl.handle.net/10138/318754 |
no |
0bb766ac9414f95e |
DLTM_twitter634_77_13.cnf.xz |
main_2026 |
| 306a29e966fa6293d407bc7ebbc3ecb1 |
44b4f194861b7bb2adc716da3b8c8bb5 |
graph-coloring |
anders |
unsat |
empty |
no |
d9dbf8fc50afbbe8 |
lattice-25.24.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 30c6fa5c4f5910029b782b712844c93a |
4536086f362a3d11e319339229b2c04e |
linear-equations |
green |
sat |
empty |
no |
0f086e84cc6da5f6 |
6.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 30e8b47741a4104c01eeea1d00bbce9e |
921bbeaa02f464d97f77f937eb2c0490 |
cryptography-cbmc |
post |
unsat |
empty |
no |
80d28a9b0d9bab4e |
aes_equiv_encry_3_rounds.debugged.cnf.xz |
anni_2022,application_2012,crypto_2021,main_2026 |
| 31fa00368fc99b15c33c04eb6b257deb |
d9fdb4c3b7312c7d498b094e3f3c2d11 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
fd5f98568e332f2c |
cabp-P-can__445.mtx.rnd-k96.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 324b2441c6f1fa9d5f3cf3a4c8447fc7 |
2fb3a24ada63299c739b89f44d0c5a5f |
scheduling |
djamegni |
unknown |
http://hdl.handle.net/10138/333647 |
no |
ef6432943cd5c40b |
SC21_Timetable_C_512_E_66_Cl_34_S_35.cnf.xz |
anni_2022,main_2021,main_2026 |
| 32e344a5ab3af245f982678d2b751c6d |
69cb2e5bb0293f36d053bbfa3695beb5 |
lights-out |
biere |
unsat |
empty |
no |
3128705fa5c5b0c5 |
lightsout_sat_24_unbounded_totalizer_corner_0_unsat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3367ba4c01fe07b385980a14211f250e |
d483f18414d40125bbaa4a3cc226df43 |
circuit-minimization |
unknown |
unknown |
empty |
no |
47e922eeaa37e8f1 |
shuffling-2-s158913847-of-bench-sat04-306.used-as.sat04-610.cnf.xz |
industrial_2004,main_2026 |
| 337ee3de87f824f99508e65faa6e1a0b |
72e71424b05bcc60138f61cd1932111c |
social-golfer |
zhou |
unsat |
empty |
no |
72018c50c15678a7 |
SocialGolfers-6-6-7-cp_c18.cnf.xz |
anni_2022,main_2019,main_2026 |
| 33c8aca6a52d10e040da959439834d6a |
fc957fe13fbf6c41f14be4859539d455 |
syndrome-decoding |
liang |
sat |
empty |
no |
a15b31ab4aae9f51 |
SDP_96_14_3612.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 34360a677fc854189c982294853e6891 |
cc40952b089bb524a39ad6592ee0a348 |
argumentation |
ding |
sat |
empty |
no |
1444fc1dc6ba3ab8 |
Large-result_b23.af_303.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3598c10125496ad7218852effc5c711f |
491c13a5a2ad6964fa4febd115064bfb |
subgraph-isomorphism |
anton |
unsat |
empty |
no |
ab66be4b7dd1d3c7 |
SGI_30_70_22_70_7-dir.shuffled-as.sat03-154.cnf.xz |
anni_2022,crafted_2011,handmade_2003,main_2026 |
| 35e0b5a19c88961d98dd806e805759f4 |
bc1cffec0b3f0d83d8a460f3ad192a2c |
count |
oertel |
unsat |
empty |
no |
aeed04658ca4bdf1 |
count_p2_M33.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 365a02a7d781d655bb2a64d2273a2d0c |
e160bf83a39938d5c0dafaaa3e00f35c |
argumentation |
ding |
sat |
empty |
no |
5713543802b962a1 |
Medium-result_b10.af_252.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 372021735d9e46002b862aa2a038a818 |
0c78aa3a8684090b0746df11432e024a |
scheduling |
shuolinli |
unsat |
http://hdl.handle.net/10138/359079 |
no |
30aa43cd484eb2b8 |
j3045_4_rggt_bm1.cnf.xz |
main_2022,main_2026,submissions_2022 |
| 3732b6ac50b1c3f28d72247de89b00e8 |
5db3dfdf07a724b8ee864909b6220e45 |
allowable-seqence |
heule |
sat |
empty |
no |
91e1c759691122f9 |
as-p123-l39-o0-rot-II-4680-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 37c88155822f1934a190dd6f4614f0ce |
4f9732fdad89fe4e84f62860d71f0232 |
scheduling |
stojadinovic |
unsat |
http://hdl.handle.net/10138/135571 |
no |
328b49f9a9ff6bc1 |
atco_enc1_opt2_20_12.cnf.xz |
anni_2022,application_2014,main_2015,main_2026,parallel_2015 |
| 37fa67bd34cc613f3fc6954cdee943c1 |
f89384fe1c7055d17554ed7bc9b0a651 |
syndrome-decoding |
liang |
sat |
empty |
no |
d13f0339ac450d54 |
SDP_106_15_2616.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3a8409393cc1ebae1444a079d216f221 |
2664b6516017e664acedc8c6f8388680 |
xor-chain |
zhang-lintao |
unknown |
empty |
no |
d566fd2ba78885c0 |
x2_64.shuffled-as.sat03-1603.cnf.mis-125.debugged.cnf.xz |
anni_2022,crafted_2012,main_2026,portfolio_2012 |
| 3a9dfcbcb56689f1118fd7a2150c3c0c |
bdf02d9f740ded29bc6aacf4431e87b9 |
ntil |
heule |
sat |
empty |
no |
3e8cfc49a05689a7 |
ntil-90d-40.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3b0eeddcabf36da8642c5774ac67680c |
f310d787c265536f00725b5b4220d4a0 |
allowable-seqence |
heule |
sat |
empty |
no |
3cd87267273156d7 |
as-p153-l57-o0-rot-rfl-II-68-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3b560b9eafce79a4ac3c1062a9e72028 |
f2929f9ce963809129eb576f52c661a4 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
ba39b2518febbcf4 |
cabp-X-can__715.mtx.rnd-k108.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3b608084b3caae2e9517a2d58cdcd275 |
55565057ade507c94fa409d9549e7237 |
argumentation |
ding |
sat |
empty |
no |
b3c69b4c69bf1647 |
Medium-result_b9.af_268.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3c4ac805726d78a869ff8116ee3533db |
b790871bcb0871ff8106309d2fa9c858 |
fpga-routing |
aloul |
unsat |
empty |
no |
aeb2baa8d75ee179 |
homer18.shuffled.cnf.xz |
anni_2022,industrial_2002,main_2026 |
| 3c51a565526faa922fb298a2658440e9 |
ade47ac1340a53687975f91f4b4a9aaa |
hard-cep |
zhenwei |
unknown |
empty |
no |
a150108b807f12fc |
fastlec_cep_14_T27_58.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3e44926d72e94f5ceccbb69de24033b2 |
d421d623195e117ceb7053a93b762ea0 |
polynomial-multiplication |
maoluo |
unsat |
http://hdl.handle.net/10138/318754 |
no |
3105c0bec3864576 |
newpol23-4.cnf.xz |
main_2026 |
| 3e7d8073c795d263ed862db64cf9f0fb |
51271f381f477a54c69f5d51244f077a |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
25aba406a0a638c8 |
bdmbwm_28_94.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 3e912cd2a499b8f956246b866e2f9f64 |
9be2e12837568b1a6ccea12f71be0286 |
cryptography |
shaw |
unsat |
http://hdl.handle.net/10138/318754 |
no |
c4c54583de28320f |
grain-53-80-0s0-seed-125-4-init-35.cnf.xz |
anni_2022,main_2020,main_2026 |
| 3ed56242f55e3653dbceeb4a70221787 |
a99f576c45bc59f4d60ea72dd1546a18 |
rbsat |
huang |
sat |
empty |
no |
3ef93e464a451d40 |
rbsat-v945c61409gyes9-sc2009.cnf.xz |
anni_2022,main_2019,main_2024,main_2026 |
| 40ae60a61929b6bfa2ac99ab4b9a0f7e |
12de8773eb6341648fc7f15863a147fd |
grs-fp-comm |
fleury |
unsat |
http://hdl.handle.net/10138/563824 |
no |
cbba7ec58c43a991 |
grs-96-192.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 416e33a8463911546e4cd87d282a7e1e |
60f769e017aafbc0a8db95a51b29b83e |
unknown-cases |
xu |
sat |
empty |
no |
eb70d69237645fa5 |
case10.cnf.xz |
main_2025,main_2026,submissions_2025 |
| 425c81fc3af7f5124b6282583d80df11 |
d3b6fdba7756186e23dcd18c77899e04 |
minimum-disagreement-parity |
bryant |
unsat |
http://hdl.handle.net/10138/359079 |
no |
b35e416cf809ff27 |
mdp-32-12-unsat.cnf.xz |
main_2024,main_2026,submissions_2022 |
| 43c298c756cac6d547a0457c2da7e468 |
a402c5255ee808050afc8d1ddc279181 |
xor-shifting |
zhenwei |
sat |
empty |
no |
a1735dca1063d1c5 |
xorshift_r14_31.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 43d40ced32b5be08814ef24f97379654 |
4d7a87a0a1f44e6931f801667afdb6bc |
sudoku-php |
shiv |
unsat |
empty |
no |
565e17a68e59d2f2 |
php_sudoku_p15_h14.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 44196693d2cfdb787ba578eef4272f74 |
7a13fae39c084e22425797ce31f40ae9 |
argumentation |
ding |
sat |
empty |
no |
2d6377d0c59bcb4d |
crusti_g2io_350_0.5_255_12.af_290.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4430d3502b0b5e6f4ed473437519e609 |
cbfc5e4ffe927e4707393c2f0b6b4070 |
allowable-seqence |
heule |
sat |
empty |
no |
fba0a0ce552e9348 |
as-p123-l39-o0-rot-II-4682-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 44452f4bac1e77157bbc900c5cc0756d |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
d8323d610e69e4ab |
1x1x13_1x3x6_pair_4_1_0_2_3_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 44b7d2c8d08574002ac959e6d1ef30ae |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
d141cae465d90879 |
1x1x14_1x2x9_pair_4_2_0_2_3_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4551c996fc6f5fbe62b43076abb25077 |
3959c4989e919ab04838de80f42dc4fb |
knights-problem |
zhou |
sat |
empty |
no |
f03a0a0a24c5d036 |
knight_18.cnf.xz |
anni_2022,main_2019,main_2022,main_2026 |
| 45a09efb026036ff4b8d19024a7563a9 |
27fcefa47bb5e5e049d457b80197b445 |
fermat |
riveros |
sat |
http://hdl.handle.net/10138/318754 |
no |
4a206f7cce33b316 |
fermat-931960058139995587.cnf.xz |
anni_2022,main_2020,main_2024,main_2026 |
| 46dc5e955b1fb541678d0634389353ac |
b7ce7f67291526590a54f302877829f3 |
ntil |
heule |
sat |
empty |
no |
f2f7a9e8ea6f120c |
ntil-90d-45.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 47173e8ab499159d3aa301b0101fe170 |
eeaf977e80b048169b9927be7179a828 |
school-timetabling |
schreiber |
unsat |
empty |
no |
8f17ad231ee47a0c |
schooltt-5-3-9-2-4-5-10-0.1-0.1-seed3.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 48432767076e402d2accbf2da7260885 |
cac9c7bd69b4898f7c30a44241253983 |
school-timetabling |
schreiber |
unsat |
empty |
no |
b123ad5e8ecd6b38 |
schooltt-5-3-8-2-4-5-10-0.1-0.2-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 49644428681a87666a68fc9380dce072 |
957339e21f26085d24869312b8ff2c0c |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
8e358206a3690308 |
cabp-X-can__715.mtx.rnd-k116.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4989239fbeb6eb40fc0b664d9ba92636 |
c8cee7d38a7ffa9fc3bc26411e410cad |
cryptography-ascon |
manthey |
unsat |
http://hdl.handle.net/10138/563824 |
no |
2afc461964b12147 |
asconhashv12_opt64_H7_M2-K1zfAs8_m0_3_U5.c.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 4aab4f954196d3277d9ca7b17c52acca |
0117c6db21f7a6196a307dde4a00c168 |
clique-coloring |
anders |
unsat |
empty |
no |
78063bee8680f4bf |
clqcl_25_8_7.normalised.cnf.xz |
main_2026,submissions_2025 |
| 4ae685a11b5cecca76dc3d463481ce92 |
e7bba0e4c294f3a254c40634274cd140 |
hamiltonian |
sterten |
sat |
https://knighttours.createaforum.com/general-hamiltonian-cycles-problem/hard-randomized-small-hcp-benchmarks/ |
no |
4fbb5ff31d55c42c |
x9-10032.sat.sanitized.cnf.xz |
main_2026,submissions_2024 |
| 4d6bd7b2c674fb67b271127586914b74 |
6f21be6c8dc16f179f5f150472549d55 |
van-der-waerden |
gopalan |
sat |
empty |
no |
17f12ff134abebc5 |
vdw_4_8_n145.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4d84e818a5ab324dde37429dd2455551 |
0792e41ac953a94945f20ffecbbcc014 |
linear-equations |
green |
sat |
empty |
no |
6dd0801c092d978e |
4.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4de5b7b3c8bf44b2e8c549128bc936a3 |
d255bdfcea0389b3675eb055bb811a67 |
allowable-seqence |
heule |
sat |
empty |
no |
b602efaa6a718248 |
as-p141-l39-o0-rot-rfl-680-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4e0de894799790b06e8d6c3efd109ade |
16bce0660d1a8c17d4f921a7f76dca40 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
2a2c517a7e30d08e |
9.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 4e64ffc14db014d5591f40865376c32a |
b936cd9610d4b72152a10fa0f7b0ecba |
satcoin |
chung |
unsat |
http://hdl.handle.net/10138/563824 |
no |
824483140bebca3d |
satcoin-genesis-UNSAT-7200.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 4f09ef861ee74e50dc101765e1ce27fb |
5e36b8fae7229c5a5f385e356605e621 |
algorithm-equivalence-checking |
kochemazov |
unsat |
http://hdl.handle.net/10138/359079 |
no |
95eeaa41e42bc0f6 |
BubbleVsPancakeSort_6_7.cnf.xz |
main_2026,submissions_2022 |
| 510df610f94d5d57073a2c3b694dac4c |
f65ec2f13ed259793226bf98a393edb1 |
station-repacking |
newman |
sat |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
16cb4218437b7837 |
51-136961.cnf.xz |
main_2026 |
| 511f1794698a8620c18a7cc32cfc7776 |
379995ebf179e987b5e87f33f02bde81 |
linear-equations |
green |
sat |
empty |
no |
ae33b52e153c08a7 |
14.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 515511be3905018ae7e6eb7ba7064d72 |
636ef67d9be10928fb448a510896f411 |
syndrome-decoding |
liang |
sat |
empty |
no |
c351b0578df96c1f |
SDP_134_18_4334.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5220b0e01fb49440531004bebbafbc44 |
74d34a07ba0daaae862eee59e2696a71 |
software-verification |
aws |
unsat |
empty |
no |
d1abc325a2e33667 |
coreMQTT:MQTT_ProcessLoop.dimacs.cnf.xz |
main_2026 |
| 5314fd6ccb53b6f6af49a594ea68a273 |
4d7939235c15ac74f43934612a0dc86f |
equivalence-checking |
zhenwei |
unsat |
empty |
no |
c5f67baa4764e193 |
oski15a01b15s_opt.cnf.xz |
main_2025,main_2026,submissions_2025 |
| 53d23b2b464a5c041114eb1f00cc4b81 |
0f43a831b8fde3f505fce5ffbf9cfe7a |
sliding-puzzle |
kaiser |
sat |
http://hdl.handle.net/10138/333647 |
no |
b2a48143cf3a1199 |
puzzle32_sat.cnf.xz |
main_2026 |
| 53e8a231196dfdf1baebfa2f29646f14 |
d483f18414d40125bbaa4a3cc226df43 |
circuit-minimization |
unknown |
unknown |
empty |
no |
0f8e13b06b54da4f |
shuffling-2-s504782760-of-bench-sat04-312.used-as.sat04-604.cnf.xz |
industrial_2004,main_2026 |
| 543e67dd5abc272c37775b1b742a1d9a |
65ace48b840b177ef2a3ed5e2684c0d8 |
quasigroup-completion |
gomes |
sat |
empty |
no |
f68ca466b425c654 |
qwh.60.1728.shuffled-as.sat03-1659.cnf.xz |
anni_2022,handmade_2003,main_2024,main_2026 |
| 546a73eef02dda3719018050b09e9392 |
ec48a1ef34f8b94712bca6147aae8493 |
school-timetabling |
schreiber |
unsat |
empty |
no |
f374e0c47607b9ad |
schooltt-5-3-8-2-4-5-10-0.1-0.2-seed1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 553b056f2651fdc182ca74174aa8ea10 |
2d67d4cc62042bca675883dc964892bf |
ntil |
heule |
unknown |
empty |
no |
71162b4ad6b9510d |
ntil-90d-46.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5553fec254b32349e0e48c7ee1e2d6c7 |
ff52693dff4907dd13fbde68d2b12616 |
cryptography-cbmc |
post |
unsat |
empty |
no |
3dfafea07d858db8 |
post-cbmc-aes-ee-r2.cnf.xz |
anni_2022,application_2012,main_2008,main_2020,main_2026 |
| 57f6bbfc8be5a981322fe9991209aa33 |
f88a80b829037c9442c187d131a68a80 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
7de1171d50a4b70a |
3.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 58eaf62034046ed4fc52562869569b44 |
0486c5f42a799df77d29b636fee0c8f5 |
count |
oertel |
unsat |
empty |
no |
e496372badd8cd51 |
count_p2_M41.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 59b585a33d30e6b7a476ed52a3f0384d |
563a7e271ed88e7dfb3207cb7cccb311 |
cril-misc |
frioux |
unsat |
empty |
no |
427a24fe3ed288a2 |
T92.2.0.cnf.xz |
anni_2022,main_2018,main_2026 |
| 5ab5ac8d66c7e375037f12a536baf721 |
52823552bd8e36627400b398a6467d7b |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
b030d9d23c8d41f6 |
sbdp4_136_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5babccd4bf9b270acf0568bba32313bd |
17925bac5d30619bc79f4a52391cd06b |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
2149ca5979656414 |
8.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5cae5c0629ce1c724746af890410cfc1 |
9d4e366d56e73d063fffbf25a4a51374 |
ensemble-computation |
jarvisalo |
sat |
empty |
no |
563dc0aa22a9f75b |
jkkk-one-one-11-38-sat.cnf.xz |
anni_2022,crafted_2012,main_2026 |
| 5ce7d137442bd97a321a883c425e4634 |
80684f3c52bb3fb17c86b2339e6becb9 |
station-repacking |
newman |
sat |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
ac55114439fb477f |
56-126575.cnf.xz |
main_2026 |
| 5d02aa18eac7304c705577f1cce07784 |
95580587ae5c6ec821b681caf58b8a9a |
allowable-seqence |
heule |
sat |
empty |
no |
4ab95354896fec48 |
as-p41-l15-o10-567.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5d06225b27017e9a703f10cb577cf3bf |
571bc2ace3598ac9d9028f19dc861cfe |
clique-coloring |
anders |
unsat |
empty |
no |
458833a5597f1ef3 |
clqcl_25_7_6.normalised.cnf.xz |
main_2026,submissions_2025 |
| 5d8b47745dba3fe50f9c8712be389cd5 |
ba9ffae572316eb5d3c4f2732055eb0b |
exam-scheduling |
zheng |
unsat |
empty |
no |
c99a0f201e83b44d |
mexam_25_20_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5de866bc7ff4dfde3cd682b5aca75894 |
6e1d22cd8be0a5a98d62624e3583d479 |
stable-semantics |
hangjiang |
sat |
empty |
no |
44be8be47a9aa6ef |
n320p5q2_n.af_239.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5e1f1759de9bf931a8e26dbe7dd5b212 |
3dc0647cdddab3a44231096854b489c0 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
bd91d017befb8c99 |
cabp-V-nos6.mtx.rnd-k290.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5ee05ef0bcb42cb12bd698978c05178c |
6a06ad45b6adc3c0efda2a159488272e |
sgen-balanced |
spence |
unsat |
https://helda.helsinki.fi/bitstream/handle/10138/224324/sc2017-proceedings.pdf#page=53 |
no |
8c166d0f42682ee2 |
mp1-bsat201-707.cnf.xz |
main_2021,main_2026 |
| 5f65b4cceeb01c56e037df144309b29e |
5f73eb6d533b2c1a83afbccacab8c099 |
subgraph-isomorphism |
anton |
unsat |
empty |
no |
67ceae8511d5921c |
SGI_30_70_21_70_7-log.shuffled-as.sat03-153.cnf.xz |
anni_2022,handmade_2003,main_2026 |
| 5f729f069a233fa88dfb470bbee7c924 |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
4af9e2ccdb72630d |
1x1x14_1x2x9_pair_2_4_0_2_2_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5f81a94799858590a2bc96db917bf894 |
93db285c526960a82849521e11e8f354 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
0caff19ad12663b3 |
bdobwm_28_54.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5f9d0127b390a4686171311d38f3fbf8 |
ab9a7023224423d9b2244df4b99c3de7 |
cyclic-anti-bandwidth |
hieu |
unsat |
empty |
no |
52b431550d4aaf45 |
cabp-M-bcsstk06.mtx.rnd-k37.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5faba478cb08194407b5ec957ab08599 |
31b93a9a2959b054ac5ff9faf61f75ef |
school-timetabling |
schreiber |
sat |
empty |
no |
062e9ccc46b00bf3 |
schooltt-5-7-11-2-4-1.4-2.6-0.8-0.9-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 5fb5e437292532efe687ac6f74a9cb76 |
942d2ac8d87a2e16f638a557793c34d8 |
syndrome-decoding |
liang |
sat |
empty |
no |
0a06389f430e2e4b |
SDP_126_17_1585.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 61fee64c8fc7f05b97a2bc14c0c2bf41 |
f4d9381f9b6488dfaca6edc250777b7c |
minimal-disagreement-parity |
simon |
sat |
empty |
no |
b53106b54c160c73 |
par32-4-c.shuffled.cnf.xz |
anni_2022,handmade_2002,main_2026 |
| 62060247cd0ad566a828c30571c2c774 |
00ea72f6ff8abf2e2ad17eb0daba12c5 |
philips |
heule |
unsat |
empty |
no |
ff5e13286c4914c4 |
marijn-philips.cnf.xz |
anni_2022,application_2012,main_2008,main_2026 |
| 626c368587dd880086afc7b3fa1e6f27 |
9bb4cae2d318c9f4b2bf651a591b60a8 |
sorting-networks |
ehlers |
sat |
empty |
no |
40c4d6e1faef3b06 |
snw_16_9_CCSpre.cnf.xz |
anni_2022,application_2016,main_2026 |
| 62eae28dcf3170b1547fb5db73e6a295 |
85c99b80788240d44c38549710ec8b31 |
argumentation |
wallner |
sat |
http://hdl.handle.net/10138/135571 |
no |
aa3c37e5c104e570 |
stable-400-0.1-7-9876543214007.cnf.xz |
application_2014,main_2026 |
| 654241eda3e1283f4b139192d1db055a |
7431d583989b2c4e9a9376c639670e10 |
syndrome-decoding |
liang |
sat |
empty |
no |
e9734af81292ef7f |
SDP_140_19_8786.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 65bf849f3e86ab275e339934f4d140a0 |
8579698e58716119bb2839dd150ce8d9 |
graph-coloring |
anders |
unsat |
empty |
no |
a8654b267b56591e |
DSC125.9.30.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 65ee6b49612eccb7d213e4d950f23677 |
5a89b5b179af07e58c947ef0838c279a |
lights-out |
biere |
sat |
empty |
no |
304a88ad9b742a0e |
lightsout_sat_22_unbounded_direct_planted150_4_sat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 66204949278cdd9d81e102eace6d4669 |
571360c0c9e3fa70cacdae64a0987b32 |
van-der-waerden |
gopalan |
unsat |
empty |
no |
b704c56f528cc93f |
vdw_4_7_n109.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 667341ee8c1dea3db613db317e2b2c33 |
99cbe22e989799e7ec8d1ac4c28f2334 |
lights-out |
biere |
unsat |
empty |
no |
cae58d0dc48ffbb4 |
lightsout_sat_23_unbounded_totalizer_corner_0_unsat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 67133027ab55906e3b757148ca7011dd |
038001e3b86528d72026df8fbd30e3ae |
sorting-networks |
ehlers |
sat |
empty |
no |
18fb947ae4d83da9 |
snw_16_9_Encpre.cnf.xz |
anni_2022,application_2016,main_2021,main_2026 |
| 6793abe982f9d5f9646f6657e13ecc39 |
173071592d0ff5f4f95fb8e385b8d030 |
station-repacking |
newman |
sat |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
453d3ec2a7b8747d |
55-140792.cnf.xz |
main_2026 |
| 68ef4b1ed6a28c75defea64bb7d53e06 |
e6d03f1a28198f3c12f59a8d32b9281e |
van-der-waerden |
gopalan |
sat |
empty |
no |
b6ae6503da1d2a4a |
vdwb_k6_n350.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 6ad453d6174581d982c4e75e37a38d79 |
053b293b422802942f08e1bd3ac4bc0f |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
99a2a057382504ff |
dobdm_14_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 6add7e416c1126607afeb2666af330ac |
559913637ea30a53c2da965d1002ca17 |
quantum-kochen-specker |
zhengyu |
unsat |
http://hdl.handle.net/10138/584822 |
no |
f963acc392b13fd6 |
constraints_16_0.5_1.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| 6cd46641ebd4c840b8f116d14ca17dfd |
c53616bee41203a2eb112e1f462baf79 |
stable-semantics |
hangjiang |
sat |
empty |
no |
92dd3f580f68917e |
sembuster_7500.af_74.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 6cfd9ef85d9f6e62dcbb9a4fd9334c90 |
8ff7b466cd8ed01fef2f4692e58cdb09 |
greentao |
kullmann |
unknown |
empty |
no |
8293e6f138112338 |
GreenTao_2-4-5_4231.cnf.xz |
anni_2022,crafted_2011,main_2026 |
| 6d815089fb4095208754622b4c44a8f7 |
a795e60f90956f3e335ae5c9c1f025f9 |
multiplier-circuits |
shunyang |
sat |
http://hdl.handle.net/10138/359079 |
no |
6f5dcd0f21fccf8f |
Carry_Bits_Fast_12.cnf.cnf.xz |
main_2022,main_2026,submissions_2022 |
| 6db4b3f59a1e530ca5309d8a7544f5c3 |
ff5d46f6b62cfe05ad570498442e7fc8 |
coloring |
unknown |
unknown |
empty |
no |
963cc6cd20a9f12f |
color-19-4.shuffled-as.sat05-444.cnf.xz |
anni_2022,crafted_2005,main_2026 |
| 6ddda96839bb24cd7389d5556d3ab16d |
da0ec00ada0ef0922275597c14afcdae |
graph-coloring |
anders |
unsat |
empty |
no |
35f6affa21da215e |
inithx.i.2.30.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 6e297bdb1c3f957f6333c37804805ecb |
ae07736d6d22e5410a0c24230c9e9f27 |
cellular-automata |
chowdhury |
unsat |
http://hdl.handle.net/10138/333647 |
no |
391e783fe80075f4 |
spg_200_301.cnf.xz |
anni_2022,main_2021,main_2026 |
| 6e8dba16e06c793a2daca1fa440eeb4f |
a928875430597c60b6a6289eea3d6ce2 |
polynomial-multiplication |
maoluo |
unsat |
http://hdl.handle.net/10138/318754 |
no |
08bb6f3d5150275f |
newpol32-4.cnf.xz |
main_2026 |
| 6f1b15ebd0ac13c05fb052e5b0453f64 |
46cfc556eaf7019e07f78ba7fcdc9d81 |
allowable-seqence |
heule |
sat |
empty |
no |
cdbf960382ea0003 |
as-p93-l27-o6-rot-rfl-5682-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 71849248b47db583f56e77f55f31e525 |
66678e316f5b32314723bd4acfc95324 |
exam-scheduling |
zheng |
unsat |
empty |
no |
013119c5d646fe56 |
exam_85_70.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 727ebce936c010888c7f71f00885e643 |
23b65cfedb76d24959c0b20e20c2d609 |
count |
oertel |
unsat |
empty |
no |
3b6d743f4156e8e8 |
count_p2_M25.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7372171e2e794a98cda6540676608f32 |
c21d925b22d387aec63de3e53ceda850 |
graph-coloring |
anders |
unsat |
empty |
no |
bd3b483c08576a1c |
DSC125.9.25.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 744238c5aadea40f8e05db49429da576 |
c21c59012b295ebe56cfe9e7e9abed6d |
linear-equations |
green |
sat |
empty |
no |
af8bd3a15dfc186c |
10.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 74931e82fd208ed949fa44bccd80df6b |
7f1304a2bd21fbf630626ee9ab1d96dd |
subsumptiontest |
nuttall |
sat |
http://hdl.handle.net/10138/563824 |
no |
51b59b9e3e0af45f |
DivS_862_11.cnf.sanitized.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 75429ff7acb5acb597abe01aa745c2a6 |
1209d58d3deffe4a796788b0571ddce7 |
random-graph-xorsat |
jarvisalo |
sat |
https://www.cs.helsinki.fi/u/mjarvisa/papers/hjkn.sat05benchmarks.pdf |
no |
e084fb10de0558a8 |
mod2-rand3bip-sat-250-3.shuffled-as.sat05-2220.cnf.xz |
anni_2022,crafted_2005,main_2026 |
| 757d64688ac60cba697a980dfbbf5075 |
98f159bafbadf0333dd72091f380e14b |
chnl |
oertel |
unsat |
empty |
no |
cbbd70fa135409a3 |
chnl-030x091.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 75b23436a531bbc4004f43009cb4546e |
c0b72d7f632e51667580fdbc3a5685ef |
ntil |
heule |
sat |
empty |
no |
b4fc813a38d5e4a0 |
ntil-90d-43.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 776ff89b72b0f6290d69af6f95e13182 |
58f0e01dd5f43b079996266198aa38e3 |
allowable-seqence |
heule |
sat |
empty |
no |
4238094f3266240f |
as-p43-l16-o9-567.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 77bfac6b280653e63013f77d0991484e |
bd91596f0ce73adb3a6256cb02126d78 |
unknown-cases |
xu |
sat |
empty |
no |
5f41a879bf97e48f |
case19.normalised.cnf.xz |
main_2025,main_2026,submissions_2025 |
| 782b29d2d691fdc94e0ec5b899390e10 |
fb7f0bf23536e071364f83886740e061 |
van-der-waerden |
gopalan |
sat |
empty |
no |
b9adbf904176e2bb |
vdwb_k6_n300.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7a13ffe9546cc7dfabdedebb64700e8a |
9c5bda5c634221dca98714b01baa318a |
lam-discrete-geometry |
nejati |
unsat |
http://hdl.handle.net/10138/318754 |
no |
e607ce0b9e5d7f7c |
w19-20.0.cnf.xz |
main_2020,main_2026 |
| 7ac164a9d153f0a2d9bf54a98d429636 |
4ca2a96a9b5bfb835913996081acce93 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
2f3e4c6aeb6f8f47 |
bwoawm_28_5.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7b40e39148de4d5f8d9384d6937c287e |
40a2704744afc9a4b33a62af91be677b |
argumentation |
wallner |
sat |
http://hdl.handle.net/10138/135571 |
no |
a969da316dbf3dd1 |
stable-400-0.1-12-98765432140012.cnf.xz |
anni_2022,application_2014,main_2026 |
| 7b9620b5d7da55bda43595fe37867acd |
b41cf905d32a423ceb5fc0e2c13d9fbf |
exam-scheduling |
zheng |
unsat |
empty |
no |
416343e1a8329f3d |
exam_90_80.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7cbc3ce2052ba7c5b501f75af58ab3c4 |
3a681770e66def8c650901ce334426ee |
cryptography-simon |
yuhangqian |
sat |
http://hdl.handle.net/10138/584822 |
no |
3a4a69d1861a99e5 |
simon-r22-1.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| 7cd6b940be001c46c6294d7cac9aa610 |
18b98a7193ebbbdd574bf3e9da3b4f7a |
van-der-waerden |
gopalan |
unknown |
empty |
no |
99d6c1cb5f03ef23 |
vdw_4_8_n147.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7d311f620f4ebc4adf8f4079899750eb |
8418120db8ff49ef4f7be93bdb611ab7 |
hamiltonian |
sterten |
sat |
https://knighttours.createaforum.com/general-hamiltonian-cycles-problem/hard-randomized-small-hcp-benchmarks/ |
no |
ef3bb241c3495fc9 |
x9-11033.sat.sanitized.cnf.xz |
main_2026,submissions_2024 |
| 7db30d12cb06f0dc2f30abff80d96d6a |
e63edad418f8529781b05038a2728634 |
binary-tree-parity |
pakin |
sat |
http://hdl.handle.net/10138/584822 |
no |
07ada0346e6c153f |
two-trees-1023v.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| 7e21850936d6127540157afaaf912c02 |
938d531a64bfd2519d130063eaf3293d |
tseitin-formulas |
bevan |
unknown |
empty |
no |
e1891ed2d3877017 |
marg6x6.shuffled-as.sat03-1456.cnf.mis-119.debugged.cnf.xz |
anni_2022,crafted_2012,main_2026 |
| 7efc1b160fb755fb1e8b6bcc70bbeb90 |
f750164bb050fdc3a40fedd736abcf1c |
syndrome-decoding |
liang |
sat |
empty |
no |
54704feecd2194a4 |
SDP_132_18_9892.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7fa502dfce37c37c1cafd50b3fba263f |
d4b541b69fe8c161011b961fd16a67b4 |
syndrome-decoding |
liang |
sat |
empty |
no |
b8627cd9ffafc4a7 |
SDP_104_15_107.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 7fe153ced2c966dcdeb42b6714b4d6b7 |
5960d7b50bfc04523c0d2dfb15fefa58 |
sudoku |
zhenjiang |
unsat |
http://hdl.handle.net/10138/359079 |
no |
a85041c7ad55a93f |
sudoku-N30-11.cnf.xz |
main_2022,main_2026,submissions_2022 |
| 805a742eb8b4e0df3561ca8e0670670b |
8fe0e2540bdfc9d65eab2444e5e53944 |
fpga-routing |
aloul |
unsat |
empty |
no |
7d064196067609ae |
homer20.shuffled.cnf.xz |
anni_2022,industrial_2002,main_2026 |
| 808d66b11c602eb1d5728f3f8e90aaef |
fddb4aae094568cddfe2a5b98635a27b |
boxfolding |
heule |
sat |
empty |
no |
b7e3405417b5330a |
1x1x14_1x2x9_pair_2_0_0_2_1_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 80b163b706e0a16702173ec27f3d1331 |
a7930875f774fe9a16a30ae464920d62 |
lights-out |
biere |
unsat |
empty |
no |
d2dc9f9844b2746f |
lightsout_sat_24_unbounded_direct_corner_0_unsat.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 80bb5209e88def5643bf5593320b104f |
3b91dc9ca708e117277e838693625afa |
argumentation |
ding |
sat |
empty |
no |
2e8dcd288e9d783c |
Large-result_b24.af_2238.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8117a2ac08e1acf52f660663efe2a5ca |
7f8b8eeb26095b7f790838711b64271c |
hgen |
guanfeng |
sat |
http://hdl.handle.net/10138/318754 |
no |
ca5766ce380218bc |
170225812.cnf.xz |
main_2020,main_2026 |
| 81c36c1f55a6ee8e180f53f140ce05a3 |
49ca6ae03036b627b1c9c94884b54282 |
01-integer-programming |
riveros |
sat |
http://hdl.handle.net/10138/318754 |
no |
9af4196c92e76ac6 |
01-integer-programming-20-30-40.cnf.xz |
anni_2022,main_2020,main_2026 |
| 824cd6f379c23cc863e501e397092cb9 |
e5b9b59d83d217572d6e0fbc804113eb |
algorithm-equivalence-checking |
kochemazov |
unsat |
http://hdl.handle.net/10138/359079 |
no |
d43dc0e92c574f93 |
BubbleVsPancakeSort_7_7.cnf.xz |
main_2026,submissions_2022 |
| 826a01aaab9f98e8fb6d3fbbf349078b |
b9c305c7bb612aeb6b56a5ad9b8a65b9 |
graph-coloring |
reeves |
unsat |
empty |
no |
d01642a07e1fc7f7 |
adv_gc_n300_k13_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 82cad197a0b7919f1f51ec51f7267e6f |
db809b8856144ad46537dcabd5fdf8b4 |
tree-decomposition |
ehlers |
unsat |
empty |
no |
b45b3a7a8baa2906 |
ex095_8.cnf.xz |
anni_2022,main_2018,main_2021,main_2026 |
| 8390dca257561c53bf4eb6e158a2285f |
0ef93519e4586155e7517fd09beb9e9c |
crafted-cec |
klieber |
sat |
https://helda.helsinki.fi/bitstream/handle/10138/224324/sc2017-proceedings.pdf#page=39 |
no |
039203366b4be30e |
mp1-klieber2017s-0490-024-t12.cnf.xz |
anni_2022,main_2017,main_2021,main_2026 |
| 83ced7d9ee8058c52c9a68ded7fad0a5 |
994d3478e7f2b03bf78416e71fc0a919 |
coloring |
mayer |
sat |
empty |
no |
f41f510f79196042 |
p160_1.cnf.xz |
anni_2022,crafted_2013,main_2026 |
| 8456155de4cd22425ec479f75af089c2 |
5b25c244253994e61a993ecd02b34200 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
ca723cde5792c77c |
cabp-X-can__715.mtx.rnd-k118.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 860788f93fb766e83e00a29de84180e7 |
fffffc8c0459933e03177bb88f59b448 |
exam-scheduling |
zheng |
unsat |
empty |
no |
dc1d2b3882b9ee3e |
mexam_17_15_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 878bcc11e1e243680f7946bcf428f465 |
3e2965178f70ad2b517fdb2c1dde9c1d |
software-verification |
osama |
unsat |
http://hdl.handle.net/10138/359079 |
no |
c784ca29690cca84 |
linked_list_swap_contents_safety_unwind45.cnf.xz |
main_2024,main_2026,submissions_2022 |
| 87dbc3302b82c09e19c55059fb943191 |
0d7e2db3d33cafd6dfaee1255af2a38d |
ntil |
heule |
sat |
empty |
no |
fe3e99ec91c86055 |
ntil-90d-38.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8990b3506e948e87b005d103d1ce6eb8 |
f77f991217b124822d85afe645e522fb |
algorithm-equivalence-checking |
kochemazov |
unsat |
http://hdl.handle.net/10138/359079 |
no |
d4a7a72498c4d24c |
BubbleVsPancakeSort_8_5.cnf.xz |
main_2026,submissions_2022 |
| 8aa9ffb211d1cba850be2ee9d173b7e1 |
0b5e3d47d71066205ef0a4f73d84679a |
graph-coloring |
reeves |
unsat |
empty |
no |
8e6a5e45a031da31 |
adv_gc_n300_k12_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8caa9b4b72b5f1782fe4554980978cbc |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
63a3c7893a081b81 |
1x1x14_1x2x9_pair_4_1_0_2_1_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8d0d8518a438d93428257d9a38863c3c |
5cbdf73b5ab8879f8648542ae85c9af6 |
allowable-seqence |
heule |
sat |
empty |
no |
7114b0a7b0470612 |
as-p31-l12-o9-56.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8d2b018a5f8855b6ba1868a3ffff9d2f |
d10b5f00c4d53e01cd4e038278b362d6 |
xor-shifting |
zhenwei |
sat |
empty |
no |
7837206352861755 |
xorshift_r15_113.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8d2dfc50c1759dc11a6564d5c368c6df |
f35841761091182f1ed516452e08199b |
equivalence-chain-principle |
sambuss |
unsat |
http://hdl.handle.net/10138/584822 |
no |
6f21c2ce81c42ee2 |
FmlaImplyChain_3_7_8.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| 8da88a43b4ac226f614dd82d4519d8c6 |
b7a4f8577af6ab4e17014433446666f4 |
prime-factoring |
bebel |
sat |
empty |
no |
cf43a93db483c07a |
toughsat_factoring_inf.cnf.xz |
anni_2022,crafted_2013,crafted_2014,main_2026 |
| 8db998d5fd64f85a1847115208f73873 |
44bb97d3abd1c7adc37c3b841a1467c3 |
stable-semantics |
hangjiang |
sat |
empty |
no |
0f1d5c449b969f96 |
Medium-result_b14.af_285.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8e1cdc28bad48753110be5bd578cb934 |
44b8ee7913508ce1be460cb72ac8b946 |
linear-equations |
green |
sat |
empty |
no |
4b04ae94a11e1366 |
15.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8e5da99e8323af36e983a99b4df03b92 |
0f0845fc92df4bbe833d29cd75a2a43f |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
391f69c99b0dfc9f |
bwobdm_28_56.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 8f5bca645bd8738eb74c2e1dc284774a |
5cf082f0e7e0d0080edd31de794952a7 |
social-golfer |
lynce |
sat |
empty |
no |
69831bb4f53165de |
sgp_7-4-6.shuffled-as.sat05-2671.cnf.xz |
anni_2022,crafted_2005,main_2026 |
| 8fcde459f828e0df9672933e68fa1af2 |
9e82b29b8f0e0a433e19bba871b10f77 |
chnl |
oertel |
unsat |
empty |
no |
a979f3cd688fc5b5 |
chnl-020x061.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9078ea73ff67edf2b6dcd007c9696ca0 |
be4a6d8e6b11672eaf73e2c47fbbba07 |
linear-equations |
green |
sat |
empty |
no |
499db26edcf164f5 |
13.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 90937ed75ba0560158d8fe45f303868a |
30109d64a8286edba612f68877772300 |
polynomial-multiplication |
xiao |
unknown |
https://helda.helsinki.fi/bitstream/handle/10138/224324/sc2017-proceedings.pdf#page=43 |
no |
721256c2a34925a6 |
mp1-Nb7T08.cnf.xz |
anni_2022,main_2017,main_2026 |
| 91860f79f079fede859034c7d76a98a2 |
ae08e177fd49ae0bdbb0325f4e2bf83e |
station-repacking |
newman |
sat |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
2f9729ac5ada7d5d |
41-119494.cnf.xz |
main_2026 |
| 91e0db01b254eb78f6643328045bfeb9 |
af8730519d158c0818cc0147603182f1 |
stedman-triples |
johnson |
sat |
empty |
no |
206140e7d95180b7 |
sted5_0x1e3-20.cnf.xz |
anni_2022,main_2018,main_2021,main_2024,main_2026 |
| 920bbe559da4ea37fd636605316a791c |
9115895017e2394c2936e463d5cb88c1 |
set-covering |
zheng |
unsat |
http://hdl.handle.net/10138/359079 |
no |
9e1a541193a28e3d |
SCPC-500-19.cnf.xz |
main_2022,main_2026,submissions_2022 |
| 92b22042a950db2a9841f08d169d1bb5 |
3f91b02cee97480acd3966df52c449ca |
exam-scheduling |
zheng |
unsat |
empty |
no |
352417981fc5373c |
exam_90_70.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 932e2329dd1efeafe7151a0ebf3a343f |
3998cd7edb71831f59ebbca1dac1f336 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
58da24f22f0f4339 |
bdodo_28_6.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9376a4be372c14aa68235831712ff3f9 |
57422db25401ceb4dbe7b7e756a5de72 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
645874f6d29b5174 |
cabp-X-can__715.mtx.rnd-k102.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 93983a1211a506a87907c7e2ffa4e818 |
8693ab614b4ffc90e3b252acffca73d7 |
circuit-minimization |
unknown |
unknown |
empty |
no |
4a908cf3e50501aa |
shuffling-1-s1719683924-of-bench-sat04-310.used-as.sat04-467.cnf.xz |
industrial_2004,main_2026 |
| 9541d12f3e3d9201085c13f25145d2f7 |
6a372dccc4d9dc72febf88550b6f62de |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
52db730b60139d07 |
cabp-V-nos6.mtx.rnd-k275.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 958fd8bd1936e5bad8cbccae492edd81 |
a07eecc6baeb2a419e4ee3141eff8ef8 |
stable-semantics |
hangjiang |
unsat |
empty |
no |
4845ee484b72d24e |
crusti_g2io_200_0.1_127_14.af_151.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 95f346a183b890307596310fd33b4836 |
65531c7716cdae1f4abf4fb1e6faa0a0 |
prime-testing |
jingchao |
unknown |
http://hdl.handle.net/10138/333647 |
no |
e03675a09e0334ed |
quad_res_r30_m35.cnf.xz |
main_2026 |
| 965ca988015c9aee5a1a7b2136c1fe5d |
0eb0b5c05472f1f65752375b79e40ab9 |
register-allocation |
green |
unsat |
http://hdl.handle.net/10138/563824 |
no |
453fa425e2b912b4 |
os_fwalk_12.cnf.xz |
main_2023,main_2026,submissions_2023 |
| 97af3e49faef7cf67794928b6690b67c |
af0b2e5dddd75e47206325b956b4f640 |
stable-semantics |
hangjiang |
sat |
empty |
no |
157ab60a6e0d543d |
Medium-result_b29.af_78.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 981b0e855eed536df112bf2e4ff98807 |
a1f969f136ebd75c8c20baac049b0fb8 |
graph-coloring |
reeves |
unsat |
empty |
no |
bc9d9f06f48c60bd |
adv_gc_n50_k12_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 991aec61a2751602d6d7b3e838035610 |
5d7506dd21b74315a9b3c7c4c033af4d |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
3cd0735a37669eb9 |
bwodo_28_7.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 996bd6326ca560055b6fe916708dfdaa |
6ca3ce9432e729b7526387a511c4e072 |
van-der-waerden |
gopalan |
unsat |
empty |
no |
20f6b69d02c75a2a |
vdw_3_13_n160.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 997491c0cbc3e558a3e3266e2a142215 |
c4f382f6330fe2426f1a3e126ac4203a |
graph-coloring |
anders |
unsat |
empty |
no |
4513cf8e4859e49e |
mulsol.i.4.30.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9a4671d8bb658361162976c0f06cc47e |
a312bdeeeda695b620691e1fb1fcef79 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
789b7930c091ef40 |
10.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9a4837429c656a71283b8d5bb41c05a7 |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
77d31e5d23bf6c13 |
1x1x14_1x2x9_pair_2_4_0_3_2_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9aa85c5c114245c182ed6afbe3d8daed |
f2ca21f260eb2608a56d5d490a9d901a |
school-timetabling |
schreiber |
unsat |
empty |
no |
3beb25db98bf610b |
schooltt-5-3-8-2-4-5-10-0.1-0.2-seed4.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9ba8145e0d02318dea5507fc3ba03472 |
6af76d8c976897714234743f58070d36 |
graph-coloring |
anders |
unsat |
empty |
no |
a3c1627e6a6d8e68 |
latin_square_10.15.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9c5dd2eb0a40a150c686459a118c720a |
e89a031189d24c5125ab1adf707388e8 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
8c0b8a85f8fa0e7c |
1.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| 9d20bb1bd01838d70177ffd3aa284aeb |
1f6040b8ab9fb989624bead9f441f13e |
miter |
kojevnikov |
sat |
empty |
no |
85ffc3c189af7340 |
ak128modbtbg2msisc.cnf.xz,g2-ak128modbtbg2msisc.cnf.xz |
anni_2022,application_2016,main_2017,main_2026 |
| 9ef9243ff051b32795890fccd6c3f6b2 |
02c14303e87107af67407428a02119ba |
sum-of-3-cubes |
riveros |
sat |
http://hdl.handle.net/10138/333647 |
no |
311103f30d9b8cc0 |
sum_of_3_cubes_50_bits_91.cnf.xz |
anni_2022,main_2021,main_2026 |
| 9fbe200523c648000d71b2c739093aa2 |
052ea6c3af3dd331dfd7e12900ce58ac |
graph-coloring |
reeves |
unsat |
empty |
no |
9e6379e3c0fecbdd |
adv_gc_n100_k13_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a08c17f9a3888841cf7bbc75a807ff7e |
6d7563fa35c83fd98dbfc7acfce8140e |
xor-shifting |
zhenwei |
sat |
empty |
no |
2510f15a7b2b87c5 |
xorshift_r14_110.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a08d0fcc98fe0ce9c53b2fd0c69ccc4b |
fd4ac16b795ae1caaabbc05efe25a716 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
e7dbe9dd01efaddb |
bwmdm_28_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a110c13186ef5785df8da4bfa2ce9a6d |
bf8dffee13fc48c3d19c5f60769d4323 |
xor-shifting |
zhenwei |
sat |
empty |
no |
6fc2ab0244a626ac |
xorshift_r14_7.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a20f076f7fce54172e823c63ea7948f7 |
38ef03a985b3fa2bb54faf4d8b85e1b7 |
van-der-waerden |
gopalan |
unsat |
empty |
no |
351e4efb002966b7 |
vdwb_k5_n260.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a2fdd0935df1379c67cf1bb93ef2cfad |
5abbb340f6b74af70e9129afcf2f91de |
station-repacking |
newman |
unknown |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
d31e6857973cb61e |
54-138766.cnf.xz |
main_2026 |
| a42230be4432b010789b6f97b090343c |
549c52099d5ed1ab70699e613f5c3ddd |
algebra |
gardam |
sat |
http://hdl.handle.net/10138/359079 |
no |
6813ffe1df05c0ef |
soelberg_unit_223.cnf.xz |
main_2022,main_2026,submissions_2022 |
| a45aefde8bb26edb9634004146d0de89 |
40f2b44f777189df721d54479bbd0602 |
circuit-multiplier |
unknown |
sat |
http://hdl.handle.net/10138/333647 |
no |
a481cc61f96f5108 |
Circuit_multiplier36.cnf.xz |
main_2021,main_2026 |
| a4eec7a5fef59547129822f6b513d54c |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
4c2d394b576cfe94 |
1x1x13_1x3x6_pair_2_2_1_3_2_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a4f816482e853dfad9a685ac1459e66d |
94548121293edfc0356ee1e3a8fd557f |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
e9610092906a4d71 |
bwodm_28_5.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a5dc08b83ff806ac2c2c8cc23053fb07 |
aed85198b301f83c9f7b6f9ce8618c69 |
syndrome-decoding |
liang |
sat |
empty |
no |
7c39f83ca2b91a17 |
SDP_118_16_5515.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a60a138325ac9c88ab293ec0c801a95c |
d181f822dca43ea3d11435bfc9bcc49e |
xor-shifting |
zhenwei |
sat |
empty |
no |
56f70f8667282c84 |
xorshift_r15_191.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a78606fdfd6cf6ee8358bd35fa833be6 |
65622652c8c76c748f8c4c55ba569d53 |
allowable-seqence |
heule |
sat |
empty |
no |
cba0af3d1893be93 |
as-p61-l22-o8-II-568.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a789d0722f1aa0d44c5a38b374719c69 |
daca2d110bc8ab506aa7c4d2150ed1ea |
md5-equivalence-checking |
jianmin |
sat |
empty |
no |
e63e37af3d7402b0 |
13.normalised.cnf.xz |
main_2026,submissions_2025 |
| a7e5d03892a17e51e22b688f51cf0aab |
72d4f7851793f27bbf6d0b37de4abef3 |
exam-scheduling |
zheng |
unsat |
empty |
no |
e7a9b97676e19951 |
mexam_20_18_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a80a252b748882980d9a80ddea8c5cff |
9abaa6edce52db44f5b09790f71f15bf |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
aad5d7a7ced057db |
bdmdm_28_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a8dcaf436bda091dad9ca1ff58de7287 |
2cf5d2720b0dc32e74c1b86e579279bf |
cryptography-ascon |
manthey |
unsat |
http://hdl.handle.net/10138/563824 |
no |
78fc25f713bd7d79 |
asconhashv12_opt64_H10_M2-BPHqhzNzqi_m5_6_U14.c.cnf.xz |
main_2023,main_2026,submissions_2023 |
| a957fdb07df865bb4fd24a00ceb49fdb |
bc4a0c743ca2c01371faa1925206eaf7 |
cril-misc |
frioux |
unsat |
empty |
no |
12b5a26c2786e601 |
T90.2.0.cnf.xz |
anni_2022,main_2018,main_2026 |
| a95f0373ebf724f474fcc9ccd7197bd9 |
9750a8cf4a73503c65b0f3f6a91a47d0 |
chnl |
oertel |
unsat |
empty |
no |
4e5da1875cfe7b1f |
chnl-030x061.sanitized.cnf.xz |
main_2026,submissions_2026 |
| a9856534b6ca67123d58dd5fd9c9a1b2 |
90d54279660d9b7316eaa5ba9650d65c |
syndrome-decoding |
liang |
sat |
empty |
no |
49ce0a17c079cc48 |
SDP_98_14_7360.sanitized.cnf.xz |
main_2026,submissions_2026 |
| aa0eadb6c4935468fd6954e23a550504 |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
6f240a553a99d9fb |
1x1x13_1x3x6_pair_4_2_0_2_0_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| aa2e02360b19c83da68e39e39c530923 |
8861c09372b346d3bc6fb08b64bce28a |
cyclic-anti-bandwidth |
hieu |
unknown |
empty |
no |
b3b87b9e3f23475a |
cabp-V-nos6.mtx.rnd-k333.sanitized.cnf.xz |
main_2026,submissions_2026 |
| aa4e80476e6a6ea1034e303e6b2e46dc |
73b93ea37c4cc4c42f257d0a012fbf05 |
exam-scheduling |
zheng |
unsat |
empty |
no |
77b709acd4764ec6 |
exam_75_70.sanitized.cnf.xz |
main_2026,submissions_2026 |
| aa62e8cb5d38ac1b2d9eeeb8394eadeb |
3e621e149f038666a125e3b6d3ca8a40 |
allowable-seqence |
heule |
sat |
empty |
no |
feb895b9738b7904 |
as-p87-l30-o6-rot-II-5678-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ab17eed90e4da47767f72f518e3b4a26 |
8b6ec62643f2fda32ce1d689cc00df0a |
van-der-waerden |
gopalan |
sat |
empty |
no |
5843b2c8107ebbec |
vdwb_k6_n250.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ab2ab3a0651f0f35ba319ad976b1b6fd |
fbce861cceb88b6f1689ce73a3f31890 |
linear-equations |
green |
sat |
empty |
no |
7c33377dd501f733 |
1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ac3e3bb744e258282990aa4307c08cb8 |
99163d0678a32ddf33512a62c4204679 |
2d-strip-packing |
leberre |
unsat |
empty |
no |
e164ab59769a1392 |
E00X23.cnf.xz |
anni_2022,application_2011,application_2013,main_2021,main_2026 |
| ac6256657058fe65dc7ddaf773ab83bf |
f7f37d8760f4c7e2913f0d3c91544038 |
scheduling |
djamegni |
sat |
http://hdl.handle.net/10138/333647 |
no |
3679f3ea94051e3e |
SC21_Timetable_C_527_E_71_Cl_35_S_35.cnf.xz |
anni_2022,main_2021,main_2022,main_2026 |
| aca9f4faabeb57a57c678d55f5bbd2f4 |
9ca099dc99a1fa6e3e82511e3351cf57 |
linear-equations |
green |
sat |
empty |
no |
e32bf02301372e85 |
12.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ad2247443454da1fbd4543dd1fa5b57c |
e952049822cd3d321691636959c32a58 |
school-timetabling |
schreiber |
unsat |
empty |
no |
420ac228a62a122c |
schooltt-5-3-9-2-4-5-10-0.1-0.2-seed3.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ad5b80bb4d1b60bee12163df25846801 |
3240dc0af44fd68550c85cad9c4e89c6 |
xor-shifting |
zhenwei |
sat |
empty |
no |
a8431f6d32f58f9d |
xorshift_r15_104.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ad6bc2d583c43ff9ef00faad7e29a9c2 |
8d52f27ad0059b39b37ac8f962bd462f |
allowable-seqence |
heule |
sat |
empty |
no |
515060fe3332dadb |
as-p99-l33-o6-rot-rfl-568-i.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ae48df6541d190c096b1e5ba22d1b534 |
25e2198c4186fb31b2f4f7ce40005f80 |
2d-strip-packing |
leberre |
unsat |
empty |
no |
efbd6252f614b05d |
korf-17.cnf.xz |
anni_2022,application_2011,application_2012,application_2014,main_2026 |
| af8248aa34c4803bfc0add954cf2e620 |
8726b0f7845c0c3bba76a04947a5623d |
argumentation |
ding |
sat |
empty |
no |
90b6548256eff43e |
sembuster_4200.af_72.sanitized.cnf.xz |
main_2026,submissions_2026 |
| af9c2fb7046eb845f185c64cd9dd1006 |
6121661b149d4d54830e92f323719af4 |
cyclic-anti-bandwidth |
hieu |
unknown |
empty |
no |
8459a6166ddb24c7 |
cabp-T-dwt__592.mtx.rnd-k145.sanitized.cnf.xz |
main_2026,submissions_2026 |
| b0142b06940fb02e2b4ddb7a2101a3d6 |
1c5b3fda8fb679523e7e6a6b430d2969 |
count |
oertel |
unsat |
empty |
no |
3e5bfa82f6729b34 |
count_p2_M21.sanitized.cnf.xz |
main_2026,submissions_2026 |
| b023ea0eb9adbd9182c01d7e2d443289 |
e80f4e31dca38fe179f80052a7de05bd |
cardinality-constraints |
wynn |
unsat |
empty |
no |
e148f8577647a1bc |
mp1-tri_ali_s11_c35_bail_UNS.cnf.xz |
anni_2022,main_2017,main_2021,main_2026 |
| b0abaa97c4663edc2048d86de3e2b226 |
7ffd843031d891bc6b23318d3faf0789 |
school-timetabling |
schreiber |
unsat |
empty |
no |
262b79ba13d04d3c |
schooltt-5-3-9-2-4-5-10-0.1-0.2-seed4.sanitized.cnf.xz |
main_2026,submissions_2026 |
| b13ba48e09e575d6a628c02200ac23f7 |
173e8fb0487d887e0fa3abd0885dad55 |
graph-coloring |
reeves |
unsat |
empty |
no |
58776364007b1af9 |
adv_gc_n100_k14_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| b1c44904cf06682f973b60c8282f45e8 |
64680f55198eb1665e489e7a724a2ce5 |
cardinality-constraints |
wynn |
sat |
empty |
no |
45e6d40755d4ab80 |
mp1-squ_ali_s10x10_c39_bail_SAT.cnf.xz |
anni_2022,main_2017,main_2022,main_2026 |
| b2047f327e213b5f14adb8c75ee514fb |
bbb90e7859c413eddac06225169bd9a3 |
station-repacking |
newman |
sat |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
e0af5710f645bcad |
60-135969.cnf.xz |
main_2026 |
| b358bf7111086fd6d60b11c2f01465b8 |
293036bb1d36bec4c3ec1ff87c2c5dd5 |
automata-synchronization |
skvortsov |
sat |
empty |
no |
355ffa00f81a1005 |
crn_40_1521_s.cnf.xz |
anni_2022,crafted_2011,main_2026 |
| b3c587501567db72e6e66c6930cf15ed |
fc8d74caffe5088d711aabda9e926eae |
st-connectivity-principle |
sambuss |
unsat |
http://hdl.handle.net/10138/584822 |
no |
37888cd7474e6f35 |
StConn_7_128.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| b438fa464c20a19fdb7788a3f0016f32 |
06cffde9dcefe44821dfd181777e5066 |
tensors |
savicky |
sat |
empty |
no |
2efc2c0a5333d38c |
size_5_5_5_i116_r12.cnf.xz |
main_2019,main_2026 |
| b54b26f38d40a687b6277c49cf85de69 |
e6a2764df08edff7062bf37b323d768d |
baseball-lineup |
hickey |
sat |
http://hdl.handle.net/10138/318754 |
no |
7452a4ee0f4b01f2 |
baseballcover11with25_and6positions.cnf.xz |
main_2026 |
| b69132879ed9ea0c8af1bc1e478d6ec3 |
6b848a97e640aa2a90a8adc58112610d |
bitvector |
preiner |
unknown |
empty |
no |
a2d61a517e84ca64 |
128.smt2.cnf.xz |
main_2026 |
| b697738cefe9cb2dd62f24653a13b341 |
59a40e0430d31201c54fb70a03561dff |
erdos-discrepancy |
heule |
unknown |
http://hdl.handle.net/10138/135571 |
no |
aad708af96680627 |
EDP3-60000.cnf.xz |
anni_2022,crafted_2014,main_2026 |
| b6de3c794e223fe515682f52e5d81272 |
8c431807e70f0404e4c33670327c0f98 |
stable-semantics |
hangjiang |
unsat |
empty |
no |
e8d0fad8264021e6 |
ER_500_50_1.af.sanitized.cnf.xz |
main_2026,submissions_2026 |
| b76b9699c2deb74dd9b4a99a05179acd |
2b7962632ae3fc4a5eaef44a1a270aab |
cryptography |
soos |
unsat |
empty |
no |
143f5eb94eead552 |
hitag2-8-60-0-0xdcdbc8bf368ee73-37.cnf.xz |
anni_2022,application_2013,application_2014,main_2026 |
| b9a626da76f235aab854c6ef516b9240 |
3e4d3216d6dc20eb6a092e1157c05739 |
termination-analysis |
fuhs |
unknown |
empty |
no |
004e5cf6665a9a95 |
AProVE07-26-sc2007.cnf.xz |
anni_2022,main_2019,main_2026 |
| ba14be209c2fc064726025f017cef17a |
fa588a7d70d22e62883616ac6b17d918 |
school-timetabling |
schreiber |
sat |
empty |
no |
37eb873533ebe314 |
schooltt-5-7-12-2-4-1.4-2.6-0.8-0.9-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ba7732774961fdf7508a998a41bd5366 |
4271b0cc1edd28d3f4546d69c371f9ba |
graph-coloring |
faraja |
unsat |
empty |
no |
b0fe5f25f99ad7d4 |
factorize-1022117.sanitized.cnf.xz |
main_2026,submissions_2026 |
| bb8db7af8ede49391a66d4442d91c10b |
0a4569a1c03fb92e7844bc10220d524c |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
5a638fd2364bab01 |
7.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| bbcfd33f07cbf6fefa950d8254aa34ce |
74ee814b045253682c01c05b185ebd11 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
ce5c9c41ac58a855 |
5.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| bcdc894819cf050e57849fe84a1e8cc4 |
a2960b517b5f07d4fc783e07635e18ba |
chnl |
oertel |
unsat |
empty |
no |
66c7de224fb3967b |
chnl-020x101.sanitized.cnf.xz |
main_2026,submissions_2026 |
| bd0b055b890a9ace598a0c4aba40de30 |
b6f0b46d85aca7002427631e81f96b22 |
trigonometric-functions |
hiller |
unsat |
http://hdl.handle.net/10138/563824 |
no |
cf6d27000e5e4294 |
sat-bench-trig-bhaskara.cnf.xz |
main_2023,main_2026,submissions_2023 |
| bf8c8761003704e761ce36db6665f741 |
e6bd1066ed9fdb54e87ca1b66e436679 |
stable-semantics |
hangjiang |
unsat |
empty |
no |
342c953fcc39d165 |
scc_6087_19_0.3_0.1_20.af_130.sanitized.cnf.xz |
main_2026,submissions_2026 |
| bfc825d1eb0670fd90805c546fea5c6b |
10c3c770ca0e2bf8468089309538755c |
sorting-networks |
ehlers |
unsat |
empty |
no |
5d15757121038dcd |
snw_17_9_CCSpreOptEncpre.cnf.xz |
anni_2022,application_2016,main_2026 |
| c14f0c610d59a9d5e8cec328485b916f |
d2d7beae44aa75203d44a17be2d92c57 |
van-der-waerden |
gopalan |
unsat |
empty |
no |
5cf890deb070d158 |
vdw_3_13_n161.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c15b09b9a7ceff4d4c8fe705958f92ba |
05cf1e7df9e619f53115695f08173ab4 |
sorting-networks |
ehlers |
sat |
empty |
no |
86479989cc2ab142 |
snw_16_9_preOpt_pre.cnf.xz |
anni_2022,application_2016,main_2026 |
| c261941bfec8b89d75fee1a66a839169 |
f5bfafbbd309b4f08c7e453ad27436e0 |
gray_codes |
manthey |
unsat |
empty |
no |
1473ee83a8c23bc3 |
manthey_single-ordered-initialized-w48-b9.cnf.xz |
anni_2022,main_2015,main_2026,parallel_2015 |
| c300445f0f756c8f5d6571ebf0bb6edc |
d2a5066864d6d62866b41a641e44e31c |
cyclic-anti-bandwidth |
hieu |
unsat |
empty |
no |
93829b20207db111 |
cabp-M-bcsstk06.mtx.rnd-k36.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c3bc9b01e5f804723b74715508941bf2 |
3148538884c378ecb71201f51491f1f0 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
95f0c9bfdab2786f |
2.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c44762c4b177ac64fd0919f37de8382e |
dd9ef0fc91e8eccc3202fd2be97d0b1b |
exam-scheduling |
zheng |
unsat |
empty |
no |
742f95130ea9cb7b |
mexam_14_12_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c557ad9cb79983b9d429c219e3cecbb8 |
8c7e515a2c9ce1aabc78aa98fc1070ce |
stable-semantics |
hangjiang |
unsat |
empty |
no |
635cb0812e49ef66 |
scc_7216_12_0.5_0.2_11.af_463.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c615d49f357813514966186ab834be28 |
99ff70e54507d651a0f0570504002d54 |
cryptography |
shaw |
unknown |
http://hdl.handle.net/10138/318754 |
no |
eb74a7424426fbe1 |
preimage_80r_486m_160h_seed_306.cnf.xz |
crypto_2021,main_2026 |
| c62a1855a4db8ae0b4bd625455332a4c |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
7ca590ddff09ea63 |
1x1x14_1x2x9_pair_2_2_0_3_2_1.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c6487f6dfcc1438eccca1876a33d9a9c |
6ddd951c311231b1748bbd16cdb9c651 |
genurq |
ostrowski |
unknown |
empty |
no |
2a65fbd4b20bc728 |
genurq7Sat.shuffled-as.sat03-1513.cnf.mis-135.debugged.cnf.xz |
anni_2022,crafted_2012,main_2026 |
| c7449e5bc5ef75a69f8a454c13d371de |
eefe3ad7bd2ac28d7ad67b389b9f6ec4 |
multiplier-circuit-miters |
yalun |
unsat |
empty |
no |
8f1ec5319adbd08d |
bdoawm_28_4.sanitized.cnf.xz |
main_2026,submissions_2026 |
| c8cde50f32ca3f78a4c74a173c63449b |
943109d5fb200af15430ad32e185d9cd |
belpyramid-puzzle |
mihal |
sat |
empty |
no |
b00d4b7b7e1f59c3 |
bp5_CSO.normalised.cnf.xz |
main_2025,main_2026,submissions_2025 |
| ca18feb7d2bb6bee7a8ab28673fe1d62 |
8bd2a05987010afcdb36bbe281522bc2 |
allowable-seqence |
heule |
sat |
empty |
no |
89ed16a22c9d0bb9 |
as-p75-l27-o6-rot-4568.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ca7f7824a958b98512a0c96d73251f8b |
2e28dfd7e332d7519db70c2328eda2ae |
xor-shifting |
zhenwei |
sat |
empty |
no |
f3c9e635bfd7e407 |
xorshift_r16_180.sanitized.cnf.xz |
main_2026,submissions_2026 |
| cb2e8b7fada420c5046f587ea754d052 |
8230924e8ac3d44dd8ecbfdf126e7ea7 |
clique-formulas |
oertel |
unsat |
http://hdl.handle.net/10138/584822 |
no |
ace90e89155ba88b |
clique_n2_k10.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| cc42cc7a8022820cbd0e98595126d07e |
543de5369f44ddc949f43783f7209ee1 |
cril-misc |
frioux |
unsat |
empty |
no |
c6de7aa7776050c0 |
g2-T97.2.1.cnf.xz |
anni_2022,main_2017,main_2026 |
| cc436db9fe0278663ce376e068069815 |
f529e921ab398b29b47250199869ec02 |
bitvector |
unknown |
unsat |
empty |
no |
dcfb30f43f3e10a5 |
minandmaxor128.cnf.xz |
anni_2022,application_2009,application_2011,application_2013,application_2014,main_2015,main_2026,parallel_2015 |
| d0b5d1dc96a5bf33d2c65106c3b179a8 |
7db91b0f9d54477a7bac9a8d8d9f605d |
generic-csp |
connamacher |
unsat |
empty |
no |
09ee9de37b54b449 |
connm-ue-csp-sat-n600-d0.04-s1793042357.used-as.sat04-975.cnf.xz |
anni_2022,handmade_2004,main_2026 |
| d10b8bcd1bb5977c5ffe2d1859e4335f |
d10b5f00c4d53e01cd4e038278b362d6 |
xor-shifting |
zhenwei |
sat |
empty |
no |
f1757a53ac09ad83 |
xorshift_r15_175.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d1335d8a6a98a1988b54e1f481a64fcf |
fae64bb63f7736857a6a7040ef0ea46e |
graph-coloring |
anders |
unsat |
empty |
no |
51feeb7bc38ff304 |
mulsol.i.1.48.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d27f76623aed2fce608c092b2aafafc5 |
2440afa681ed386ac0dbdbc43bb9c60e |
exam-scheduling |
zheng |
unsat |
empty |
no |
dffa4432832b13e4 |
exam_95_70.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d418605014fdeb1236bfa720ac460c62 |
381ef30c3ff1e7d7f9b308310027b532 |
xor-shifting |
zhenwei |
sat |
empty |
no |
a83beccdc3113aa5 |
xorshift_r14_85.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d4a6b1a299c7a8ad6ea9769abcc60507 |
8167e485f49456087d0424f6705504d1 |
greentao |
kullmann |
unknown |
empty |
no |
57390eb7a0ed0f87 |
GreenTao_2-3-7_13850.cnf.xz |
main_2026 |
| d5949f26c5c5128ef2d4ac4d3b432cc2 |
5ce9f0c112b3a3fa2f0cef13aa77e1b2 |
allowable-seqence |
heule |
sat |
empty |
no |
277c395d5484a2b0 |
as-p51-l19-o8-II-568.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d699355595398f0765c5f51c9d0ad852 |
ea0c55a8e5359df36fe6d61b9eea45c1 |
argumentation |
ding |
sat |
empty |
no |
39bf65a2febcc895 |
crusti_g2io_350_0.5_255_21.af_299.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d737aeb8e2eb9baed7f007056b3874af |
d2c30eb196e678733609cc049e601443 |
argumentation |
ding |
sat |
empty |
no |
9b13666bcfc11b57 |
scc_7216_12_0.5_0.2_11.af.sanitized.cnf.xz |
main_2026,submissions_2026 |
| d8225a58e2ca7c2fb93c533f406c02d5 |
4c463bbedb5908b3d3de08e96bcdde6c |
antibandwidth |
biere |
sat |
http://hdl.handle.net/10138/318754 |
no |
68992d26305c1b30 |
abw-K-dwt__234.mtx-w50.cnf.xz |
main_2026 |
| d9fe50de72fb34ea94518c32d8f3077c |
76f9aabd4d057b9df645fc1fcbec6e8f |
cryptography |
soos |
unsat |
empty |
no |
fa082acca3dcc29f |
hitag2-7-60-0-0xe8fa35372ed37e2-80.cnf.xz |
anni_2022,application_2013,application_2014,crypto_2021,main_2026 |
| da34db9ea6b524f13708357f38432bb6 |
cb7cf5fd616e15a7c7a4a9c8f470df21 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
f24bbb32cf12336c |
cabp-V-nos6.mtx.rnd-k274.sanitized.cnf.xz |
main_2026,submissions_2026 |
| da6fae94ae1b1cedcced7169df02a762 |
4f57a6de70d5e84b2fe4dfff801fc5d8 |
boxfolding |
heule |
sat |
empty |
no |
3babddf984f63e78 |
1x1x13_1x3x6_pair_2_2_1_3_4_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| db099269d468029b70419bf4a49e99a1 |
4e07b513fbac4c5cec2c35a4926a6022 |
argumentation |
wallner |
sat |
http://hdl.handle.net/10138/135571 |
no |
eee603b44c3dddb6 |
stable-400-0.1-2-9876543214002.cnf.xz |
application_2014,main_2026 |
| db15a85651e0d941a11bf8640625edd8 |
8be327aec5fec9a1eefaff4b90b40fbc |
minimum-disagreement-parity |
bryant |
sat |
http://hdl.handle.net/10138/359079 |
no |
9fb97b64030ed771 |
mdp-32-11-sat.cnf.xz |
main_2024,main_2026,submissions_2022 |
| dbbcaa7797145dfddfa4fe73ce91fdec |
e5012693b9f34568a68c85d406f71da8 |
cyclic-anti-bandwidth |
hieu |
unsat |
empty |
no |
20654322d7d3e3c2 |
cabp-M-bcsstk06.mtx.rnd-k39.sanitized.cnf.xz |
main_2026,submissions_2026 |
| dc3ac89f98e9c3fc43450e256dce1154 |
ff7b02951256dc1c2aa7702824eea114 |
van-der-waerden |
gopalan |
unsat |
empty |
no |
6c288f74778f1bbd |
vdw_4_7_n110.sanitized.cnf.xz |
main_2026,submissions_2026 |
| dc691557cfebca28aefe7360768389e5 |
b09351eea52bd0aa108a4349f1f0875f |
ntil |
heule |
sat |
empty |
no |
17f2ce7d98e732ec |
ntil-90d-48.sanitized.cnf.xz |
main_2026,submissions_2026 |
| dc7817dfa2817916b266c1cfacd2ee66 |
21a9b6e12129b543792a14dff04eb8f4 |
ramsey |
zhengyu |
unsat |
http://hdl.handle.net/10138/584822 |
no |
30ffde9badb0cec5 |
constraints_25_4_5_12_12_0_0_0.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| dd062c307e10ebbb0d5641709ff26a7e |
6ec5c39c18827e964d08e118440da3ff |
syndrome-decoding |
liang |
sat |
empty |
no |
6cfc36af4810f832 |
SDP_108_15_6925.sanitized.cnf.xz |
main_2026,submissions_2026 |
| dd5d530ac8bf0019412d023488b075eb |
4536c62cf101dcdc130e910b56ed7921 |
p-center |
shuolin |
unsat |
empty |
no |
820af3ff860ae7d2 |
arles_thres20_p20_r4109.cnf.xz |
main_2026,submissions_2025 |
| ddf6fff9ebbbe9ec2a02f70b3316db6d |
ae22eece935ef0f8e3e3bf8c3de5be02 |
quasigroup-completion |
unknown |
sat |
empty |
no |
22d8b3da92d7093b |
QuasiGroup-4-12_c18.cnf.xz |
main_2019,main_2026 |
| de3440b67769e7af00e58ec9cce9847b |
1be72a1771bc61f829e28112312a7c44 |
syndrome-decoding |
liang |
unknown |
empty |
no |
416e11b1f252fd1a |
SDP_136_18_712.sanitized.cnf.xz |
main_2026,submissions_2026 |
| de8c42d50f1dbf43a731f1916dc6bf01 |
867ca841a58463501d944e518ad5812d |
multiplier-equivalence-checking |
yalun |
unsat |
empty |
no |
f1a3be7484d93d1f |
16_16_booth_dadda_mapped_and_and_wallace_origin_bit28.cnf.xz |
main_2025,main_2026,submissions_2025 |
| e1292f8d651e022362630d34fef69312 |
4e36182b05634c7b7f158a6578635b60 |
stable-semantics |
hangjiang |
sat |
empty |
no |
6f73a941f110a1b1 |
Medium-result_b30.af_80.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e2b819680a045a8af67f82fa2f3d945a |
bb4ef15d139503c80cbac11a94da27ff |
station-repacking |
newman |
unknown |
https://satcompetition.github.io/2020/downloads/station-repacking.pdf |
no |
783c3aeef445b7a5 |
59-134241.cnf.xz |
main_2026 |
| e305def35c314eec8266087e89a9ab46 |
8e24d32d21aeb3749f76b2d5f02f4f97 |
ntil |
heule |
sat |
empty |
no |
0712fd12c0787aae |
ntil-90d-35.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e3a132ecb8108f7d8a46b6686e686b60 |
27525ffad5272f53e9fffa8a7cf9cc2f |
linear-equations |
green |
sat |
empty |
no |
d5a6f30f130e0bae |
9.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e430acf720b63044e5c825a00a76b0eb |
8305024f6dbff1f2e40336e53693e375 |
relativized-pigeon-hole |
yldirimoglu |
unsat |
http://hdl.handle.net/10138/563824 |
no |
1446877e85276d5a |
rphp_p25_r25.cnf.xz |
main_2025,main_2026,submissions_2023 |
| e4d1892db27b721b88e5ee7e5987649f |
d0a9af751f7b7c2e349da65989e317d0 |
prime-testing |
jingchao |
unknown |
http://hdl.handle.net/10138/333647 |
no |
f033bb4ab3c60e7b |
quad_res_r33_m36.cnf.xz |
anni_2022,main_2021,main_2026 |
| e5066e18b03451d92863160ed8166bdf |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
e00b65f7568452b5 |
1x1x14_1x2x9_pair_2_4_0_3_1_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e55a49d8065d65650f24c0f3ecef30b6 |
36d1e273ee957e4f38149659679e32f5 |
maxsat-optimum |
cherif |
unsat |
http://hdl.handle.net/10138/359079 |
no |
5a351b464e0e0640 |
af-synthesis_stb_50_120_4_unsat.cnf.xz |
main_2022,main_2026,submissions_2022 |
| e5787bb4c8c29aa39b14a5e11387999d |
6844e3daf1e2b56f4682053d5a368cc3 |
graph-coloring |
anders |
unsat |
empty |
no |
d43c91a352a74301 |
fpsol2.i.2.29.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e67d733d9938c565d6359002333611ff |
9c335c90313fe4394e86d068ace3d77f |
argumentation |
niskanen |
sat |
http://hdl.handle.net/10138/563824 |
no |
60913d63b7cd9417 |
WS_500_16_70_10.apx_2_DS-ST.cnf.xz |
main_2026,submissions_2023 |
| e685a5d96e1ee9e051f191eca84b0d88 |
136d8ba60da58b217534935cc0a0cbea |
datapath-equivalence-checking |
xudong |
unsat |
empty |
no |
254d1eb903bdd974 |
sbdp4_140_2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e85fb114c33f450dc2622c78bc6fa019 |
2f2406553279854874841ae91933bc41 |
miter |
jinjinliu |
sat |
http://hdl.handle.net/10138/584822 |
no |
f80ff207db4051ea |
lru_7.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| e8ccbfaa2762cd0fc22b0ab05bacf529 |
f0d9b41e6b8a1167fd7e151337cacae4 |
ntil |
heule |
sat |
empty |
no |
910d7fab9cb9ac84 |
ntil-90d-36.sanitized.cnf.xz |
main_2026,submissions_2026 |
| e91253303b915493090c1f4b59d9e969 |
49d9ac41b139919e99510a58208a8334 |
graph-coloring |
anders |
unsat |
empty |
no |
2c32ef51664d4b42 |
lattice-20.19.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ebc40cf47836100655aea44ef1ed46da |
a54a5b9ed6248e3f56acc90b59deeca3 |
matrix-multiplication |
heule |
unknown |
empty |
no |
c3eb80b20bd65260 |
MM-23-2-2-3-B.cnf.xz |
main_2019,main_2026 |
| ee44c3f464238366729bf2cb16eb412a |
669320938d1a41c56e133aff20673759 |
stable-semantics |
hangjiang |
sat |
empty |
no |
a73f71f5f7856bf4 |
n384p5q2_vh.af_138.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ee8c86d39745aea1c1731d4f34bcaed7 |
c4246c033e41315425d694086755a4e1 |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
4a6dbb52dae072d9 |
6.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ef063cf2e17dd6472f514ab549a5eed5 |
7aa5fc7e6901e4edf999d15cc9d58e64 |
cyclic-anti-bandwidth |
hieu |
sat |
empty |
no |
4d893a8c188a25f8 |
cabp-V-nos6.mtx.rnd-k297.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f15a3ce898e0c66f309bf07d73744adf |
87ebfb396c398171127434bb2051d21e |
argumentation |
ding |
sat |
empty |
no |
ef7a6a54e695e8ce |
crusti_g2io_350_0.5_255_42.af_264.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f1d1a4fee20e2907c33465a88d1e24f2 |
c983de6f5dc9301db0ad84ae369a147a |
planning |
rintanen |
unknown |
empty |
no |
a4f9880e191a9db7 |
openstacks-sequencedstrips-nonadl-nonnegated-os-sequencedstrips-p30_1.035-NOTKNOWN.cnf.xz |
anni_2022,application_2011,application_2016,main_2026 |
| f2c6d035d0aa58cc06927af6be7a821f |
2e2bbe2a820e121aa56bd2c491f2c5f1 |
stable-semantics |
hangjiang |
unsat |
empty |
no |
32016c7b7471080e |
scc_9630_26_0.3_0.1_17.af_516.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f497bda3018958d7ba2d1cd99da3982e |
32934425a71645c65f55c4c779872e82 |
graph-coloring |
reeves |
unsat |
empty |
no |
ed2ad4cdd14f5d6a |
adv_gc_n100_k12_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f52a349677a5b5b5315b5954b3181fe3 |
bfff17ee6e99dc60caec6594568493de |
school-timetabling |
schreiber |
sat |
empty |
no |
992e45d5e2974fc7 |
schooltt-5-7-12-2-4-1.4-2.6-0.2-0.9-seed2.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f554b55356a5e0ed39dbf8c1030ebce0 |
b4b5ccb73adab1e7e26b0b0c6d571dde |
ecc-equivalence-checking |
guo |
sat |
empty |
no |
5458fea10cdb21d6 |
4.xz.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f5bb000a2fb23f3a5c19df2b6613cf77 |
2074774d140817e8466849f11fe6954b |
ntil |
heule |
unknown |
empty |
no |
9dbef897676f7ce9 |
ntil-90d-47.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f604f43d1f5525f3dab4090190adbc66 |
e1a78a6fd8972cd1461324ed7a061f18 |
boxfolding |
heule |
sat |
empty |
no |
b6530746fdecb462 |
1x1x14_1x2x9_pair_2_4_0_3_3_0.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f83424f869b61931d720f93e5a12df3c |
197c4f0a4b6ea6ecb18166fedd3f12fe |
sudoku-php |
shiv |
unsat |
empty |
no |
c7c75bf3ed5c924b |
php_sudoku_p20_h19.sanitized.cnf.xz |
main_2026,submissions_2026 |
| f8443057c188f6c9cfb711ff3d4aa6ff |
9a818462ee907730c021f58e6264a9ec |
quantum-kochen-specker |
zhengyu |
unsat |
http://hdl.handle.net/10138/584822 |
no |
a8ce7ca26e1e9a99 |
constraints_17_0.5_2.sanitized.cnf.xz |
main_2024,main_2026,submissions_2024 |
| f8a3fae231fe11905d91db3fb6c42449 |
16267255e428f2c90288d4567e0e2b94 |
mosoi-289 |
mosoi |
unknown |
empty |
no |
a3c0873940b74869 |
289-unsat-13x32.cnf.xz |
anni_2022,crafted_2011,main_2026 |
| fa3e27fb7209620b792d5c75a75d669b |
c7e635a3e55ac68c67f8695f6f808fdc |
school-timetabling |
schreiber |
unknown |
empty |
no |
2e741d852dd82dce |
schooltt-5-5-10-2-4-5-10-0.1-0.2-seed5.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fac2035ba83ac2d0c2d67509d3f82b94 |
9f5998ca6f41bfc6ee9c93cd6535d081 |
multiplier-equivalence-checking |
yalun |
unsat |
empty |
no |
2af32cff3c179a73 |
16_16_booth_dadda_origin_and_default_mapped_ultra_bit29.cnf.xz |
main_2026,submissions_2025 |
| faf4561dc9f61c71b926d7d0aec7fb4a |
86cef46cc652cf57687fc2b8068f3a52 |
bitvector |
brummayer |
unknown |
empty |
no |
2406282062ac5bb4 |
smulo128.cnf.xz |
anni_2022,application_2009,application_2016,main_2026 |
| fbbfbee9e6cba8bca18fbcfc23dcfcb6 |
c716c843309984f0cb5c78d9894c60e2 |
graph-coloring |
reeves |
unsat |
empty |
no |
f73df5eca25ac76b |
adv_gc_n100_k11_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fbd9968f5067604694f11f14c07c5527 |
194a59b1585af59a29eaed8639486107 |
count |
oertel |
unsat |
empty |
no |
9e87a4802069a11a |
count_p2_M45.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fbf3b9f8a03a1efedae3da04622fe96e |
4e167c5e7c1a2198405451c6ac2a941e |
circuit-equivalence-checking |
xinyan |
unsat |
http://hdl.handle.net/10138/359079 |
no |
b8a9197ef0d24760 |
sqrt-mitern168.cnf.xz |
main_2022,main_2026,submissions_2022 |
| fca71c20202ef404349136c3a00465eb |
fe10dc1beb5b0bb3a47cef7c29d64c93 |
edge-matching |
heule |
sat |
empty |
no |
b4d2896711e58ff8 |
em_8_4_5_fbc.cnf.xz |
anni_2022,crafted_2009,crafted_2011,crafted_2012,main_2026,portfolio_2012 |
| fd1e0ce3662b9b25d23eb01c6e53a425 |
aabe243211e008e11f1f206ba8e4a1bf |
ntil |
heule |
sat |
empty |
no |
967a9ac7d5d2ee6a |
ntil-90d-42.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fe776dd02d74e0d68a3e3fc3f9d934de |
7b74429e1795500e23ca162513bbfea1 |
van-der-waerden |
gopalan |
unknown |
empty |
no |
25de7c8456ba53be |
vdwb_k7_n3703.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fed1f1b55b33c7e0f8356832d571b0bf |
387bf641fccc24735006db107c1d107f |
ntil |
heule |
sat |
empty |
no |
5705b48784cf85f7 |
ntil-90d-41.sanitized.cnf.xz |
main_2026,submissions_2026 |
| fed3f8d39738c2e935e8ed13ddeb6967 |
8c629874ec668f8d3e10c46eb4abc7f4 |
linear-equations |
green |
sat |
empty |
no |
0d417b22401db5ac |
8.sanitized.cnf.xz |
main_2026,submissions_2026 |
| ff706804d01ac07e8b8502de6331f2de |
fe07e59abd241f9f0c756132d55d470f |
graph-coloring |
reeves |
unsat |
empty |
no |
02ec58b0a1614900 |
adv_gc_n200_k15_UNSAT_s42.sanitized.cnf.xz |
main_2026,submissions_2026 |