forked from arminbiere/cadiback
-
Notifications
You must be signed in to change notification settings - Fork 1
/
cadiback.cpp
1857 lines (1617 loc) · 56.6 KB
/
cadiback.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
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
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
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
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
// clang-format off
static const char * usage =
"usage: cadiback [ <option> ... ] [ <dimacs> [ <backbone> ] ]\n"
"\n"
"where '<option>' is one of the following:\n"
"\n"
" -c | --check check that backbones are really backbones\n"
" -f | --force force writing backbone to CNF alike path\n"
" -h | --help print this command line option summary\n"
" -l | --logging extensive logging for debugging\n"
" -n | --no-print do not print backbone\n"
" -q | --quiet disable all messages\n"
" -r | --report report what the SAT solver is doing\n"
" -s | --statistics always print full statistics (not only with '-v')\n"
" -v | --verbose increase verbosity (SAT solver needs three)\n"
" -V | --version print version and exit\n"
"\n"
" --no-constrain use activation literals instead of 'constrain'\n"
" --no-filter do not filter additional candidates\n"
" --no-fixed do not use root-level fixed literal information\n"
#ifndef NFLIP
" --no-flip do not try to find flippable candidates in models\n"
" --really-flip actually flip flippable candidates in models\n"
#endif
" --no-inprocessing disable any preprocessing and inprocessing\n"
"\n"
" --chunking increase constraint size by factor 10 if successful\n"
" --cores use core based algorithm as preprocessing step\n"
" --one-by-one try candidates one-by-one (do not use 'constrain')\n"
" --set-phase force phases to satisfy negation of candidates\n"
"\n"
" --big search for backbones in the BIG first\n"
" --big-no-els do not apply ELS to the BIG before extracting backbones\n"
" --big-roots only probe the roots of the ELS\n"
"\n"
" --default set optimization options to the default\n"
" --plain disable all optimizations, which is the same as:\n"
"\n"
" --no-filter --no-fixed"
#ifndef NFLIP
" --no-flip"
#endif
"\n"
" --no-inprocessing --one-by-one\n"
"\n"
"The first argument '<dimacs>' is a formula in DIMACS format for which\n"
"the backbone is determined and then printed (unless '-n' is specified).\n"
"If a second file argument '<backbone>' is given it specifies a file\n"
"to which the backbones are written. If no file argument is given the\n"
"formula is read from '<stdin>'. The same can be achieved by using '-'\n"
"as first argument. For reading all compressed file types supported by\n"
"'CaDiCaL' are supported.\n"
;
// clang-format on
#include <cassert>
#include <cctype>
#include <climits>
#include <cstdarg>
#include <cstdio>
#include <cstdlib>
#include <cstring>
#include <algorithm>
#include <numeric>
// Include the main 'CaDiCaL' API from 'cadical.hpp', but also some helper
// code from its library (from the 'CaDiCaL' source code directory').
#include "cadical.hpp" // Main 'CaDiCaL' API.
#include "resources.hpp" // Get time and memory usage.
#include "signal.hpp" // To set up a signal handler.
#include "version.hpp" // Print 'CaDiCaL' version too.
// 'CadiBack' build information is generated by './generate'.
#include "config.hpp"
// Verbosity level: -1=quiet, 0=default, 1=verbose, INT_MAX=logging.
static int verbosity;
// Checker solver to check that backbones are really back-bones, enabled by
// '-c' or '--check' (and quite expensive but useful for debugging).
//
static const char *check;
static CaDiCaL::Solver *checker;
// Force writing to CNF alike output file.
//
static const char *force;
// Print backbones by default. Otherwise only produce statistics.
//
static const char *no_print;
// Disable by default printing those 'c <character> ...' lines
// in the solver. If enabled is useful to see what is going on.
//
static bool report = false;
// From command line option '-s'.
//
static bool always_print_statistics;
// Use activation literals instead of 'constrain' API call.
//
static const char *no_constrain;
// Do not filter candidates by obtained models.
//
static const char *no_filter;
#ifndef NFLIP
// There is an extension of CaDiCaL with 'bool flippable (int lit)' and
// 'bool flip (lit)' API calls which allow check whether a literal can be
// flipped in the given model without falsifying the formula. The first
// 'flippable' function only checks this and 'flip' actually does it.
// We can use both to remove backbone candidates.
//
static const char *no_flip; // No use of flippable information.
static const char *really_flip; // Also actually flip flippable.
#endif
// The solver can give back information about root-level fixed literals
// which can cheaply be used to remove candidates or determine backbones.
//
static const char *no_fixed;
// Disable preprocessing and inprocessing.
//
static const char *no_inprocessing;
// Force the SAT solver to assign decisions to a value which would make the
// remaining backbone candidate literals false. This is a very natural idea
// but actual had negative effects and thus is now disabled by default.
//
static bool set_phase;
// Try each candidate after each other with a single assumption, i.e., do
// not use the 'constrain' optimization.
//
static const char *one_by_one;
// If we use constraints ('one-by-one' is off) then we might want to limit
// the size of the constraints. On success (solver returns 'unsatisfiable')
// we increase the constraint size by factor of 10 and on failure (solver
// finds a model) we reset constraint size to '1'.
//
static const char *chunking;
// If the following option is enabled we try to compute cores as in
// 'MiniBones', which assumes the conjunction of the complement of
// all the remaining backbone candidates. If solving under this
// assumption is satisfiable all the backbones which were assumed
// negatively are not backbones. Otherwise if it is unsatisfiable
// (the expected case) we check the failed literal among the assumptions,
// aka the (literal) core of the query. If that core has one element
// its negation is fixed and a backbone literal. Otherwise we remove
// from the set of assumed assumptions the core literals and try again until
// the set of assumptions becomes empty, in which case we fall back
// to the iterative algorithms.
//
static const char *cores;
// If this option is enable CadiBack will initially run our algorithm KB3 to
// search for Backbones that can be identified in the BIG (Binary
// Implication Graph) alone. This can be useful to find a (sometimes large)
// subset of backbones early on. If CadiBack is not used in an
// anytime-context this option usally doesn't yield any benefit, however it
// also usually doesn't cost much. See our FMCAD'23 paper on Big Backbones
// for a description of the algorithm and experimental resutls.
static const char *big;
// Applying ELS (Equivalent literal substitution) turns the BIG into a DAG.
// This isn't necessary for KB3 but can increase performance.
static const char *big_no_els;
// KB3 probes individual literals by propagating them in the BIG. To find
// all Backbones in the BIG it is sufficent to only probe the roots of the
// BIG. This can however have detrimental effects for KB3 and is disabled by
// default. This option requires ELS.
static const char *big_roots;
static int vars; // The number of variables in the CNF.
static int *fixed; // The resulting fixed backbone literals.
static int *candidates; // The backbone candidates (if non-zero).
static int *constraint; // Literals to constrain.
static int *core; // Remaining core literals.
static char *marked; // Flag used for ELS and BIG propagation.
// Here we have the files on which the tool operators. The first file
// argument is the '<dimacs>' if specified. Otherwise we will use '<stdin>'.
// If a second argument is specified we write the backbones to that file
// instead of printing them on '<stdout>'.
struct {
struct {
bool close;
FILE *file;
const char *path;
} dimacs, backbone;
} files;
// The actual incrementally used solver for backbone computation is a global
// variable such that it can be accessed by the signal handler to print
// statistics even if execution is interrupted or an error occurs.
//
static CaDiCaL::Solver *solver;
// Some statistics are collected here.
static struct {
size_t backbones; // Number of backbones found.
size_t dropped; // Number of non-backbones found.
size_t filtered; // Number of candidates with two models.
size_t checked; // How often checked model or backbone.
size_t fixed; // Number of fixed variables.
size_t failed; // Failed literals during core based approach.
size_t core; // Set by core based approach.
size_t big_backbones; // Number of backbones found.
struct {
size_t sat; // Calls with result SAT to SAT solver.
size_t unsat; // Calls with result UNSAT to SAT solver.
size_t unknown; // Interrupted solver calls.
size_t total; // Calls to SAT solver.
} calls;
#ifndef NFLIP
size_t flipped; // How often 'solver->flip (lit)' succeeded.
size_t flippable; // How often 'solver->flip (lit)' succeeded.
#endif
} statistics;
// Some time profiling information is collected here.
static double first_time, sat_time, unsat_time, solving_time, unknown_time;
static double satmax_time, unsatmax_time, flip_time, check_time;
static double big_search_time, big_read_time, big_els_time, big_check_time,
big_extension_time;
static volatile double *started, start_time;
// Declaring these with '__attribute__ ...' gives nice warnings.
static void die (const char *, ...) __attribute__ ((format (printf, 1, 2)));
static void msg (const char *, ...) __attribute__ ((format (printf, 1, 2)));
static void fatal (const char *, ...)
__attribute__ ((format (printf, 1, 2)));
// Actual message printing code starts here.
static void msg (const char *fmt, ...) {
if (verbosity < 0)
return;
fputs ("c ", stdout);
va_list ap;
va_start (ap, fmt);
vprintf (fmt, ap);
va_end (ap);
fputc ('\n', stdout);
fflush (stdout);
}
static void line () {
if (verbosity < 0)
return;
fputs ("c\n", stdout);
fflush (stdout);
}
static void die (const char *fmt, ...) {
fputs ("cadiback: error: ", stderr);
va_list ap;
va_start (ap, fmt);
vfprintf (stderr, fmt, ap);
va_end (ap);
fputc ('\n', stderr);
exit (1);
}
static void dbg (const char *fmt, ...) {
if (verbosity < INT_MAX)
return;
fputs ("c CADIBACK ", stdout);
va_list ap;
va_start (ap, fmt);
vprintf (fmt, ap);
va_end (ap);
fputc ('\n', stdout);
fflush (stdout);
}
static void fatal (const char *fmt, ...) {
fputs ("cadiback: fatal error: ", stderr);
va_list ap;
va_start (ap, fmt);
vfprintf (stderr, fmt, ap);
va_end (ap);
fputc ('\n', stderr);
fflush (stderr);
abort ();
}
static double average (double a, double b) { return b ? a / b : 0; }
static double percent (double a, double b) { return average (100 * a, b); }
static double time () { return CaDiCaL::absolute_process_time (); }
static void start_timer (double *timer) {
assert (!started);
start_time = time ();
started = timer;
}
static double stop_timer () {
assert (started);
double *timer = (double *) started;
started = 0;
double end = time ();
double delta = end - start_time;
*timer += delta;
return delta;
}
static void print_statistics () {
if (verbosity < 0)
return;
solver->prefix ("c ");
double total_time = time ();
volatile double *timer = started;
if (started) {
double delta = stop_timer ();
if (timer == &solving_time) {
statistics.calls.unknown++;
unknown_time += delta;
}
}
printf ("c\n");
printf ("c --- [ backbone statistics ] ");
printf ("------------------------------------------------\n");
printf ("c\n");
printf ("c found %9zu backbones %3.0f%%\n",
statistics.backbones, percent (statistics.backbones, vars));
printf ("c dropped %9zu candidates %3.0f%%\n",
statistics.dropped, percent (statistics.dropped, vars));
printf ("c\n");
printf ("c filtered %9zu candidates %3.0f%%\n",
statistics.filtered, percent (statistics.filtered, vars));
#ifndef NFLIP
printf ("c flippable %9zu candidates %3.0f%%\n",
statistics.flippable, percent (statistics.flippable, vars));
printf ("c flipped %9zu candidates %3.0f%%\n",
statistics.flipped, percent (statistics.flipped, vars));
#endif
printf ("c fixed %9zu candidates %3.0f%%\n", statistics.fixed,
percent (statistics.fixed, vars));
printf ("c core %9zu candidates %3.0f%%\n", statistics.core,
percent (statistics.core, vars));
printf ("c found %9zu big_backbone %3.0f%%\n",
statistics.big_backbones,
percent (statistics.big_backbones, statistics.backbones));
printf ("c failed %9zu candidates %3.0f%%\n", statistics.failed,
percent (statistics.failed, vars));
printf ("c\n");
printf ("c called solver %9zu times %3.0f%%\n",
statistics.calls.total,
percent (statistics.calls.total, vars + 1));
printf ("c satisfiable %9zu times %3.0f%%\n",
statistics.calls.sat,
percent (statistics.calls.sat, statistics.calls.total));
printf ("c unsatisfiable %9zu times %3.0f%%\n",
statistics.calls.unsat,
percent (statistics.calls.unsat, statistics.calls.total));
printf ("c\n");
printf ("c --- [ backbone profiling ] ");
printf ("-------------------------------------------------\n");
printf ("c\n");
if (always_print_statistics || verbosity > 0 || first_time)
printf ("c %10.2f %6.2f %% first\n", first_time,
percent (first_time, total_time));
if (verbosity > 0 || sat_time)
printf ("c %10.2f %6.2f %% sat\n", sat_time,
percent (sat_time, total_time));
if (verbosity > 0 || unsat_time)
printf ("c %10.2f %6.2f %% unsat\n", unsat_time,
percent (unsat_time, total_time));
if (verbosity > 0 || satmax_time)
printf ("c %10.2f %6.2f %% satmax\n", satmax_time,
percent (satmax_time, total_time));
if (verbosity > 0 || unsatmax_time)
printf ("c %10.2f %6.2f %% unsatmax\n", unsatmax_time,
percent (unsatmax_time, total_time));
if (verbosity > 0 || unknown_time)
printf ("c %10.2f %6.2f %% unknown\n", unknown_time,
percent (unknown_time, total_time));
if (verbosity > 0 || solving_time)
printf ("c %10.2f %6.2f %% solving\n", solving_time,
percent (solving_time, total_time));
if (verbosity > 0 || flip_time)
printf ("c %10.2f %6.2f %% flip\n", flip_time,
percent (flip_time, total_time));
if (big && (verbosity > 0 || big_read_time))
printf ("c %10.2f %6.2f %% big_read\n", big_read_time,
percent (big_read_time, total_time));
if (big && (verbosity > 0 || big_els_time))
printf ("c %10.2f %6.2f %% big_no_els\n", big_els_time,
percent (big_els_time, total_time));
if (big && (verbosity > 0 || big_search_time))
printf ("c %10.2f %6.2f %% big_search\n", big_search_time,
percent (big_search_time, total_time));
if (big && (verbosity > 0 || big_extension_time))
printf ("c %10.2f %6.2f %% big_extension\n", big_extension_time,
percent (big_extension_time, total_time));
if (big && (verbosity > 0 || big_check_time))
printf ("c %10.2f %6.2f %% big_check\n", big_check_time,
percent (big_check_time, total_time));
if (verbosity > 0 || check_time)
printf ("c %10.2f %6.2f %% check\n", check_time,
percent (check_time, total_time));
printf ("c ====================================\n");
printf ("c %10.2f 100.00 %% total\n", total_time);
printf ("c\n");
printf ("c\n");
fflush (stdout);
if (!solver)
return;
if (always_print_statistics || verbosity > 0)
solver->statistics ();
solver->resources ();
}
class CadiBackSignalHandler : public CaDiCaL::Handler {
virtual void catch_signal (int sig) {
if (verbosity < 0)
return;
printf ("c caught signal %d\n", sig);
print_statistics ();
}
};
static int remaining_candidates () {
size_t determined = statistics.dropped + statistics.backbones;
assert (determined <= (size_t) vars);
return vars - determined;
}
// Provide a wrapper function for calling the main solver.
static int solve () {
assert (solver);
start_timer (&solving_time);
statistics.calls.total++;
{
char prefix[32];
snprintf (prefix, sizeof prefix, "c #%zu ", statistics.calls.total);
solver->prefix (prefix);
}
int remain = remaining_candidates ();
if (report || verbosity > 1) {
line ();
msg ("---- [ "
"SAT solver call #%zu (%d candidates remain %.0f%%)"
" ] ----",
statistics.calls.total, remain, percent (remain, vars));
line ();
} else if (verbosity > 0)
msg ("SAT solver call %zu (%d candidates remain %0.f%%)",
statistics.calls.total, remain, percent (remain, vars));
int res = solver->solve ();
if (res == 10) {
statistics.calls.sat++;
} else {
assert (res == 20);
statistics.calls.unsat++;
}
double delta = stop_timer ();
if (statistics.calls.total == 1)
first_time = delta;
if (res == 10) {
sat_time += delta;
if (delta > satmax_time)
satmax_time = delta;
} else {
unsat_time += delta;
if (delta > unsatmax_time)
unsatmax_time = delta;
}
return res;
}
// If 'check' is set (through '-c' or '--check') then we check all literals
// to either be a backbone literal or that they have a model. The cost for
// doing this is expensive and needs one call to the checker SAT solver for
// each literal. The checker solver is copied from the main incremental
// solver after parsing. The first model of the main solver is not checked.
static void inc_checked () {
assert (checker);
statistics.checked++;
char prefix[32];
snprintf (prefix, sizeof prefix, "c C%zu ", statistics.checked);
checker->prefix (prefix);
}
static void check_model (int lit) {
double *timer = (double *) started;
if (timer)
stop_timer ();
start_timer (&check_time);
inc_checked ();
dbg ("checking that there is a model with %d", lit);
checker->assume (lit);
int tmp = checker->solve ();
if (tmp != 10)
fatal ("checking claimed model for %d failed", lit);
stop_timer ();
if (timer)
start_timer (timer);
}
static void check_backbone (int lit) {
start_timer (&check_time);
inc_checked ();
dbg ("checking that there is no model with %d", -lit);
checker->assume (-lit);
int tmp = checker->solve ();
if (tmp != 20)
fatal ("checking %d backbone failed", -lit);
stop_timer ();
}
// The given variable was proven not be a backbone variable.
static void drop_candidate (int idx) {
int lit = candidates[idx];
dbg ("dropping candidate literal %d", lit);
assert (lit);
candidates[idx] = 0;
assert (!fixed[idx]);
assert (statistics.dropped < (size_t) vars);
statistics.dropped++;
if (set_phase)
solver->unphase (idx);
if (check)
check_model (-lit);
}
#ifndef NFLIP
// This is a technique first implemented in 'Kitten' for SAT sweeping within
// 'Kissat', which checks whether it is possible to flip the value of a
// literal in a model of the formula without making the formula false. It
// goes over the watches of the literal and checks if all watched clauses
// are double satisfied.
// This requires support by 'CaDiCaL' via the 'bool flippable (int lit)' or
// 'bool flip (int lit)' functions function, which is slightly more
// expensive than the one in 'Kitten' as in essence it is compatible with
// blocking literals (used in 'CaDiCaL' but not in 'Kitten'). The first
// check for flipping a literal will need to propagate all the assigned
// literals and find replacement watches while ignoring blocking literals.
// We check all remaining backbone candidate literals until none can be
// flipped anymore. This optimization pays off if on average close to one
// literal can be flipped but still is pretty cheap if not.
// As only more recent versions of CaDiCaL (starting with '1.5.4-rc.2')
// support flipping we keep it under compile time control too (beside
// allowing to disable it during run-time).
static void try_to_flip_remaining (int start) {
if (no_flip)
return;
start_timer (&flip_time);
for (int idx = start; idx <= vars; idx++) {
int lit = candidates[idx];
if (!lit)
continue;
if (really_flip) {
if (!solver->flip (lit))
continue;
dbg ("flipped literal %d", lit);
statistics.flipped++;
} else {
if (!solver->flippable (lit))
continue;
dbg ("literal %d can be flipped", lit);
statistics.flippable++;
}
drop_candidate (idx);
}
stop_timer ();
}
#else
#define try_to_flip_remaining(START) \
do { \
} while (0)
#endif
// If the SAT solver has a model in which the candidate backbone literal for
// the given variable index is false, we drop it as a backbone candidate.
static bool filter_candidate (int idx) {
assert (!no_filter);
int lit = candidates[idx];
if (!lit)
return false;
int val = solver->val (idx) < 0 ? -idx : idx; // Legacy support.
assert (val == idx || val == -idx);
if (lit == val)
return false;
assert (lit == -val);
dbg ("model also satisfies negation %d "
"of backbone candidate %d thus dropping %d",
-lit, lit, lit);
statistics.filtered++;
drop_candidate (idx);
return true;
}
// Try dropping as many variables as possible from 'start' to 'vars' based
// on the value of the remaining candidates in the current model.
static void filter_candidates (int start) {
if (no_filter || start > vars)
return;
unsigned res = 0;
for (int idx = start; idx <= vars; idx++)
if (filter_candidate (idx), !res)
res++;
assert (res);
(void) res;
}
// Drop the first candidate refuted by the current model and drop it. In
// principle we could have merged this logic with 'filter_candidates' but we
// want to distinguish the one guaranteed dropped candidate if we find a
// model from the additional ones filtered by the model both with respect to
// statistics as well as supporting '--no-filter'.
static int drop_first_candidate (int start) {
assert (start <= vars);
int idx = start, lit = 0, val = 0;
for (;; idx++) {
assert (idx <= vars);
lit = candidates[idx];
if (!lit)
continue;
val = solver->val (idx) < 0 ? -idx : idx; // Legacy support.
assert (val == idx || val == -idx);
if (lit == -val)
break;
}
assert (lit);
assert (lit == -val);
assert (idx <= vars);
assert (candidates[idx] == lit);
dbg ("model satisfies negation %d "
"of backbone candidate %d thus dropping %d",
-lit, lit, lit);
drop_candidate (idx);
return idx;
}
// Assume the given variable is a backbone variable with its candidate
// literal as backbone literal. Optionally print, check and count it.
static bool backbone_variable (int idx) {
int lit = candidates[idx];
if (!lit)
return false;
fixed[idx] = lit;
candidates[idx] = 0;
if (!no_print) {
fprintf (files.backbone.file, "b %d\n", lit);
fflush (files.backbone.file);
}
if (checker)
check_backbone (lit);
assert (statistics.backbones < (size_t) vars);
statistics.backbones++;
return true;
}
static bool fix_candidate (int idx) {
assert (!no_fixed);
int lit = candidates[idx];
assert (lit);
int tmp = solver->fixed (lit);
if (!tmp)
return false;
if (tmp > 0) {
dbg ("found fixed backbone %d", lit);
backbone_variable (idx);
}
if (tmp < 0) {
dbg ("removing fixed backbone %d candidate", lit);
drop_candidate (idx);
}
statistics.fixed++;
return true;
}
// Force all variables from 'start' to 'vars' to be backbones unless they
// were already dropped. This is used for 'constrain'.
static void backbone_variables (int assumed) {
int count = 0;
for (int i = 0; i != assumed; i++) {
int lit = constraint[i];
int idx = abs (lit);
if (backbone_variable (idx))
count++;
}
assert (count);
(void) count;
}
// Want to make sure not to overwrite accidentally (without '--force') files
// which look like CNF files (as this happened to me all the time).
static bool match_until_dot (const char *str, const char *pattern) {
assert (str);
assert (pattern);
const char *p = str, *q = pattern;
while (*q) {
if (tolower (*p) != tolower (*q))
return false;
p++, q++;
}
return !*p || *p == '.';
}
static bool looks_like_a_dimacs_file (const char *path) {
const char *dots[2] = {0, 0};
char ch;
for (const char *p = path; (ch = *p); p++)
if (ch == '.')
dots[0] = dots[1], dots[1] = p + 1;
const char *suffix = dots[1];
if (!suffix)
return false;
if (match_until_dot (suffix, "gz") || match_until_dot (suffix, "bz2") ||
match_until_dot (suffix, "xz") || match_until_dot (suffix, "lzma"))
suffix = dots[0];
if (!suffix)
return false;
return match_until_dot (suffix, "dimacs") ||
match_until_dot (suffix, "cnf");
}
int ind (int i) {
assert (i);
return (abs (i) << 1) - 1 - (i > 0);
}
int lit (int i) { return ((i >> 1) + 1) * ((i & 1) ? -1 : 1); }
int var (int i) { return (i >> 1) + 1; }
int neg (int i) { return i ^ 1; }
class BigDegreeIterator : public CaDiCaL::ClauseIterator {
public:
int num_edges = 0;
std::vector<int> &f;
BigDegreeIterator (std::vector<int> &f) : f (f) {}
bool clause (const std::vector<int> &c) {
if (c.size () != 2)
return true;
num_edges += 2;
++f[neg (ind (c[0])) + 2];
++f[neg (ind (c[1])) + 2];
return true;
}
};
class BigEdgeIterator : public CaDiCaL::ClauseIterator {
public:
std::vector<int> &f, &e;
BigEdgeIterator (std::vector<int> &f, std::vector<int> &e)
: f (f), e (e) {}
bool clause (const std::vector<int> &c) {
if (c.size () != 2)
return true;
const int u = ind (c[0]);
const int v = ind (c[1]);
e[f[neg (u) + 1]++] = v;
e[f[neg (v) + 1]++] = u;
return true;
}
};
static void big_extract (int num_nodes, std::vector<int> &f,
std::vector<int> &e) {
f.resize (num_nodes + 2);
BigDegreeIterator fillF (f);
solver->traverse_clauses (fillF);
e.resize (fillF.num_edges);
for (size_t i = 1; i < f.size (); i++)
f[i] += f[i - 1];
BigEdgeIterator fillE (f, e);
solver->traverse_clauses (fillE);
f.pop_back ();
assert (f.size () == static_cast<size_t> (num_nodes + 1));
msg ("read BIG with %d nodes and %d edges", num_nodes, fillF.num_edges);
}
static int big_els (std::vector<int> &f, std::vector<int> &e,
std::vector<int> &extension, bool check_only = false) {
if (e.empty ())
return 0;
// tarjan
const unsigned INV = UINT_MAX;
// using MSB as closed flag
const unsigned MSB = 1 << (sizeof (unsigned) * 8 - 1);
const int n = f.size () - 1;
std::vector<unsigned> rep (n, INV);
std::vector<int> work, scc;
unsigned i = 0;
for (int u = 0; u < n; u++) {
if (rep[u] != INV)
continue;
work = {u};
while (work.size () > 0) {
int u = work.back ();
if (u == static_cast<int> (INV)) {
work.pop_back ();
int u = work.back ();
work.pop_back ();
bool closed_scc = true;
for (int v = f[u]; v < f[u + 1]; v++) {
if (rep[u] > rep[e[v]]) {
rep[u] = rep[e[v]];
closed_scc = false;
}
}
if (closed_scc) {
size_t entry = scc.size () - 1;
int min_lit = scc[entry];
while (scc[entry] != u) {
entry--;
min_lit = std::min (min_lit, scc[entry]);
}
assert (scc[entry] == u);
for (size_t i = entry; i < scc.size (); ++i) {
int v = scc[i];
if (neg (min_lit) == v)
return 20; // unsatisfiable
assert (rep[v] < MSB);
rep[v] = min_lit | MSB;
}
scc.resize (entry);
assert (scc.size () == 0 or scc.back () != u);
}
} else if (rep[u] == INV) {
scc.push_back (u);
rep[u] = i++;
work.push_back (INV);
for (int v = f[u]; v < f[u + 1]; v++) {
if (rep[e[v]] == INV) {
work.push_back (e[v]);
}
}
} else {
work.pop_back ();
}
}
assert (scc.size () == 0);
}
std::transform (rep.begin (), rep.end (), rep.begin (),
[] (int x) { return x ^ MSB; });
assert (std::all_of (rep.begin (), rep.end (),
[] (unsigned n) { return n < MSB; }));
if (check_only)
return 0;
// sort (stable) node indices by their rep
std::vector<int> sccs (n);
std::iota (sccs.begin (), sccs.end (), 0);
std::stable_sort (sccs.begin (), sccs.end (),
[&] (int a, int b) { return rep[a] < rep[b]; });
// substitute
int r = -1, u_prime = -1, l = 0;
std::vector<int> f_prime (n + 1), e_prime, edges;
e_prime.reserve (n);
for (int u : sccs) {
int r_prime = rep[u];
if (r_prime != r) {
if (l) {
l = 0;
extension.push_back (-1);
} else if (r != -1)
extension.pop_back ();
r = r_prime;
for (int v : edges) {
marked[v] = false;
e_prime.push_back (v);
}
assert (static_cast<size_t> (u_prime + 1) < f_prime.size ());
f_prime.at (u_prime + 1) = edges.size (); // needs prefix sum
edges.clear ();
u_prime = r;
} else
l++;
extension.push_back (u);
assert (static_cast<int> (rep[u]) == r);
for (int i = f[u]; i < f[u + 1]; ++i) {
const int v = rep[e[i]];
if (v == r)
continue;
if (!marked[v]) {
edges.push_back (v);
marked[v] = true;
}
}
}
if (l) {
l = 0;
extension.push_back (-1);
} else
extension.pop_back ();
if (edges.size ()) {
for (int v : edges) {
marked[v] = false;
e_prime.push_back (v);
}
f_prime[u_prime + 1] = edges.size (); // needs prefix sum
edges.clear ();
}
for (size_t i = 1; i < f_prime.size (); i++)
f_prime[i] += f_prime[i - 1];
assert (f_prime.size () == static_cast<size_t> (n + 1));
assert (e_prime.size () == static_cast<size_t> (f_prime.back ()));
f = std::move (f_prime);
e = std::move (e_prime);
return 0;
}
static bool big_backbone_node (int node) {
int literal = lit (node);
int idx = var (node);
if (!literal)
return false;
fixed[idx] = literal;
if (!no_print) {
fprintf (files.backbone.file, "b %d\n", literal);
fflush (files.backbone.file);
}
solver->add (literal);
solver->add (0);
assert (statistics.backbones < (size_t) vars);
statistics.backbones++;
statistics.big_backbones++;
return true;
}
static void big_backbone_base (const std::vector<int> &f,
const std::vector<int> &e) {
msg ("BIG base searching for backbones after %.2f seconds", time ());
const int n = f.size () - 1;
for (int c = 0; c < n; ++c) {
if (fixed[var (c)])
continue;
marked[c] = true;
std::vector<int> tree{c};
size_t i = 0;
while (i < tree.size ()) {
const int u = tree[i++];
for (int j = f[u]; j < f[u + 1]; ++j) {