Novel Atomic-Set Computation Based On SAT Solving

[h3ssto]

Recently, we evaluated the performance of our novel atomic-set computation algorithm [1] against the one implemented in FeatJar. We found that FeatJar, on average, is about 40x slower. Now we are curious to understand whether this difference stems from the algorithm or simply FeatJar's implementation in Java and its use of SAT4J.

As our algorithm should be easy to implement, we are hopeful that this question can be answered without much effort.

[1] https://arxiv.org/abs/2501.12490

[h3ssto]

e7f8652 or following commits introduced a regression, leading to missing atomic sets in the output (file).

For instance, for ea2468.dimacs (attached):

FeatJar:

[[1, 8, 9, 10, 11, 12], [128, 129, 130, 131, 132, 133, 148, 149, 152, 95, 96, 100, 107, 109, 114, 116, 120, 121, 123, 125], [98, 421], [771, 99], [104, 103], [105, 106], [117, 118], [160, 161, 162, 163, 164, 172, 173, 154, 155, 158], [174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 208], [209, 210, 211, 214, 216, 217, 218, 219, 220, 221], [212, 215], [224, 225], [226, 228, 229, 303, 304, 305, 306], [231, 236, 237, 238, 239], [232, 233, 234], [240, 242], [244, 245], [246, 247], [248, 249], [250, 251], [252, 253], [256, 255], [257, 258], [259, 260], [261, 262], [265, 266, 271, 272, 273], [268, 269, 270], [274, 275], [277, 278, 279, 280, 281], [283, 284, 285, 286, 287], [289, 290, 291, 292, 293], [295, 296, 297, 298, 299], [300, 301], [308, 309, 310, 311, 312, 313, 314, 315, 316, 317], [320, 323, 337, 338, 318, 319], [321, 322], [331, 333], [339, 341], [352, 353, 354, 355, 356, 360, 361], [357, 358], [362, 368, 369, 370, 371], [365, 366, 367], [407, 393, 372, 405, 406, 404, 408, 409, 410], [398, 373, 382], [514, 516, 518, 519, 520, 521, 411, 412, 424, 425, 426, 427, 431, 432, 433, 442, 445, 446, 453, 454, 455, 475, 476, 477, 479, 490], [413, 414, 415], [416, 417], [435, 436], [443, 444], [448, 447], [460, 462], [465, 466, 467, 468, 469, 470, 471], [472, 473], [496, 494], [548, 549, 550, 551, 552, 522, 523, 524, 526, 529, 534, 535], [544, 545, 540, 543], [651, 652, 654, 656, 657, 658, 660, 663, 665, 667, 670, 672, 673, 675, 680, 553, 554, 555, 556, 557, 558, 681, 560, 561, 683, 563, 685, 565, 566, 686, 568, 688, 689, 691, 692, 696, 701, 702, 708, 709, 711, 712, 714, 589, 590, 719, 592, 594, 596, 724, 598, 600, 602, 731, 604, 732, 606, 733, 608, 610, 612, 615, 617, 632], [736, 743, 745, 746, 747, 748, 735], [749, 750, 751, 752, 753], [770, 772, 773, 774, 775, 754, 756, 757, 758], [760, 762], [766, 767], [800, 776, 778, 779, 780, 781, 786, 790, 791, 797, 798, 799], [782, 783], [801, 802, 806, 808, 809, 816, 817, 818, 819, 820, 821], [832, 833, 822, 826, 828, 830, 831], [834, 840, 841, 842, 843, 844, 855, 856, 857, 858, 859], [870, 876, 877, 878, 879, 880, 860, 861, 862, 863], [864, 865], [912, 881], [889, 890, 891, 892], [899, 900], [908, 902], [904, 905], [909, 910, 911], [913, 914, 915, 936, 937, 938, 941, 942, 943, 961, 963, 964, 965, 966, 967, 968, 969, 970, 971, 972, 973, 974, 975, 976, 977, 978, 979], [922, 923], [924, 925], [926, 927], [928, 929], [930, 931], [932, 933], [934, 935], [939, 940], [944, 945, 948, 949], [946, 947], [954, 955, 950, 951], [952, 953], [957, 958], [960, 959], [992, 993, 980, 981, 982, 983, 987, 990, 991], [1000, 1001, 1002, 1003, 1004, 1006, 1007, 1011, 1012, 1013, 1014], [1016, 1021, 1022, 1023], [1017, 1019], [1024, 1025, 1029, 1030, 1031, 1032, 1033, 1034, 1038, 1042], [1036, 1037], [1043, 1044, 1045, 1046, 1047, 1048, 1081, 1082, 1083, 1084, 1086, 1118, 1119, 1126, 1127, 1130, 1131, 1132, 1133, 1134, 1135, 1136, 1137, 1138, 1139, 1140, 1141, 1144, 1146, 1147, 1148], [1058, 1054, 1055], [1056, 1057], [1059, 1060], [1072, 1066, 1062], [1064, 1065, 1063], [1069, 1070], [1074, 1075, 1076], [1089, 1090, 1091], [1092, 1093, 1094, 1095, 1096, 1097], [1142, 1143], [1152, 1153, 1154, 1155, 1156, 1157, 1159, 1162, 1149, 1150, 1151], [1168, 1169, 1163, 1167], [1170, 1171, 1172, 1173, 1174, 1175, 1176, 1178, 1180, 1181, 1182, 1183], [1184, 1185, 1186, 1187, 1188, 1189], [1217, 1190, 1191, 1193, 1194, 1195, 1196, 1207, 1209, 1212, 1213, 1214, 1215], [1203, 1204, 1205, 1206], [1218, 1219], [1221, 1227, 1229, 1230, 1231], [1232, 1222], [1224, 1223], [1225, 1226], [1235, 1236], [1237, 1238], [1239, 1242, 1243, 1244, 1245], [1287, 1288, 1289, 1290, 1291, 1292, 1246, 1247], [1256, 1257, 1258], [1264, 1265, 1266, 1263], [1267, 1268], [1269, 1270], [1272, 1273, 1274], [1275, 1276, 1277, 1278], [1280, 1279], [1281, 1282], [1284, 1285, 1286], [1293, 1294], [1296, 1297, 1309, 1311], [1298, 1299], [1300, 1301, 1302, 1303, 1304], [1305, 1308], [1306, 1307], [1315, 1316], [1317, 1324, 1330, 1331, 1332, 1334], [1320, 1321, 1318, 1319], [1329, 1325], [1336, 1335], [1344, 1345, 1346, 1347, 1337, 1338, 1342, 1343], [1348, 1349, 1350, 1351, 1352, 1353, 1356, 1357, 1358, 1359, 1360, 1373], [1368, 1369, 1367], [1370, 1371, 1372], [1377, 1378, 1379, 1374], [1382, 1383, 1384, 1385, 1392], [1389, 1390, 1391], [1393, 1394, 1395, 1396], [1397, 1399], [1400, 1401, 1402], [1403, 1404, 1405], [1408, 1406, 1407]]

While the following sets are correct:

[[1, 8, 9, 10, 11, 12], [2, 3, 4, 5, 6, 7, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 1110, 1111, 1112, 1113, 1114, 1115, 1116, 1117, 126, 150, 169, 1323, 1340, 334, 335, 359, 883, 884, 1104, 1105, 441, 1106, 1107, 1108, 1109, 480, 481, 482, 483, 484, 485, 486, 487, 994, 995, 996, 997, 998, 999], [128, 129, 130, 131, 132, 133, 148, 149, 152, 95, 96, 100, 107, 109, 114, 116, 120, 121, 123, 125], [98, 421], [771, 99], [104, 103], [105, 106], [117, 118], [160, 161, 162, 163, 164, 172, 173, 154, 155, 158], [174, 175, 176, 177, 178, 179, 180, 181, 182, 183, 184, 185, 186, 187, 188, 189, 190, 191, 192, 193, 194, 195, 196, 197, 198, 199, 200, 201, 202, 203, 204, 205, 206, 208], [209, 210, 211, 214, 216, 217, 218, 219, 220, 221], [212, 215], [224, 225], [226, 228, 229, 303, 304, 305, 306], [231, 236, 237, 238, 239], [232, 233, 234], [240, 242], [244, 245], [246, 247], [248, 249], [250, 251], [252, 253], [256, 255], [257, 258], [259, 260], [261, 262], [265, 266, 271, 272, 273], [268, 269, 270], [274, 275], [277, 278, 279, 280, 281], [283, 284, 285, 286, 287], [289, 290, 291, 292, 293], [295, 296, 297, 298, 299], [300, 301], [308, 309, 310, 311, 312, 313, 314, 315, 316, 317], [320, 323, 337, 338, 318, 319], [321, 322], [331, 333], [339, 341], [352, 353, 354, 355, 356, 360, 361], [357, 358], [362, 368, 369, 370, 371], [365, 366, 367], [407, 393, 372, 405, 406, 404, 408, 409, 410], [382, 373, 398], [514, 516, 518, 519, 520, 521, 411, 412, 424, 425, 426, 427, 431, 432, 433, 442, 445, 446, 453, 454, 455, 475, 476, 477, 479, 490], [413, 414, 415], [416, 417], [435, 436], [443, 444], [448, 447], [460, 462], [465, 466, 467, 468, 469, 470, 471], [472, 473], [496, 494], [548, 549, 550, 551, 552, 522, 523, 524, 526, 529, 534, 535], [544, 545, 540, 543], [651, 652, 654, 656, 657, 658, 660, 663, 665, 667, 670, 672, 673, 675, 680, 553, 681, 554, 555, 556, 557, 558, 683, 560, 561, 685, 563, 686, 565, 566, 688, 568, 689, 691, 692, 696, 701, 702, 708, 709, 711, 712, 714, 589, 590, 719, 592, 594, 596, 724, 598, 600, 602, 731, 604, 732, 606, 733, 608, 610, 612, 615, 617, 632], [736, 743, 745, 746, 747, 748, 735], [749, 750, 751, 752, 753], [770, 772, 773, 774, 775, 754, 756, 757, 758], [760, 762], [766, 767], [800, 776, 778, 779, 780, 781, 786, 790, 791, 797, 798, 799], [782, 783], [801, 802, 806, 808, 809, 816, 817, 818, 819, 820, 821], [832, 833, 822, 826, 828, 830, 831], [834, 840, 841, 842, 843, 844, 855, 856, 857, 858, 859], [870, 876, 877, 878, 879, 880, 860, 861, 862, 863], [864, 865], [912, 881], [889, 890, 891, 892], [899, 900], [908, 902], [904, 905], [909, 910, 911], [913, 914, 915, 936, 937, 938, 941, 942, 943, 961, 963, 964, 965, 966, 967, 968, 969, 970, 971, 972, 973, 974, 975, 976, 977, 978, 979], [922, 923], [924, 925], [926, 927], [928, 929], [930, 931], [932, 933], [934, 935], [939, 940], [944, 945, 948, 949], [946, 947], [954, 955, 950, 951], [952, 953], [957, 958], [960, 959], [992, 993, 980, 981, 982, 983, 987, 990, 991], [1000, 1001, 1002, 1003, 1004, 1006, 1007, 1011, 1012, 1013, 1014], [1016, 1021, 1022, 1023], [1017, 1019], [1024, 1025, 1029, 1030, 1031, 1032, 1033, 1034, 1038, 1042], [1036, 1037], [1043, 1044, 1045, 1046, 1047, 1048, 1081, 1082, 1083, 1084, 1086, 1118, 1119, 1126, 1127, 1130, 1131, 1132, 1133, 1134, 1135, 1136, 1137, 1138, 1139, 1140, 1141, 1144, 1146, 1147, 1148], [1058, 1054, 1055], [1056, 1057], [1059, 1060], [1072, 1066, 1062], [1064, 1065, 1063], [1069, 1070], [1074, 1075, 1076], [1089, 1090, 1091], [1092, 1093, 1094, 1095, 1096, 1097], [1142, 1143], [1152, 1153, 1154, 1155, 1156, 1157, 1159, 1162, 1149, 1150, 1151], [1168, 1169, 1163, 1167], [1170, 1171, 1172, 1173, 1174, 1175, 1176, 1178, 1180, 1181, 1182, 1183], [1184, 1185, 1186, 1187, 1188, 1189], [1217, 1190, 1191, 1193, 1194, 1195, 1196, 1207, 1209, 1212, 1213, 1214, 1215], [1203, 1204, 1205, 1206], [1218, 1219], [1221, 1227, 1229, 1230, 1231], [1232, 1222], [1224, 1223], [1225, 1226], [1235, 1236], [1237, 1238], [1239, 1242, 1243, 1244, 1245], [1287, 1288, 1289, 1290, 1291, 1292, 1246, 1247], [1256, 1257, 1258], [1264, 1265, 1266, 1263], [1267, 1268], [1269, 1270], [1272, 1273, 1274], [1275, 1276, 1277, 1278], [1280, 1279], [1281, 1282], [1284, 1285, 1286], [1293, 1294], [1296, 1297, 1309, 1311], [1298, 1299], [1300, 1301, 1302, 1303, 1304], [1305, 1308], [1306, 1307], [1315, 1316], [1317, 1324, 1330, 1331, 1332, 1334], [1320, 1321, 1318, 1319], [1329, 1325], [1336, 1335], [1344, 1345, 1346, 1347, 1337, 1338, 1342, 1343], [1348, 1349, 1350, 1351, 1352, 1353, 1356, 1357, 1358, 1359, 1360, 1373], [1368, 1369, 1367], [1370, 1371, 1372], [1377, 1378, 1379, 1374], [1382, 1383, 1384, 1385, 1392], [1389, 1390, 1391], [1393, 1394, 1395, 1396], [1397, 1399], [1400, 1401, 1402], [1403, 1404, 1405], [1408, 1406, 1407]]

For instance, the second atomic set, containing variable 2, is missing.

Furthermore, the file output format has changed, currently the sample file format is used, which naturally mainly consists of 0s.

example.zip

[h3ssto]

A combination of commits that produces correct results:

• base aae98ff13f08598668851f85e0dabaf751a23b34
• formula 9ce6df5c1dd28afc9296b19cd291b7539fa46450
• formula-analysis-sat4j c7b5991