From c5cce1b9b35bc74566f192c43620bff03e4a9ff6 Mon Sep 17 00:00:00 2001 From: Armin Biere Date: Wed, 15 Jun 2022 17:37:25 +0200 Subject: [PATCH] imported sc2022-bulky --- LICENSE | 1 + NEWS.md | 29 + README.md | 2 +- VERSION | 2 +- configure | 9 + scripts/prepare-competition.sh | 16 +- src/allocate.h | 5 + src/analyze.c | 23 +- src/ands.c | 2 +- src/application.c | 11 +- src/backbone.c | 2 +- src/backtrack.c | 6 +- src/backward.c | 10 +- src/bits.h | 4 +- src/branching.c | 56 + src/branching.h | 11 + src/build.c | 18 +- src/bump.c | 102 +- src/bump.h | 4 +- src/colors.h | 4 +- src/compact.c | 30 +- src/config.h | 7 - src/decide.c | 11 +- src/deduce.c | 5 +- src/definition.c | 22 +- src/dump.c | 9 +- src/eliminate.c | 393 ++--- src/eliminate.h | 5 - src/failed.c | 7 +- src/flags.c | 9 +- src/forward.c | 66 +- src/ifthenelse.c | 6 +- src/inlinescore.h | 19 +- src/internal.c | 7 +- src/internal.h | 15 +- src/{limits.c => kimits.c} | 86 +- src/{limits.h => kimits.h} | 44 +- src/kissat.h | 2 +- src/kitten.c | 241 ++- src/kitten.h | 7 +- src/learn.c | 2 +- src/logging.c | 90 +- src/logging.h | 45 + src/makefile | 1 - src/mode.c | 12 +- src/options.h | 42 +- src/probe.c | 19 +- src/profile.h | 1 + src/promote.c | 8 +- src/promote.h | 7 +- src/propbeyond.c | 35 + src/propbeyond.h | 9 + src/proplit.h | 219 +-- src/propsearch.c | 3 + src/reduce.c | 12 - src/rephase.c | 8 +- src/resize.c | 10 +- src/resolve.c | 25 +- src/resources.c | 8 +- src/restart.c | 12 +- src/search.c | 9 +- src/shrink.c | 4 +- src/statistics.c | 3 + src/statistics.h | 65 +- src/strengthen.c | 11 +- src/substitute.c | 2 +- src/sweep.c | 1540 +++++++++++++++----- src/terminate.h | 42 +- src/ternary.c | 4 +- src/trail.c | 24 +- src/trail.h | 1 - src/transitive.c | 2 +- src/utilities.h | 4 +- src/vector.c | 14 +- src/vivify.c | 97 +- src/walk.c | 12 +- src/warmup.c | 48 + src/warmup.h | 8 + src/watch.c | 24 + src/watch.h | 3 + src/xors.c | 8 +- test/cnf/miter1.cnf | 2495 ++++++++++++++++++++++++++++++++ test/cnf/strash1.cnf | 15 + test/cnf/strash2.cnf | 21 + test/cnf/strash3.cnf | 9 + test/testbump.c | 4 +- test/testcnfs.h | 2 + test/testconfig.c | 9 + 88 files changed, 5046 insertions(+), 1310 deletions(-) create mode 100644 NEWS.md create mode 100644 src/branching.c create mode 100644 src/branching.h rename src/{limits.c => kimits.c} (78%) rename src/{limits.h => kimits.h} (86%) delete mode 120000 src/makefile create mode 100644 src/propbeyond.c create mode 100644 src/propbeyond.h create mode 100644 src/warmup.c create mode 100644 src/warmup.h create mode 100644 test/cnf/miter1.cnf create mode 100644 test/cnf/strash1.cnf create mode 100644 test/cnf/strash2.cnf create mode 100644 test/cnf/strash3.cnf diff --git a/LICENSE b/LICENSE index d33afdaa..b0d7ce03 100644 --- a/LICENSE +++ b/LICENSE @@ -1,4 +1,5 @@ Copyright (c) 2019-2021 Armin Biere, Johannes Kepler University Linz, Austria +Copyright (c) 2021-2022 Armin Biere, University of Freiburg, Germany Permission is hereby granted, free of charge, to any person obtaining a copy of this software and associated documentation files (the "Software"), to deal diff --git a/NEWS.md b/NEWS.md new file mode 100644 index 00000000..4e472e73 --- /dev/null +++ b/NEWS.md @@ -0,0 +1,29 @@ +Version sc2022-bulky +-------------------- + +Compared to version 2.0.2 and thus the version submitted to the competition +in 2021 we added the following features: + + - added ACIDS branching variable heuristics (disabled by default) + - added CHB variable branching heuristic (but disabled by default) + inspired by the success of 'kissat_mab' in the SAT Competition 2021 + - faster randomization of phases in the Kitten sub-solver + - using literal flipping for faster refinement during sweeping + - literal flipping in a partial model obtained by Kitten + - disabled priority queue for variable elimination (elimination attempts + of variables in the given variable order is now enforced) + - disabled by default reusing the trail during restarts + - disabled by default hyper ternary resolution + - obtain initial local search assignment through propagation + (similar to the "warming-up" idea of Donald Knuth and how Shaowei Cai + for "ReasonLS" solvers initializes the local search) + - actual watch replacement of true literals during unit propagation instead + of just updating the blocking literal (as suggested by Norbert Manthey) + - fixed clause length and variable occurrences during variable elimination + instead of increasing the limits dynamically (but very rarely actually) + + +Version 2.0.2 +------------- + +- removed 'src/makefile' from git (set during configuration instead) diff --git a/README.md b/README.md index cf96c18a..7f029392 100644 --- a/README.md +++ b/README.md @@ -1,5 +1,5 @@ [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT) -[![Build Status](https://travis-ci.com/arminbiere/kissat.svg?branch=master)](https://travis-ci.com/arminbiere/kissat) +[![Build Status](https://app.travis-ci.com/github/arminbiere/kissat.svg?branch=master)](https://app.travis-ci.com/github/arminbiere/kissat) The Kissat SAT Solver ===================== diff --git a/VERSION b/VERSION index 38f77a65..8ff32b02 100644 --- a/VERSION +++ b/VERSION @@ -1 +1 @@ -2.0.1 +sc2022-bulky diff --git a/configure b/configure index da53bb86..eb7ff970 100755 --- a/configure +++ b/configure @@ -685,3 +685,12 @@ sed \ -e "s#@AR@#$AR#" \ -e "s#@GOALS@#$goals#" \ ../makefile.in > makefile + +if [ -f ../src/makefile ] +then + msg "removing src/makefile" + rm -f ../src/makefile +fi + +msg "linking src/makefile" +ln -s $ROOT/makefile ../src diff --git a/scripts/prepare-competition.sh b/scripts/prepare-competition.sh index 494aeaba..b2397a37 100755 --- a/scripts/prepare-competition.sh +++ b/scripts/prepare-competition.sh @@ -99,16 +99,13 @@ exec ./build.sh EOF chmod 755 $starexec_build -for config in default sat unsat -do - build=$dir/build/build.sh cat < $build #!/bin/sh tar xf ../archive/kissat* mv kissat* kissat cd kissat -./configure --competition --$config --test +./configure --competition --test make all || exit 1 build/tissat || exit 1 exec install -s build/kissat ../../bin/ @@ -118,22 +115,23 @@ chmod 755 $build starexec_run_default=$dir/bin/starexec_run_default cat <$starexec_run_default #!/bin/sh -exec ./kissat --$config \$1 \$2/proof.out +exec ./kissat \$1 \$2/proof.out EOF chmod 755 $starexec_run_default -msg "generated '$config' build and run scripts" +msg "generated build and run scripts" +version=`cat VERSION` description=$dir/starexec_description.txt cat <$description -Keep it Simple bare metal SAT solver with $config configuration +Keep it simple bare metal SAT Solver EOF msg "included the following description:" printf $BOLD cat $description printf $NORMAL -zipfile=/tmp/$base-$config.zip +zipfile=/tmp/$base.zip rm -f $zipfile cd $dir @@ -145,5 +143,3 @@ BYTES="`ls --block-size=1 -s $zipfile 2>/dev/null |awk '{print $1}'`" msg "zip file has $BYTES bytes" echo $zipfile - -done diff --git a/src/allocate.h b/src/allocate.h index 76be2c63..4d5fa2c8 100644 --- a/src/allocate.h +++ b/src/allocate.h @@ -15,6 +15,11 @@ void kissat_dealloc (struct kissat *, void *ptr, size_t n, size_t size); void *kissat_realloc (struct kissat *, void *, size_t old, size_t bytes); void *kissat_nrealloc (struct kissat *, void *, size_t o, size_t n, size_t); +#define NALLOC(P,N) \ +do { \ + (P) = kissat_nalloc (solver, (N), sizeof *(P)); \ +} while (0) + #define CALLOC(P,N) \ do { \ (P) = kissat_calloc (solver, (N), sizeof *(P)); \ diff --git a/src/analyze.c b/src/analyze.c index c3c7827d..55636d6d 100644 --- a/src/analyze.c +++ b/src/analyze.c @@ -177,6 +177,8 @@ analyze_reason_side_literal (kissat * solver, size_t limit, ward * arena, static void analyze_reason_side_literals (kissat * solver) { + if (!GET_OPTION (bump)) + return; if (!GET_OPTION (bumpreasons)) return; if (solver->probing) @@ -245,21 +247,6 @@ analyze_reason_side_literals (kissat * solver) solver->delays.bumpreasons.count); } -#if 0 - -#define RANK_LITERAL_BY_INVERSE_LEVEL(LIT) \ - (~assigned[IDX (LIT)].level) - -static void -sort_deduced_clause (kissat * solver) -{ - unsigneds *clause = &solver->clause; - assigned *assigned = solver->assigned; - RADIX_STACK (unsigned, unsigned, *clause, RANK_LITERAL_BY_INVERSE_LEVEL); -} - -#else - #define RADIX_SORT_LEVELS_LIMIT 32 #define RANK_LEVEL(A) (A) @@ -365,8 +352,6 @@ sort_deduced_clause (kissat * solver) #endif } -#endif - static void reset_levels (kissat * solver) { @@ -653,8 +638,8 @@ kissat_analyze (kissat * solver, clause * conflict) } if (!EMPTY_STACK (solver->analyzed)) { - if (!solver->probing) - kissat_bump (solver); + if (!solver->probing && GET_OPTION (bump)) + kissat_bump_analyzed (solver); kissat_reset_only_analyzed_literals (solver); } } diff --git a/src/ands.c b/src/ands.c index 43fa8592..0b4921a0 100644 --- a/src/ands.c +++ b/src/ands.c @@ -41,7 +41,7 @@ kissat_find_and_gate (kissat * solver, unsigned lit, unsigned negative) const value value = values[other]; if (value > 0) { - kissat_eliminate_clause (solver, c, INVALID_LIT); + kissat_mark_clause_as_garbage (solver, c); base = 0; break; } diff --git a/src/application.c b/src/application.c index 57b10752..ac433e98 100644 --- a/src/application.c +++ b/src/application.c @@ -14,6 +14,8 @@ #include #include +#define SOLVER_NAME "Kissat SAT Solver" + typedef struct application application; struct application @@ -261,7 +263,7 @@ parsed_one_option_and_return_zero_exit_code (char *arg) } if (!strcmp (arg, "--banner")) { - kissat_banner (0, "KISSAT SAT Solver"); + kissat_banner (0, SOLVER_NAME); return true; } if (!strcmp (arg, "--build")) @@ -271,7 +273,8 @@ parsed_one_option_and_return_zero_exit_code (char *arg) } if (!strcmp (arg, "--copyright")) { - printf ("%s\n", kissat_copyright ()); + for (const char **p = kissat_copyright (), *line; (line = *p); p++) + printf ("%s\n", line); return true; } if (!strcmp (arg, "--compiler")) @@ -841,7 +844,7 @@ print_limits (application * application) static int run_application (kissat * solver, - int argc, char **argv, bool * cancel_alarm_ptr) + int argc, char **argv, bool *cancel_alarm_ptr) { *cancel_alarm_ptr = false; if (argc == 2) @@ -858,7 +861,7 @@ run_application (kissat * solver, kissat_section (solver, "banner"); if (!GET_OPTION (quiet)) { - kissat_banner ("c ", "KISSAT SAT Solver"); + kissat_banner ("c ", SOLVER_NAME); fflush (stdout); } #endif diff --git a/src/backbone.c b/src/backbone.c index 7138180f..916a2aa1 100644 --- a/src/backbone.c +++ b/src/backbone.c @@ -396,7 +396,7 @@ compute_backbone (kissat * solver) unsigned inconsistent = INVALID_LIT; SET_EFFORT_LIMIT (ticks_limit, backbone, backbone_ticks, - kissat_linear (1 + solver->active)); + 1 + solver->active); size_t round_limit = GET_OPTION (backbonerounds); assert (solver->statistics.backbone_computations); diff --git a/src/backtrack.c b/src/backtrack.c index 993ccf9b..46367aff 100644 --- a/src/backtrack.c +++ b/src/backtrack.c @@ -99,7 +99,7 @@ kissat_backtrack_without_updating_phases (kissat * solver, unsigned new_level) unsigned *q = new_end; if (solver->stable) { - heap *scores = &solver->scores; + heap *scores = SCORES; for (const unsigned *p = q; p != old_end; p++) { const unsigned lit = *p; @@ -182,16 +182,12 @@ kissat_backtrack_after_conflict (kissat * solver, unsigned new_level) kissat_backtrack_without_updating_phases (solver, new_level); } -// TODO check whether this can be merged with -// 'kissat_restart_and_flush_trail'. - void kissat_backtrack_propagate_and_flush_trail (kissat * solver) { if (solver->level) { assert (solver->watching); - assert (solver->level > 0); kissat_backtrack_in_consistent_state (solver, 0); #ifndef NDEBUG clause *conflict = diff --git a/src/backward.c b/src/backward.c index 6d0eeed0..5b503492 100644 --- a/src/backward.c +++ b/src/backward.c @@ -29,7 +29,7 @@ backward_subsume_lits (kissat * solver, reference ignore, assert (min_lit != INVALID_LIT); - const unsigned occlim = solver->bounds.subsume.occurrences; + const unsigned occlim = GET_OPTION (subsumeocclim); if (min_occs > occlim) return true; @@ -40,7 +40,7 @@ backward_subsume_lits (kissat * solver, reference ignore, const value *const values = solver->values; ward *const arena = BEGIN_STACK (solver->arena); - const unsigned clslim = solver->bounds.subsume.clause_size; + const unsigned clslim = GET_OPTION (subsumeclslim); const unsigned match = (size > 2 ? INVALID_LIT : (lits[0] ^ lits[1] ^ min_lit)); @@ -90,7 +90,6 @@ backward_subsume_lits (kissat * solver, reference ignore, INC (duplicated); kissat_disconnect_binary (solver, other, min_lit); kissat_delete_binary (solver, false, false, min_lit, other); - kissat_update_after_removing_variable (solver, IDX (other)); q--; } else @@ -136,8 +135,6 @@ backward_subsume_lits (kissat * solver, reference ignore, { LOGCLS (c, "satisfied by %s", LOGLIT (lit)); kissat_mark_clause_as_garbage (solver, c); - kissat_update_after_removing_clause (solver, c, - INVALID_LIT); break; } if (value < 0) @@ -180,7 +177,6 @@ backward_subsume_lits (kissat * solver, reference ignore, INC (subsumed); INC (backward_subsumed); kissat_mark_clause_as_garbage (solver, c); - kissat_update_after_removing_clause (solver, c, INVALID_LIT); q--; continue; } @@ -206,7 +202,6 @@ backward_subsume_lits (kissat * solver, reference ignore, if (satisfied) { kissat_mark_clause_as_garbage (solver, c); - kissat_update_after_removing_clause (solver, c, INVALID_LIT); q--; continue; } @@ -272,7 +267,6 @@ backward_subsume_lits (kissat * solver, reference ignore, q--; } kissat_mark_removed_literal (solver, remove); - kissat_update_after_removing_variable (solver, IDX (remove)); } } diff --git a/src/bits.h b/src/bits.h index a1cea475..2be3bbf8 100644 --- a/src/bits.h +++ b/src/bits.h @@ -16,7 +16,7 @@ static inline size_t kissat_bits_size_in_words (size_t size) { assert (sizeof (bits) == 4); - return (size >> 5) + ! !(size & 31); + return (size >> 5) + !!(size & 31); } static inline bool @@ -29,7 +29,7 @@ kissat_get_bit (const bits * bits, size_t size, size_t bit) const unsigned y = (bit & 31); const unsigned mask = (1u << y); const unsigned masked = word & mask; - const bool res = ! !masked; + const bool res = !!masked; (void) size; return res; } diff --git a/src/branching.c b/src/branching.c new file mode 100644 index 00000000..e6498a60 --- /dev/null +++ b/src/branching.c @@ -0,0 +1,56 @@ +#include "internal.h" +#include "print.h" + +#ifndef QUIET + +static const char * +branching_name (kissat * solver, unsigned branching) +{ +#ifdef NOPTIONS + (void) solver; +#endif + return branching ? "CHB" : GET_OPTION (acids) ? "ACIDS" : "VSIDS"; +} + +#endif + +void +kissat_init_branching (kissat * solver) +{ + if (!GET_OPTION (bump)) + return; + + solver->branching = GET_OPTION (chb) == 2; + kissat_very_verbose (solver, + "will start with %s branching heuristics", + branching_name (solver, solver->branching)); + + if (GET_OPTION (chb)) + { + const int emachb = GET_OPTION (emachb); + solver->alphachb = 1.0 / emachb; + kissat_very_verbose (solver, "CHB branching alpha %g (window %d)", + solver->alphachb, emachb); + } +} + +bool +kissat_toggle_branching (kissat * solver) +{ + assert (solver->stable); + if (!GET_OPTION (bump)) + return false; + if (GET_OPTION (chb) != 1) + return false; +#ifndef QUIET + const unsigned current = solver->branching; + const unsigned next = solver->branching = !current; + kissat_extremely_verbose (solver, + "switching from %s branching heuristic to %s", + branching_name (solver, current), + branching_name (solver, next)); +#else + (void) solver; +#endif + return true; +} diff --git a/src/branching.h b/src/branching.h new file mode 100644 index 00000000..bde64e18 --- /dev/null +++ b/src/branching.h @@ -0,0 +1,11 @@ +#ifndef _branching_h_INCLUDED +#define _branching_h_INCLUDED + +#include + +struct kissat; + +void kissat_init_branching (struct kissat *); +bool kissat_toggle_branching (struct kissat *); + +#endif diff --git a/src/build.c b/src/build.c index 5fdd99a2..1f4153b6 100644 --- a/src/build.c +++ b/src/build.c @@ -23,10 +23,16 @@ kissat_compiler (void) return COMPILER; } -const char * +static const char *copyright_lines[] = { + "Copyright (c) 2021-2022 Armin Biere University of Freiburg", + "Copyright (c) 2019-2021 Armin Biere Johannes Kepler University Linz", + 0 +}; + +const char ** kissat_copyright (void) { - return "Copyright (c) 2019-2021 Armin Biere JKU Linz"; + return copyright_lines; } const char * @@ -83,9 +89,15 @@ kissat_banner (const char *prefix, const char *name) NL (); PREFIX (BOLD MAGENTA); - fputs (kissat_copyright (), stdout); NL (); + for (const char **p = kissat_copyright (), *line; (line = *p); p++) + { + PREFIX (BOLD MAGENTA); + fputs (line, stdout); + NL (); + } + if (prefix) { PREFIX (""); diff --git a/src/bump.c b/src/bump.c index bf8f4ebf..41d0f9de 100644 --- a/src/bump.c +++ b/src/bump.c @@ -30,9 +30,11 @@ sort_bump (kissat * solver) } static void -rescale_scores (kissat * solver, heap * scores) +rescale_scores (kissat * solver) { INC (rescaled); + assert (!solver->branching); + heap *scores = &solver->scores[0]; const double max_score = kissat_max_score_on_heap (scores); kissat_phase (solver, "rescale", GET (rescaled), "maximum score %g increment %g", max_score, solver->scinc); @@ -46,7 +48,7 @@ rescale_scores (kissat * solver, heap * scores) } static void -bump_score_increment (kissat * solver, heap * scores) +bump_score_increment (kissat * solver) { const double old_scinc = solver->scinc; const double decay = GET_OPTION (decay) * 1e-3; @@ -56,32 +58,36 @@ bump_score_increment (kissat * solver, heap * scores) LOG ("new score increment %g = %g * %g", new_scinc, factor, old_scinc); solver->scinc = new_scinc; if (new_scinc > MAX_SCORE) - rescale_scores (solver, scores); + rescale_scores (solver); } static inline void -bump_variable_score (kissat * solver, heap * scores, unsigned idx) +bump_analyzed_variable_score (kissat * solver, unsigned idx) { + assert (!solver->branching); + heap *scores = &solver->scores[0]; const double old_score = kissat_get_heap_score (scores, idx); - const double new_score = old_score + solver->scinc; - LOG ("new score[%u] = %g = %g + %g", - idx, new_score, old_score, solver->scinc); + const double inc = GET_OPTION (acids) ? + (CONFLICTS - old_score) / 2.0 : solver->scinc; + const double new_score = old_score + inc; + LOG ("new score[%u] = %g = %g + %g", idx, new_score, old_score, inc); kissat_update_heap (solver, scores, idx, new_score); if (new_score > MAX_SCORE) - rescale_scores (solver, scores); + rescale_scores (solver); } static void bump_analyzed_variable_scores (kissat * solver) { - heap *scores = &solver->scores; + assert (!solver->branching); flags *flags = solver->flags; for (all_stack (unsigned, idx, solver->analyzed)) if (flags[idx].active) - bump_variable_score (solver, scores, idx); + bump_analyzed_variable_score (solver, idx); - bump_score_increment (solver, scores); + if (!GET_OPTION (acids)) + bump_score_increment (solver); } static void @@ -109,15 +115,81 @@ move_analyzed_variables_to_front_of_queue (kissat * solver) CLEAR_STACK (solver->ranks); } +static void +update_conflicted (kissat * solver) +{ + const uint64_t conflicts = CONFLICTS; + flags *flags = solver->flags; + + for (all_stack (unsigned, idx, solver->analyzed)) + if (flags[idx].active) + solver->conflicted[idx] = conflicts; +} + void -kissat_bump (kissat * solver) +kissat_bump_analyzed (kissat * solver) { START (bump); const size_t bumped = SIZE_STACK (solver->analyzed); - if (solver->stable) - bump_analyzed_variable_scores (solver); - else + if (!solver->stable) move_analyzed_variables_to_front_of_queue (solver); + else if (solver->branching) + update_conflicted (solver); + else + bump_analyzed_variable_scores (solver); ADD (literals_bumped, bumped); STOP (bump); } + +void +kissat_bump_propagated (kissat * solver) +{ + assert (solver->branching); + assert (GET_OPTION (bump)); + + const unsigned level = solver->level; + if (!level) + return; + + assert (!solver->probing); + + const uint64_t conflicts = CONFLICTS; + const double alpha = solver->alphachb; + + const uint64_t *conflicted = solver->conflicted; + const struct assigned *assigned = solver->assigned; + assert (solver->branching); + heap *scores = &solver->scores[1]; + + const unsigned *begin = BEGIN_STACK (solver->trail); + const unsigned *end = END_STACK (solver->trail); + const unsigned *t = end; + + while (t > begin) + { + const unsigned lit = *--t; + const unsigned idx = IDX (lit); + + if (assigned[idx].level != level) + break; + + const uint64_t last = conflicted[idx]; + const uint64_t diff = last ? (conflicts - last) : 0; // UINT_MAX; + const uint64_t age = (diff == UINT64_MAX ? UINT64_MAX : diff + 1); + const double reward = 1.0 / age; + const double old_score = kissat_get_heap_score (scores, idx); + const double new_score = alpha * reward + (1 - alpha) * old_score; + LOG ("new score[%u] = %g vs %g", idx, new_score, old_score); + kissat_update_heap (solver, scores, idx, new_score); + } +} + +void +kissat_update_scores (kissat * solver) +{ + assert (solver->stable); + heap *scores = SCORES; + for (all_variables (idx)) + if (ACTIVE (idx) && !kissat_heap_contains (scores, idx)) + kissat_push_heap (solver, scores, idx); +} diff --git a/src/bump.h b/src/bump.h index 697366eb..718a3c40 100644 --- a/src/bump.h +++ b/src/bump.h @@ -5,7 +5,9 @@ struct kissat; -void kissat_bump (struct kissat *); +void kissat_bump_analyzed (struct kissat *); +void kissat_bump_propagated (struct kissat *); +void kissat_update_scores (struct kissat *); #define MAX_SCORE 1e150 diff --git a/src/colors.h b/src/colors.h index f395e0db..d2edcc36 100644 --- a/src/colors.h +++ b/src/colors.h @@ -15,8 +15,8 @@ #define WHITE "\037[34m" #define YELLOW "\033[33m" -#define LIGHT_GRAY "\033[0;37m" -#define DARK_GRAY "\033[1;30m" +#define LIGHT_GRAY "\033[1;37m" +#define DARK_GRAY "\033[0;37m" #ifdef _POSIX_C_SOURCE #define assert_if_posix assert diff --git a/src/compact.c b/src/compact.c index e21b725f..22d8fe41 100644 --- a/src/compact.c +++ b/src/compact.c @@ -131,6 +131,8 @@ compact_literal (kissat * solver, unsigned dst_lit, unsigned src_lit) solver->values[dst_lit] = solver->values[src_lit]; solver->values[not_dst_lit] = solver->values[not_src_lit]; + solver->conflicted[dst_idx] = solver->conflicted[src_idx]; + cache *cache = &solver->cache; if (cache->valid) { @@ -200,7 +202,24 @@ compact_queue (kissat * solver) } static void -compact_scores (kissat * solver, unsigned vars) +compact_sweep (kissat * solver) +{ + unsigned *q = BEGIN_STACK (solver->sweep); + const unsigned *const end = END_STACK (solver->sweep); + for (const unsigned *p = q; p != end; p++) + { + const unsigned idx = *p; + const unsigned midx = map_idx (solver, idx); + if (midx == INVALID_IDX) + continue; + *q++ = midx; + } + SET_END_OF_STACK (solver->sweep, q); + SHRINK_STACK (solver->sweep); +} + +static void +compact_scores (kissat * solver, heap * old_scores, unsigned vars) { LOG ("compacting scores"); @@ -208,8 +227,6 @@ compact_scores (kissat * solver, unsigned vars) memset (&new_scores, 0, sizeof new_scores); kissat_resize_heap (solver, &new_scores, vars); - heap *old_scores = &solver->scores; - if (old_scores->tainted) { LOG ("copying scores of tainted old scores heap"); @@ -235,7 +252,7 @@ compact_scores (kissat * solver, unsigned vars) } kissat_release_heap (solver, old_scores); - solver->scores = new_scores; + *old_scores = new_scores; } static void @@ -452,13 +469,16 @@ kissat_finalize_compacting (kissat * solver, unsigned vars, unsigned mfixed) compact_units (solver, mfixed); memset (solver->assigned + vars, 0, reduced * sizeof (assigned)); + memset (solver->conflicted + vars, 0, reduced * sizeof (uint64_t)); memset (solver->flags + vars, 0, reduced * sizeof (flags)); memset (solver->values + 2 * vars, 0, 2 * reduced * sizeof (value)); memset (solver->watches + 2 * vars, 0, 2 * reduced * sizeof (watches)); compact_queue (solver); + compact_sweep (solver); compact_cache (solver, vars); - compact_scores (solver, vars); + for (all_scores (scores)) + compact_scores (solver, scores, vars); compact_frames (solver); compact_export (solver, vars); compact_best_and_target_values (solver, vars); diff --git a/src/config.h b/src/config.h index cd8f6727..16eac8c0 100644 --- a/src/config.h +++ b/src/config.h @@ -2,13 +2,6 @@ #ifndef _config_h_INCLUDED #define _config_h_INCLUDED -#define CONFIGURATIONS \ -CONFIGURATION (default) \ -CONFIGURATION (sat) \ -CONFIGURATION (unsat) \ - -struct kissat; - void kissat_configuration_usage (void); #endif diff --git a/src/decide.c b/src/decide.c index df5a5ee2..99714075 100644 --- a/src/decide.c +++ b/src/decide.c @@ -36,15 +36,16 @@ last_enqueued_unassigned_variable (kissat * solver) static unsigned largest_score_unassigned_variable (kissat * solver) { - unsigned res = kissat_max_heap (&solver->scores); + heap *scores = SCORES; + unsigned res = kissat_max_heap (scores); const value *const values = solver->values; while (values[LIT (res)]) { - kissat_pop_max_heap (solver, &solver->scores); - res = kissat_max_heap (&solver->scores); + kissat_pop_max_heap (solver, scores); + res = kissat_max_heap (scores); } #if defined(LOGGING) || defined(CHECK_HEAP) - const double score = kissat_get_heap_score (&solver->scores, res); + const double score = kissat_get_heap_score (scores, res); #endif LOG ("largest score unassigned %s score %g", LOGVAR (res), score); #ifdef CHECK_HEAP @@ -54,7 +55,7 @@ largest_score_unassigned_variable (kissat * solver) continue; if (VALUE (LIT (idx))) continue; - const double idx_score = kissat_get_heap_score (&solver->scores, idx); + const double idx_score = kissat_get_heap_score (scores, idx); assert (score >= idx_score); } #endif diff --git a/src/deduce.c b/src/deduce.c index aeb2f4da..0adcbdb4 100644 --- a/src/deduce.c +++ b/src/deduce.c @@ -15,8 +15,9 @@ mark_clause_as_used (kissat * solver, clause * c) c->used = 1; if (c->hyper) return; - const unsigned new_glue = kissat_recompute_glue (solver, c); - if (new_glue < c->glue) + const unsigned old_glue = c->glue; + const unsigned new_glue = kissat_recompute_glue (solver, c, old_glue); + if (new_glue < old_glue) kissat_promote_clause (solver, c, new_glue); else if (used && c->glue <= (unsigned) GET_OPTION (tier2)) c->used = 2; diff --git a/src/definition.c b/src/definition.c index 045c5228..89a75aed 100644 --- a/src/definition.c +++ b/src/definition.c @@ -148,10 +148,11 @@ kissat_find_definition (kissat * solver, unsigned lit) LOG ("exported %u = %zu + %zu environment clauses to sub-solver", exported, occs[0], occs[1]); INC (definitions_checked); + const size_t limit = GET_OPTION (definitionticks); + kitten_set_ticks_limit (kitten, limit); int status = kitten_solve (kitten); if (status == 20) { - INC (definitions_extracted); LOG ("sub-solver result UNSAT shows definition exists"); uint64_t learned; unsigned reduced = kitten_compute_clausal_core (kitten, &learned); @@ -161,11 +162,14 @@ kissat_find_definition (kissat * solver, unsigned lit) { kitten_shrink_to_clausal_core (kitten); kitten_shuffle_clauses (kitten); -#ifndef NDEBUG - int tmp = -#endif - kitten_solve (kitten); - assert (tmp == 20); + kitten_set_ticks_limit (kitten, 10 * limit); + int tmp = kitten_solve (kitten); + assert (!tmp || tmp == 20); + if (!tmp) + { + LOG ("aborting core extraction"); + goto ABORT; + } #ifndef NDEBUG unsigned previous = reduced; #endif @@ -177,6 +181,7 @@ kissat_find_definition (kissat * solver, unsigned lit) (void) reduced; #endif } + INC (definitions_extracted); kitten_traverse_core_ids (kitten, &extractor, traverse_definition_core); size_t size[2]; size[0] = SIZE_STACK (solver->gates[0]); @@ -245,7 +250,10 @@ kissat_find_definition (kissat * solver, unsigned lit) res = true; } else - LOG ("sub-solver failed to show that definition exists"); + { + ABORT: + LOG ("sub-solver failed to show that definition exists"); + } CLEAR_STACK (solver->analyzed); STOP (definition); return res; diff --git a/src/dump.c b/src/dump.c index 1488175f..6b1eab6c 100644 --- a/src/dump.c +++ b/src/dump.c @@ -147,7 +147,7 @@ dump_queue (kissat * solver) static void dump_scores (kissat * solver) { - heap *heap = &solver->scores; + heap *heap = SCORES; printf ("scores.vars = %u\n", heap->vars); printf ("scores.size = %u\n", heap->size); for (unsigned i = 0; i < SIZE_STACK (heap->stack); i++) @@ -285,7 +285,6 @@ dump_binaries (kissat * solver) const unsigned other = watch.binary.lit; if (lit > other) continue; - COVER (watch.binary.redundant); if (watch.binary.redundant) printf ("redundant "); else @@ -344,8 +343,12 @@ dump (kissat * solver) dump_etrail (solver); dump_extend (solver); dump_trail (solver); + printf ("stable = %u\n", (unsigned) solver->stable); if (solver->stable) - dump_scores (solver); + { + printf ("branching = %u\n", solver->branching); + dump_scores (solver); + } else dump_queue (solver); dump_values (solver); diff --git a/src/eliminate.c b/src/eliminate.c index 39f6d27e..287c9cc5 100644 --- a/src/eliminate.c +++ b/src/eliminate.c @@ -22,7 +22,7 @@ static uint64_t eliminate_adjustment (kissat * solver) { - return 2 * CLAUSES + kissat_nlogn (1 + solver->active); + return 2 * CLAUSES + NLOGN (1 + solver->active); } static bool @@ -57,123 +57,11 @@ kissat_eliminating (kissat * solver) return false; } -static inline void -update_after_adding_variable (kissat * solver, heap * schedule, unsigned idx) -{ - if (!GET_OPTION (eliminateheap)) - return; - assert (schedule->size); - kissat_update_variable_score (solver, schedule, idx); -} - -static inline void -update_after_adding_stack (kissat * solver, unsigneds * stack) -{ - if (!GET_OPTION (eliminateheap)) - return; - assert (!solver->probing); - heap *schedule = &solver->schedule; - if (!schedule->size) - return; - for (all_stack (unsigned, lit, *stack)) - update_after_adding_variable (solver, schedule, IDX (lit)); -} - -static inline void -update_after_removing_variable (kissat * solver, unsigned idx) -{ - if (!GET_OPTION (eliminateheap)) - return; - assert (!solver->probing); - flags *f = solver->flags + idx; - if (f->fixed) - return; - assert (!f->eliminated); - heap *schedule = &solver->schedule; - if (!schedule->size) - return; - kissat_update_variable_score (solver, schedule, idx); - if (!kissat_heap_contains (schedule, idx)) - kissat_push_heap (solver, schedule, idx); -} - -void -kissat_update_after_removing_variable (kissat * solver, unsigned idx) -{ - update_after_removing_variable (solver, idx); -} - -static inline void -update_after_removing_clause (kissat * solver, clause * c, unsigned except) -{ - if (!GET_OPTION (eliminateheap)) - return; - assert (c->garbage); - for (all_literals_in_clause (lit, c)) - if (lit != except) - update_after_removing_variable (solver, IDX (lit)); -} - -void -kissat_update_after_removing_clause (kissat * solver, - clause * c, unsigned except) -{ - update_after_removing_clause (solver, c, except); -} - void kissat_eliminate_binary (kissat * solver, unsigned lit, unsigned other) { kissat_disconnect_binary (solver, other, lit); kissat_delete_binary (solver, false, false, lit, other); - update_after_removing_variable (solver, IDX (other)); -} - -void -kissat_eliminate_clause (kissat * solver, clause * c, unsigned lit) -{ - kissat_mark_clause_as_garbage (solver, c); - update_after_removing_clause (solver, c, lit); -} - -static unsigned -schedule_variables (kissat * solver) -{ - const bool eliminateheap = GET_OPTION (eliminateheap); - - LOG ("initializing variable schedule"); - assert (!solver->schedule.size); - - if (eliminateheap) - kissat_resize_heap (solver, &solver->schedule, solver->vars); - - flags *all_flags = solver->flags; - - size_t scheduled = 0; - - for (all_variables (idx)) - { - flags *flags = all_flags + idx; - if (!flags->active) - continue; - if (!flags->eliminate) - continue; - LOG ("scheduling %s", LOGVAR (idx)); - scheduled++; - if (eliminateheap) - update_after_removing_variable (solver, idx); - } -#ifndef NDEBUG - if (eliminateheap) - assert (scheduled == kissat_size_heap (&solver->schedule)); -#endif -#ifndef QUIET - size_t active = solver->active; - kissat_phase (solver, "eliminate", GET (eliminations), - "scheduled %zu variables %.0f%%", - scheduled, kissat_percent (scheduled, active)); -#endif - return scheduled; } void @@ -191,13 +79,11 @@ kissat_flush_units_while_connected (kissat * solver) if (!kissat_dense_propagate (solver)) return; LOG ("marking and flushing unit satisfied clauses"); - const value *const values = solver->values; end_trail = END_ARRAY (solver->trail); while (propagate != end_trail) { const unsigned unit = *propagate++; - assert (values[unit] > 0); watches *unit_watches = &WATCHES (unit); watch *begin = BEGIN_WATCHES (*unit_watches), *q = begin; const watch *const end = END_WATCHES (*unit_watches), *p = q; @@ -208,20 +94,13 @@ kissat_flush_units_while_connected (kissat * solver) { const watch watch = *q++ = *p++; if (watch.type.binary) - { - const unsigned other = watch.binary.lit; - if (!values[other]) - update_after_removing_variable (solver, IDX (other)); - } - else - { - const reference ref = watch.large.ref; - clause *c = kissat_dereference_clause (solver, ref); - if (!c->garbage) - kissat_eliminate_clause (solver, c, unit); - assert (c->garbage); - q--; - } + continue; + const reference ref = watch.large.ref; + clause *c = kissat_dereference_clause (solver, ref); + if (!c->garbage) + kissat_mark_clause_as_garbage (solver, c); + assert (c->garbage); + q--; } assert (q <= end); size_t flushed = end - q; @@ -238,44 +117,47 @@ connect_resolvents (kissat * solver) bool backward = GET_OPTION (backward); const value *const values = solver->values; assert (EMPTY_STACK (solver->clause)); - uint64_t added = 0; bool satisfied = false; + uint64_t added = 0; for (all_stack (unsigned, other, solver->resolvents)) { if (other == INVALID_LIT) { if (satisfied) satisfied = false; - else if (kissat_forward_subsume_temporary (solver)) - LOGTMP ("temporary forward subsumed"); else { - size_t size = SIZE_STACK (solver->clause); - if (!size) - { - assert (!solver->inconsistent); - LOG ("resolved empty clause"); - CHECK_AND_ADD_EMPTY (); - ADD_EMPTY_TO_PROOF (); - solver->inconsistent = true; - break; - } - else if (size == 1) - { - const unsigned unit = PEEK_STACK (solver->clause, 0); - LOG ("resolved unit clause %s", LOGLIT (unit)); - kissat_learned_unit (solver, unit); - } + LOGTMP ("temporary resolvent"); + if (kissat_forward_subsume_temporary (solver)) + LOGTMP ("temporary forward subsumed"); else { - assert (size > 1); - reference ref = kissat_new_irredundant_clause (solver); - update_after_adding_stack (solver, &solver->clause); - added++; - - if (backward) - backward = - kissat_backward_subsume_temporary (solver, ref); + const size_t size = SIZE_STACK (solver->clause); + if (!size) + { + assert (!solver->inconsistent); + LOG ("resolved empty clause"); + CHECK_AND_ADD_EMPTY (); + ADD_EMPTY_TO_PROOF (); + solver->inconsistent = true; + break; + } + else if (size == 1) + { + const unsigned unit = PEEK_STACK (solver->clause, 0); + LOG ("resolved unit clause %s", LOGLIT (unit)); + kissat_learned_unit (solver, unit); + } + else + { + assert (size > 1); + reference ref = kissat_new_irredundant_clause (solver); + added++; + + if (backward) + backward = + kissat_backward_subsume_temporary (solver, ref); + } } } CLEAR_STACK (solver->clause); @@ -337,7 +219,7 @@ weaken_clauses (kissat * solver, unsigned lit) if (!satisfied) kissat_weaken_clause (solver, lit, c); LOGCLS (c, "removing %s", LOGLIT (lit)); - kissat_eliminate_clause (solver, c, lit); + kissat_mark_clause_as_garbage (solver, c); } } RELEASE_WATCHES (*pos_watches); @@ -374,7 +256,7 @@ weaken_clauses (kissat * solver, unsigned lit) if (!optimize && !satisfied) kissat_weaken_clause (solver, not_lit, d); LOGCLS (d, "removing %s", LOGLIT (not_lit)); - kissat_eliminate_clause (solver, d, not_lit); + kissat_mark_clause_as_garbage (solver, d); } } if (optimize && !EMPTY_WATCHES (*neg_watches)) @@ -447,20 +329,20 @@ can_eliminate_variable (kissat * solver, unsigned idx) if (!flags->eliminate) return false; - LOG ("next elimination candidate %s", LOGVAR (idx)); - - LOG ("marking %s as not removed", LOGVAR (idx)); - flags->eliminate = false; - return true; } static bool eliminate_variable (kissat * solver, unsigned idx) { + LOG ("next elimination candidate %s", LOGVAR (idx)); + assert (!solver->inconsistent); - if (!can_eliminate_variable (solver, idx)) - return false; + assert (can_eliminate_variable (solver, idx)); + + LOG ("marking %s as not removed", LOGVAR (idx)); + FLAGS (idx)->eliminate = false; + unsigned lit; if (!kissat_generate_resolvents (solver, idx, &lit)) return false; @@ -486,10 +368,10 @@ eliminate_variables (kissat * solver) kissat_very_verbose (solver, "trying to eliminate variables with bound %u", solver->bounds.eliminate.additional_clauses); + assert (!solver->inconsistent); #ifndef QUIET - unsigned active_before = solver->active; + unsigned before = solver->active; #endif - unsigned last_round_eliminated; unsigned eliminated = 0; uint64_t tried = 0; @@ -497,7 +379,13 @@ eliminate_variables (kissat * solver) eliminate, eliminate_resolutions, eliminate_adjustment (solver)); - bool forward_subsumption_complete = false; + solver->budget.forward = + 1 * (resolution_limit - solver->statistics.eliminate_resolutions); + kissat_extremely_verbose (solver, + "temporary forward subsumption budget set to %s", + FORMAT_COUNT (solver->budget.forward)); + + bool complete; int round = 0; const bool forward = GET_OPTION (forward); @@ -505,16 +393,12 @@ eliminate_variables (kissat * solver) for (;;) { round++; - last_round_eliminated = 0; - forward_subsumption_complete = true; LOG ("starting new elimination round %d", round); - kissat_release_heap (solver, &solver->schedule); if (forward) { unsigned *propagate = solver->propagate; - forward_subsumption_complete = - kissat_forward_subsume_during_elimination (solver); + complete = kissat_forward_subsume_during_elimination (solver); if (solver->inconsistent) break; kissat_flush_large_connected (solver); @@ -525,76 +409,64 @@ eliminate_variables (kissat * solver) break; } else - kissat_connect_irredundant_large_clauses (solver); - - const unsigned last_round_scheduled = schedule_variables (solver); - kissat_very_verbose (solver, - "scheduled %u variables %.0f%% to eliminate " - "in round %d", last_round_scheduled, - kissat_percent (last_round_scheduled, - solver->active), round); - - if (forward_subsumption_complete && !last_round_scheduled) - break; + { + kissat_connect_irredundant_large_clauses (solver); + complete = true; + } - const bool eliminateheap = GET_OPTION (eliminateheap); - unsigned idx = 0; - bool done = false; + unsigned successful = 0; - while (!done && !solver->inconsistent) + for (unsigned idx = 0; idx != solver->vars; idx++) { - if (eliminateheap && kissat_empty_heap (&solver->schedule)) - done = true; - else if (!eliminateheap && idx == solver->vars) - done = true; - else if (TERMINATED (eliminate_terminated_1)) - done = true; - else if (solver->statistics.eliminate_resolutions > - resolution_limit) + if (TERMINATED (eliminate_terminated_1)) + { + complete = false; + break; + } + if (!can_eliminate_variable (solver, idx)) + continue; + if (solver->statistics.eliminate_resolutions > resolution_limit) { kissat_extremely_verbose (solver, "eliminate round %u hits " "resolution limit %" PRIu64 " at %" PRIu64 " resolutions", round, resolution_limit, - solver->statistics. - eliminate_resolutions); - done = true; - } - else - { - tried++; - if (eliminateheap) - idx = kissat_pop_max_heap (solver, &solver->schedule); - if (eliminate_variable (solver, idx)) - eliminated++, last_round_eliminated++; - if (!solver->inconsistent) - kissat_flush_units_while_connected (solver); - if (!eliminateheap) - idx++; + solver-> + statistics.eliminate_resolutions); + complete = false; + break; } + tried++; + if (eliminate_variable (solver, idx)) + successful++; + if (solver->inconsistent) + break; + kissat_flush_units_while_connected (solver); + if (solver->inconsistent) + break; + } + + if (successful) + { + complete = false; + eliminated += successful; } + if (!solver->inconsistent) { kissat_flush_large_connected (solver); kissat_dense_collect (solver); } + kissat_phase (solver, "eliminate", GET (eliminations), - "eliminated %u variables %.0f%% in round %u", - last_round_eliminated, - kissat_percent (last_round_eliminated, - last_round_scheduled), round); -#ifndef QUIET - { - const bool round_successful = - solver->inconsistent || last_round_eliminated; - REPORT (!round_successful, 'e'); - } -#endif + "eliminated %u variables in round %u", successful, round); + REPORT (!successful, 'e'); + if (solver->inconsistent) break; - if (eliminateheap) - kissat_release_heap (solver, &solver->schedule); + if (complete) + break; if (round == GET_OPTION (eliminaterounds)) break; if (solver->statistics.eliminate_resolutions > resolution_limit) @@ -603,77 +475,17 @@ eliminate_variables (kissat * solver) break; } - const unsigned remain = kissat_size_heap (&solver->schedule); - kissat_release_heap (solver, &solver->schedule); #ifndef QUIET kissat_very_verbose (solver, - "eliminated %u variables %.0f%% of %" PRIu64 " tried" - " (%u remain %.0f%%)", - eliminated, kissat_percent (eliminated, tried), tried, - remain, kissat_percent (remain, solver->active)); + "eliminated %u variables %.0f%% of %" PRIu64 " tried", + eliminated, kissat_percent (eliminated, tried), tried); kissat_phase (solver, "eliminate", GET (eliminations), "eliminated %u variables %.0f%% out of %u in %d rounds", - eliminated, kissat_percent (eliminated, active_before), - active_before, round); + eliminated, kissat_percent (eliminated, before), + before, round); #endif if (!solver->inconsistent) - { - const bool complete = - !remain && !last_round_eliminated && forward_subsumption_complete; - set_next_elimination_bound (solver, complete); - if (!complete && !GET_OPTION (eliminatekeep)) - { - const flags *end = solver->flags + VARS; -#ifndef QUIET - unsigned dropped = 0; -#endif - for (struct flags * f = solver->flags; f != end; f++) - if (f->eliminate) - { - f->eliminate = false; -#ifndef QUIET - dropped++; -#endif - } - - kissat_very_verbose (solver, - "dropping %u eliminate candidates", dropped); - } - } -} - -static void -setup_elim_bounds (kissat * solver) -{ - solver->bounds.eliminate.clause_size = - SCALE_LIMIT (eliminations, eliminateclslim); - - solver->bounds.eliminate.occurrences = - SCALE_LIMIT (eliminations, eliminateocclim); - - kissat_phase (solver, "eliminate", GET (eliminations), - "occurrence limit %u and clause limit %u", - solver->bounds.eliminate.occurrences, - solver->bounds.eliminate.clause_size); - - solver->bounds.subsume.clause_size = - SCALE_LIMIT (eliminations, subsumeclslim); - - solver->bounds.subsume.occurrences = - SCALE_LIMIT (eliminations, subsumeocclim); - - kissat_phase (solver, "subsume", GET (eliminations), - "occurrence limit %u clause limit %u", - solver->bounds.subsume.occurrences, - solver->bounds.subsume.clause_size); - - solver->bounds.xor.clause_size = - log (MAX (solver->bounds.eliminate.occurrences, 1)) / log (2.0) + 0.5; - if (solver->bounds.xor.clause_size > (unsigned) GET_OPTION (xorsclslim)) - solver->bounds.xor.clause_size = (unsigned) GET_OPTION (xorsclslim); - assert (solver->bounds.xor.clause_size < 32); - - LOG ("maximum XOR base clause size %u", solver->bounds.xor.clause_size); + set_next_elimination_bound (solver, complete); } static void @@ -706,7 +518,6 @@ eliminate (kissat * solver) "elimination limit of %" PRIu64 " conflicts hit", solver->limits.eliminate.conflicts); const changes before = kissat_changes (solver); - setup_elim_bounds (solver); init_map_and_kitten (solver); litwatches saved; INIT_STACK (saved); @@ -728,7 +539,7 @@ kissat_eliminate (kissat * solver) assert (!solver->inconsistent); INC (eliminations); eliminate (solver); - UPDATE_CONFLICT_LIMIT (eliminate, eliminations, NLOGNLOGN, true); + UPDATE_CONFLICT_LIMIT (eliminate, eliminations, NLOG2N, true); solver->waiting.eliminate.reduce = solver->statistics.reductions + 1; solver->last.eliminate = solver->statistics.search_ticks; return solver->inconsistent ? 20 : 0; diff --git a/src/eliminate.h b/src/eliminate.h index febbac24..c84a4a0c 100644 --- a/src/eliminate.h +++ b/src/eliminate.h @@ -6,16 +6,11 @@ struct kissat; struct clause; -void kissat_update_after_removing_variable (struct kissat *, unsigned); -void kissat_update_after_removing_clause (struct kissat *, struct clause *, - unsigned except); - void kissat_flush_units_while_connected (struct kissat *); bool kissat_eliminating (struct kissat *); int kissat_eliminate (struct kissat *); void kissat_eliminate_binary (struct kissat *, unsigned, unsigned); -void kissat_eliminate_clause (struct kissat *, struct clause *, unsigned); #endif diff --git a/src/failed.c b/src/failed.c index 2e07ac05..cf6e895f 100644 --- a/src/failed.c +++ b/src/failed.c @@ -193,7 +193,7 @@ static void sort_stable_probes (kissat * solver, unsigneds * probes) { const flags *const flags = solver->flags; - const heap *const scores = &solver->scores; + const heap *const scores = SCORES; SORT_STACK (unsigned, *probes, LESS_STABLE_PROBE); } @@ -258,7 +258,7 @@ probe_round (kissat * solver, unsigned round, continue; if (solver->stable) LOG ("probing %s[%g]", LOGLIT (probe), - kissat_get_heap_score (&solver->scores, IDX (probe))); + kissat_get_heap_score (SCORES, IDX (probe))); else LOG ("probing %s{%u}", LOGLIT (probe), LINK (IDX (probe)).stamp); probed++; @@ -485,8 +485,7 @@ kissat_failed_literal_computation (kissat * solver) unsigneds roots; INIT_STACK (roots); - SET_EFFORT_LIMIT (ticks_limit, failed, probing_ticks, - kissat_linear (1 + solver->active)); + SET_EFFORT_LIMIT (ticks_limit, failed, probing_ticks, 1 + solver->active); const unsigned max_rounds = GET_OPTION (failedrounds); unsigned round = 1; diff --git a/src/flags.c b/src/flags.c index 2d6f06d5..9d4ee383 100644 --- a/src/flags.c +++ b/src/flags.c @@ -18,8 +18,8 @@ activate_literal (kissat * solver, unsigned lit) INC (variables_activated); kissat_enqueue (solver, idx); const double score = 1.0 - 1.0 / solver->statistics.variables_activated; - kissat_update_heap (solver, &solver->scores, idx, score); - kissat_push_heap (solver, &solver->scores, idx); + for (all_scores (scores)) + kissat_update_heap (solver, scores, idx, score); assert (solver->unassigned < UINT_MAX); solver->unassigned++; kissat_mark_removed_literal (solver, lit); @@ -42,8 +42,9 @@ deactivate_variable (kissat * solver, flags * f, unsigned idx) assert (solver->active > 0); solver->active--; kissat_dequeue (solver, idx); - if (kissat_heap_contains (&solver->scores, idx)) - kissat_pop_heap (solver, &solver->scores, idx); + for (all_scores (scores)) + if (kissat_heap_contains (scores, idx)) + kissat_pop_heap (solver, scores, idx); } void diff --git a/src/forward.c b/src/forward.c index d3a51411..102f366c 100644 --- a/src/forward.c +++ b/src/forward.c @@ -130,7 +130,7 @@ remove_all_duplicated_binary_clauses (kissat * solver) static void find_forward_subsumption_candidates (kissat * solver, references * candidates) { - const unsigned clslim = solver->bounds.subsume.clause_size; + const unsigned clslim = GET_OPTION (subsumeclslim); const value *const values = solver->values; const flags *const flags = solver->flags; @@ -196,21 +196,20 @@ sort_forward_subsumption_candidates (kissat * solver, references * candidates) static inline bool forward_literal (kissat * solver, unsigned lit, bool binaries, - unsigned *remove) + unsigned *remove, unsigned limit) { watches *watches = &WATCHES (lit); - const unsigned occs = SIZE_WATCHES (*watches); + const size_t size_watches = SIZE_WATCHES (*watches); - if (!occs) + if (!size_watches) return false; - if (occs > solver->bounds.subsume.occurrences) + if (size_watches > limit) return false; watch *begin = BEGIN_WATCHES (*watches), *q = begin; const watch *const end = END_WATCHES (*watches), *p = q; - const size_t size_watches = SIZE_WATCHES (*watches); uint64_t steps = 1 + kissat_cache_lines (size_watches, sizeof (watch)); uint64_t checks = 0; @@ -220,7 +219,7 @@ forward_literal (kissat * solver, unsigned lit, bool binaries, bool subsume = false; - while (p != end) + while (p != end && steps <= limit) { const watch watch = *q++ = *p++; @@ -321,10 +320,13 @@ forward_literal (kissat * solver, unsigned lit, bool binaries, } } - while (p != end) - *q++ = *p++; + if (p != q) + { + while (p != end) + *q++ = *p++; - SET_END_OF_WATCHES (*watches, q); + SET_END_OF_WATCHES (*watches, q); + } ADD (subsumption_checks, checks); ADD (forward_checks, checks); @@ -336,6 +338,7 @@ forward_literal (kissat * solver, unsigned lit, bool binaries, static inline bool forward_marked_clause (kissat * solver, clause * c, unsigned *remove) { + const unsigned limit = GET_OPTION (subsumeocclim); const flags *const flags = solver->flags; INC (forward_steps); @@ -347,9 +350,10 @@ forward_marked_clause (kissat * solver, clause * c, unsigned *remove) assert (!VALUE (lit)); - if (forward_literal (solver, lit, true, remove)) + if (forward_literal (solver, lit, true, remove, limit)) return true; - if (forward_literal (solver, NOT (lit), false, remove)) + + if (forward_literal (solver, NOT (lit), false, remove, limit)) return true; } return false; @@ -357,7 +361,7 @@ forward_marked_clause (kissat * solver, clause * c, unsigned *remove) static bool forward_subsumed_clause (kissat * solver, clause * c, - bool * removed, unsigneds * new_binaries) + bool *removed, unsigneds * new_binaries) { assert (!c->garbage); LOGCLS2 (c, "trying to forward subsume"); @@ -580,14 +584,14 @@ forward_subsume_all_clauses (kissat * solver) #ifndef QUIET size_t checked = 0; #endif - const unsigned occlim = solver->bounds.subsume.occurrences; + const unsigned occlim = GET_OPTION (subsumeocclim); unsigneds new_binaries; INIT_STACK (new_binaries); { SET_EFFORT_LIMIT (steps_limit, forward, forward_steps, - kissat_nlogn (1 + scheduled)); + NLOGN (1 + scheduled)); ward *arena = BEGIN_STACK (solver->arena); @@ -742,6 +746,12 @@ forward_marked_temporary (kissat * solver, unsigned *remove) { const flags *const flags = solver->flags; + unsigned steps_limit_per_literal = GET_OPTION (subsumeocclim); + const uint64_t started = solver->statistics.forward_steps; + const uint64_t total_steps_limit = started + steps_limit_per_literal; + const unsigned size = SIZE_STACK (solver->clause); + steps_limit_per_literal /= size; + for (all_stack (unsigned, lit, solver->clause)) { const unsigned idx = IDX (lit); @@ -750,8 +760,12 @@ forward_marked_temporary (kissat * solver, unsigned *remove) assert (!VALUE (lit)); - if (forward_literal (solver, lit, true, remove)) + if (forward_literal (solver, lit, true, remove, + steps_limit_per_literal)) return true; + + if (solver->statistics.forward_steps > total_steps_limit) + return false; } return false; @@ -776,6 +790,7 @@ forward_subsumed_temporary (kissat * solver) } unsigned remove = INVALID_LIT; + uint64_t steps = solver->statistics.forward_steps; const bool subsume = forward_marked_temporary (solver, &remove); for (all_stack (unsigned, lit, *clause)) @@ -803,6 +818,16 @@ forward_subsumed_temporary (kissat * solver) LOGTMP ("forward strengthened"); } + steps = solver->statistics.forward_steps - steps; + if (solver->budget.forward < steps) + solver->budget.forward = 0; + else + solver->budget.forward -= steps; + + LOG ("temporary forward subsumption used %" PRIu64 " steps", steps); + LOG ("new temporary forward subsumption budget %" PRIu64, + solver->budget.forward); + return subsume; } @@ -812,6 +837,15 @@ kissat_forward_subsume_temporary (kissat * solver) assert (!solver->inconsistent); if (!GET_OPTION (forward)) return false; + if (!solver->budget.forward) + { + LOG ("temporary forward subsumption budget exhausted"); + return false; + } + const unsigned subsumeclslim = GET_OPTION (subsumeclslim); + const size_t size = SIZE_STACK (solver->clause); + if (size > subsumeclslim) + return false; START (forward); bool res = forward_subsumed_temporary (solver); STOP (forward); diff --git a/src/ifthenelse.c b/src/ifthenelse.c index 8a13984a..efa0179d 100644 --- a/src/ifthenelse.c +++ b/src/ifthenelse.c @@ -18,7 +18,7 @@ get_ternary_clause (kissat * solver, reference ref, const value value = values[other]; if (value > 0) { - kissat_eliminate_clause (solver, clause, INVALID_LIT); + kissat_mark_clause_as_garbage (solver, clause); return false; } if (value < 0) @@ -57,7 +57,7 @@ match_ternary_ref (kissat * solver, reference ref, const value value = values[other]; if (value > 0) { - kissat_eliminate_clause (solver, clause, INVALID_LIT); + kissat_mark_clause_as_garbage (solver, clause); return false; } if (value < 0) @@ -122,7 +122,7 @@ kissat_find_if_then_else_gate (kissat * solver, for (const watch * p = begin; p != end; p++) if (!p->type.binary) large_clauses++; - const uint64_t limit = solver->bounds.eliminate.occurrences; + const uint64_t limit = GET_OPTION (eliminateocclim); if (large_clauses * large_clauses > limit) return false; const watch *const last = end - 1; diff --git a/src/inlinescore.h b/src/inlinescore.h index 431115cc..ff7e432a 100644 --- a/src/inlinescore.h +++ b/src/inlinescore.h @@ -3,19 +3,22 @@ #include "inlineheap.h" -static inline void -kissat_update_variable_score (kissat * solver, heap * schedule, unsigned idx) +static inline double +kissat_variable_score (kissat * solver, unsigned idx) { - if (!GET_OPTION (eliminateheap)) - return; - assert (schedule->size); const unsigned lit = LIT (idx); const unsigned not_lit = NOT (lit); size_t pos = SIZE_WATCHES (WATCHES (lit)); size_t neg = SIZE_WATCHES (WATCHES (not_lit)); - double new_score = ((double) pos) * neg + pos + neg; - LOG ("new elimination score %g for variable %u (pos %zu and neg %zu)", - new_score, idx, pos, neg); + return (double) pos *neg + pos + neg; +} + +static inline void +kissat_update_variable_score (kissat * solver, heap * schedule, unsigned idx) +{ + assert (schedule->size); + double new_score = kissat_variable_score (solver, idx); + LOG ("new score %g for variable %s", new_score, LOGVAR (idx)); kissat_update_heap (solver, schedule, idx, -new_score); } diff --git a/src/internal.c b/src/internal.c index 29d888b2..f0560108 100644 --- a/src/internal.c +++ b/src/internal.c @@ -77,7 +77,9 @@ kissat_release (kissat * solver) { kissat_require_initialized (solver); - kissat_release_heap (solver, &solver->scores); + for (all_scores (scores)) + kissat_release_heap (solver, scores); + kissat_release_heap (solver, &solver->schedule); kissat_release_clueue (solver, &solver->clueue); @@ -91,6 +93,7 @@ kissat_release (kissat * solver) RELEASE_STACK (solver->import); DEALLOC_VARIABLE_INDEXED (assigned); + DEALLOC_VARIABLE_INDEXED (conflicted); DEALLOC_VARIABLE_INDEXED (flags); DEALLOC_VARIABLE_INDEXED (links); @@ -131,6 +134,8 @@ kissat_release (kissat * solver) RELEASE_STACK (solver->xorted[0]); RELEASE_STACK (solver->xorted[1]); + RELEASE_STACK (solver->sweep); + RELEASE_STACK (solver->ranks); RELEASE_STACK (solver->antecedents[0]); diff --git a/src/internal.h b/src/internal.h index 7112ef0c..8da31f02 100644 --- a/src/internal.h +++ b/src/internal.h @@ -16,8 +16,8 @@ #include "format.h" #include "frames.h" #include "heap.h" +#include "kimits.h" #include "kissat.h" -#include "limits.h" #include "literal.h" #include "mode.h" #include "nonces.h" @@ -136,7 +136,10 @@ struct kissat rephased rephased; - heap scores; + unsigned branching; + heap scores[2]; + uint64_t *conflicted; + double alphachb; double scinc; heap schedule; @@ -195,6 +198,7 @@ struct kissat reluctant reluctant; bounds bounds; + budget budget; delays delays; enabled enabled; effort last; @@ -222,6 +226,7 @@ struct kissat #else bool gate_eliminated; #endif + unsigneds sweep; #if !defined(NDEBUG) || !defined(NPROOFS) unsigneds added; @@ -253,6 +258,9 @@ struct kissat #define VARS (solver->vars) #define LITS (2*solver->vars) +#define SCORES \ + (&solver->scores[assert (solver->branching < 2), solver->branching]) + static inline unsigned kissat_assigned (kissat * solver) { @@ -277,4 +285,7 @@ kissat_assigned (kissat * solver) C != C ## _END && (C ## _NEXT = kissat_next_clause (C), true); \ C = C ## _NEXT +#define all_scores(S) \ + heap * S = solver->scores; S != solver->scores + 2; S++ + #endif diff --git a/src/limits.c b/src/kimits.c similarity index 78% rename from src/limits.c rename to src/kimits.c index 37d69730..dd53a6de 100644 --- a/src/limits.c +++ b/src/kimits.c @@ -44,37 +44,6 @@ kissat_logn (uint64_t count) return res; } -static double -kissat_lognlogn (uint64_t count) -{ - assert (count > 0); - const double tmp = log10 (count + 9); - const double res = tmp * tmp; - assert (res >= 1); - return res; -} - -static double -kissat_lognlognlogn (uint64_t count) -{ - assert (count > 0); - const double tmp = log10 (count + 9); - const double res = tmp * tmp * tmp; - assert (res >= 1); - return res; -} - -double -kissat_ndivlogn (uint64_t count) -{ - assert (count > 0); - const double div = kissat_logn (count); - assert (div > 0); - const double res = count / div; - assert (res >= 1); - return res; -} - double kissat_sqrt (uint64_t count) { @@ -85,40 +54,13 @@ kissat_sqrt (uint64_t count) } double -kissat_linear (uint64_t count) -{ - assert (count > 0); - const double res = count; - assert (res >= 1); - return res; -} - -double -kissat_nlogn (uint64_t count) +kissat_nlogpown (uint64_t count, unsigned exponent) { assert (count > 0); - const double factor = kissat_logn (count); - assert (factor >= 1); - const double res = count * factor; - assert (res >= 1); - return res; -} - -double -kissat_nlognlogn (uint64_t count) -{ - assert (count > 0); - const double factor = kissat_lognlogn (count); - const double res = count * factor; - assert (res >= 1); - return res; -} - -double -kissat_nlognlognlogn (uint64_t count) -{ - assert (count > 0); - const double factor = kissat_lognlognlogn (count); + const double tmp = log10 (count + 9); + double factor = 1; + while (exponent--) + factor *= tmp; assert (factor >= 1); const double res = count * factor; assert (res >= 1); @@ -156,24 +98,6 @@ kissat_scale_delta (kissat * solver, const char *pretty, uint64_t delta) return scaled; } -uint64_t -kissat_scale_limit (kissat * solver, - const char *pretty, uint64_t count, int base) -{ - assert (base >= 0); - assert (count > 0); - const double f = kissat_logn (count); - assert (f >= 1); - uint64_t scaled = f * base; - kissat_very_verbose (solver, - "scaled %s limit %" PRIu64 " = " - "log10 (%" PRIu64 ") * %d = %g * %d", - pretty, scaled, count, base, f, base); - (void) solver; - (void) pretty; - return scaled; -} - static void init_enabled (kissat * solver) { diff --git a/src/limits.h b/src/kimits.h similarity index 86% rename from src/limits.h rename to src/kimits.h index e6684f04..2d90c869 100644 --- a/src/limits.h +++ b/src/kimits.h @@ -5,6 +5,7 @@ #include typedef struct bounds bounds; +typedef struct budget budget; typedef struct changes changes; typedef struct delays delays; typedef struct delay delay; @@ -20,20 +21,12 @@ struct bounds { uint64_t max_bound_completed; unsigned additional_clauses; - unsigned clause_size; - unsigned occurrences; } eliminate; +}; - struct - { - unsigned clause_size; - unsigned occurrences; - } subsume; - - struct - { - unsigned clause_size; - } xor; +struct budget +{ + uint64_t forward; }; struct changes @@ -137,28 +130,15 @@ void kissat_init_limits (struct kissat *); uint64_t kissat_scale_delta (struct kissat *, const char *, uint64_t); -uint64_t kissat_scale_limit (struct kissat *, - const char *, uint64_t count, int base); - -#define SCALE_LIMIT(COUNT,NAME) \ - kissat_scale_limit (solver, #NAME, \ - solver->statistics.COUNT, GET_OPTION (NAME)) - -double kissat_linear (uint64_t); -double kissat_logn (uint64_t); -double kissat_ndivlogn (uint64_t); -double kissat_nlognlognlogn (uint64_t); -double kissat_nlognlogn (uint64_t); -double kissat_nlogn (uint64_t); double kissat_quadratic (uint64_t); +double kissat_nlogpown (uint64_t, unsigned); double kissat_sqrt (uint64_t); +double kissat_logn (uint64_t); + +#define NLOGN(COUNT) kissat_nlogpown (COUNT,1) +#define NLOG2N(COUNT) kissat_nlogpown (COUNT,2) +#define NLOG3N(COUNT) kissat_nlogpown (COUNT,3) -#define LINEAR(COUNT) kissat_linear (COUNT) -#define NDIVLOGN(COUNT) kissat_ndivlogn (COUNT) -#define NLOGN(COUNT) kissat_nlogn (COUNT) -#define NLOGNLOGN(COUNT) kissat_nlognlogn (COUNT) -#define NLOGNLOGNLOGN(COUNT) kissat_nlognlognlogn (COUNT) -#define QUADRATIC(COUNT) kissat_quadratic (COUNT) #define SQRT(COUNT) kissat_sqrt (COUNT) #define INIT_CONFLICT_LIMIT(NAME,SCALE) \ @@ -202,7 +182,7 @@ do { \ const uint64_t LAST = \ solver->probing ? solver->last.probe : solver->last.eliminate; \ uint64_t REFERENCE = TICKS - LAST; \ - const uint64_t MINEFFORT = GET_OPTION (mineffort); \ + const uint64_t MINEFFORT = 1e3 * GET_OPTION (mineffort); \ if (REFERENCE < MINEFFORT) \ { \ REFERENCE = MINEFFORT; \ diff --git a/src/kissat.h b/src/kissat.h index 6f754b49..350f67aa 100644 --- a/src/kissat.h +++ b/src/kissat.h @@ -24,7 +24,7 @@ const char *kissat_id (void); const char *kissat_version (void); const char *kissat_compiler (void); -const char *kissat_copyright (void); +const char **kissat_copyright (void); void kissat_build (const char *line_prefix); void kissat_banner (const char *line_prefix, const char *name_of_app); diff --git a/src/kitten.c b/src/kitten.c index 282890c4..a7a37100 100644 --- a/src/kitten.c +++ b/src/kitten.c @@ -165,6 +165,8 @@ struct statistics { uint64_t learned; uint64_t original; + uint64_t kitten_flip; + uint64_t kitten_flipped; uint64_t kitten_sat; uint64_t kitten_solved; uint64_t kitten_conflicts; @@ -357,7 +359,7 @@ reference_klause (kitten * kitten, const klause * c) static void log_basic (kitten *, const char *, ...) -__attribute__ ((format (printf, 2, 3))); +__attribute__((format (printf, 2, 3))); static void log_basic (kitten * kitten, const char *fmt, ...) @@ -374,7 +376,7 @@ log_basic (kitten * kitten, const char *fmt, ...) static void log_reference (kitten *, unsigned, const char *, ...) -__attribute__ ((format (printf, 3, 4))); +__attribute__((format (printf, 3, 4))); static void log_reference (kitten * kitten, unsigned ref, const char *fmt, ...) @@ -729,19 +731,32 @@ kitten_randomize_phases (kitten * kitten) LOG ("randomizing phases"); - uint64_t random = kissat_next_random64 (&kitten->generator); unsigned char *phases = kitten->phases; const unsigned vars = kitten->size / 2; - for (unsigned i = 0, shift = 0; i < vars; i++) + uint64_t random = kissat_next_random64 (&kitten->generator); + + unsigned i = 0; + const unsigned rest = vars & ~63u; + + while (i != rest) { - phases[i] = (random >> shift) & 1; - if (++shift == 64) - { - shift = 0; - random = kissat_next_random64 (&kitten->generator); - } + uint64_t *p = (uint64_t *) (phases + i); + p[0] = (random >> 0) & 0x0101010101010101; + p[1] = (random >> 1) & 0x0101010101010101; + p[2] = (random >> 2) & 0x0101010101010101; + p[3] = (random >> 3) & 0x0101010101010101; + p[4] = (random >> 4) & 0x0101010101010101; + p[5] = (random >> 5) & 0x0101010101010101; + p[6] = (random >> 6) & 0x0101010101010101; + p[7] = (random >> 7) & 0x0101010101010101; + random = kissat_next_random64 (&kitten->generator); + i += 64; } + + unsigned shift = 0; + while (i != vars) + phases[i++] = (random >> shift++) & 1; } void @@ -754,8 +769,27 @@ kitten_flip_phases (kitten * kitten) unsigned char *phases = kitten->phases; const unsigned vars = kitten->size / 2; - for (unsigned i = 0; i < vars; i++) - phases[i] = !phases[i]; + unsigned i = 0; + const unsigned rest = vars & ~7u; + + while (i != rest) + { + uint64_t *p = (uint64_t *) (phases + i); + *p ^= 0x0101010101010101; + i += 8; + } + + while (i != vars) + phases[i++] ^= 1; +} + + +void +kitten_no_ticks_limit (kitten * kitten) +{ + REQUIRE_INITIALIZED (); + LOG ("forcing no ticks limit"); + kitten->limits.ticks = UINT64_MAX; } void @@ -793,7 +827,6 @@ shuffle_unsigned_array (kitten * kitten, size_t size, unsigned *a) } } - static void shuffle_unsigned_stack (kitten * kitten, unsigneds * stack) { @@ -1152,22 +1185,21 @@ propagate_literal (kitten * kitten, unsigned lit) const unsigned *const end_watches = END_STACK (*watches); unsigned const *p = q; uint64_t ticks = (((char *) end_watches - (char *) q) >> 7) + 1; - while (conflict == INVALID && p != end_watches) + while (p != end_watches) { const unsigned ref = *q++ = *p++; klause *c = dereference_klause (kitten, ref); assert (c->size > 1); unsigned *lits = c->lits; const unsigned other = lits[0] ^ lits[1] ^ not_lit; - lits[0] = other, lits[1] = not_lit; const value other_value = values[other]; + ticks++; if (other_value > 0) continue; value replacement_value = -1; unsigned replacement = INVALID; const unsigned *const end_lits = lits + c->size; unsigned *r; - ticks++; for (r = lits + 2; r != end_lits; r++) { replacement = *r; @@ -1178,7 +1210,8 @@ propagate_literal (kitten * kitten, unsigned lit) if (replacement_value >= 0) { assert (replacement != INVALID); - ROG (ref, "unwatching %u in", lit); + ROG (ref, "unwatching %u in", not_lit); + lits[0] = other; lits[1] = replacement; *r = not_lit; watch_klause (kitten, replacement, ref); @@ -1189,6 +1222,7 @@ propagate_literal (kitten * kitten, unsigned lit) ROG (ref, "conflict"); INC (kitten_conflicts); conflict = ref; + break; } else { @@ -1237,8 +1271,8 @@ static inline void unassign (kitten * kitten, value * values, unsigned lit) { const unsigned not_lit = lit ^ 1; - assert (values[lit] > 0); - assert (values[not_lit] < 0); + assert (values[lit]); + assert (values[not_lit]); const unsigned idx = lit / 2; #ifdef LOGGING kar *var = kitten->vars + idx; @@ -1263,21 +1297,43 @@ backtrack (kitten * kitten, unsigned jump) (kitten->level == jump + 1 ? "tracking" : "jumping"), jump); kar *vars = kitten->vars; value *values = kitten->values; - while (!EMPTY_STACK (kitten->trail)) + unsigneds *trail = &kitten->trail; + while (!EMPTY_STACK (*trail)) { - const unsigned lit = TOP_STACK (kitten->trail); + const unsigned lit = TOP_STACK (*trail); const unsigned idx = lit / 2; const unsigned level = vars[idx].level; if (level == jump) break; - (void) POP_STACK (kitten->trail); + (void) POP_STACK (*trail); unassign (kitten, values, lit); } - kitten->propagated = SIZE_STACK (kitten->trail); + kitten->propagated = SIZE_STACK (*trail); kitten->level = jump; check_queue (kitten); } +void +completely_backtrack_to_root_level (kitten * kitten) +{ + check_queue (kitten); + LOG ("completely backtracking to level 0"); + value *values = kitten->values; + unsigneds *trail = &kitten->trail; +#ifndef NDEBUG + kar *vars = kitten->vars; +#endif + for (all_stack (unsigned, lit, *trail)) + { + assert (vars[lit / 2].level); + unassign (kitten, values, lit); + } + CLEAR_STACK (*trail); + kitten->propagated = 0; + kitten->level = 0; + check_queue (kitten); +} + static void analyze (kitten * kitten, unsigned conflict) { @@ -1397,9 +1453,9 @@ failing (kitten * kitten) LOG ("first failed assumption %u", failed); kitten->failed[failed] = true; - if (!failed_var->level && - dereference_klause (kitten, failed_reason)->size == 1) + if (failed_unit != INVALID) { + assert (dereference_klause (kitten, failed_reason)->size == 1); LOG ("root-level falsified assumption %u", failed); kitten->failing = failed_reason; ROG (kitten->failing, "failing reason"); @@ -1407,7 +1463,7 @@ failing (kitten * kitten) } const unsigned not_failed = failed ^ 1; - if (failed_reason == INVALID) + if (failed_clashing != INVALID) { LOG ("clashing with negated assumption %u", not_failed); kitten->failed[not_failed] = true; @@ -1479,9 +1535,22 @@ failing (kitten * kitten) CLEAR_STACK (kitten->klause); } +static void +flush_trail (kitten * kitten) +{ + unsigneds *trail = &kitten->trail; + LOG ("flushing %zu root-level literals from trail", SIZE_STACK (*trail)); + assert (!kitten->level); + kitten->propagated = 0; + CLEAR_STACK (*trail); +} + static int decide (kitten * kitten) { + if (!kitten->level && !EMPTY_STACK (kitten->trail)) + flush_trail (kitten); + const value *const values = kitten->values; unsigned decision = INVALID; const size_t assumptions = SIZE_STACK (kitten->assumptions); @@ -1665,14 +1734,6 @@ end_original_klauses (kitten * kitten) kitten->end_original_ref); } -#if 0 -static klause * -begin_learned_klauses (kitten * kitten) -{ - return end_original_klauses (kitten); -} -#endif - static klause * end_klauses (kitten * kitten) { @@ -1729,7 +1790,7 @@ static void reset_incremental (kitten * kitten) { if (kitten->level) - backtrack (kitten, 0); + completely_backtrack_to_root_level (kitten); if (!EMPTY_STACK (kitten->assumptions)) reset_assumptions (kitten); else @@ -1741,6 +1802,81 @@ reset_incremental (kitten * kitten) /*------------------------------------------------------------------------*/ +static bool +flip_literal (kitten * kitten, unsigned lit) +{ + INC (kitten_flip); + signed char *values = kitten->values; + if (values[lit] < 0) + lit ^= 1; + LOG ("trying to flip value of satisfied literal %u", lit); + assert (values[lit] > 0); + katches *watches = kitten->watches + lit; + unsigned *q = BEGIN_STACK (*watches); + const unsigned *const end_watches = END_STACK (*watches); + unsigned const *p = q; + uint64_t ticks = (((char *) end_watches - (char *) q) >> 7) + 1; + bool res = true; + while (p != end_watches) + { + const unsigned ref = *q++ = *p++; + klause *c = dereference_klause (kitten, ref); + unsigned *lits = c->lits; + const unsigned other = lits[0] ^ lits[1] ^ lit; + const value other_value = values[other]; + ticks++; + if (other_value > 0) + continue; + value replacement_value = -1; + unsigned replacement = INVALID; + const unsigned *const end_lits = lits + c->size; + unsigned *r; + for (r = lits + 2; r != end_lits; r++) + { + replacement = *r; + assert (replacement != lit); + replacement_value = values[replacement]; + assert (replacement_value); + if (replacement_value > 0) + break; + } + if (replacement_value > 0) + { + assert (replacement != INVALID); + ROG (ref, "unwatching %u in", lit); + lits[0] = other; + lits[1] = replacement; + *r = lit; + watch_klause (kitten, replacement, ref); + q--; + } + else + { + assert (replacement_value < 0); + ROG (ref, "single satisfied"); + res = false; + break; + } + } + while (p != end_watches) + *q++ = *p++; + SET_END_OF_STACK (*watches, q); + ADD (kitten_ticks, ticks); + if (res) + { + LOG ("flipping value of %u", lit); + values[lit] = -1; + const unsigned not_lit = lit ^ 1; + values[not_lit] = 1; + INC (kitten_flipped); + } + else + LOG ("failed to flip value of %u", lit); + return res; +} + +/*------------------------------------------------------------------------*/ + void kitten_assume (kitten * kitten, unsigned elit) { @@ -1807,8 +1943,10 @@ kitten_solve (kitten * kitten) REQUIRE_INITIALIZED (); if (kitten->status) reset_incremental (kitten); + else if (kitten->level) + completely_backtrack_to_root_level (kitten); - LOG ("solving start under %zu assumptions", + LOG ("starting solving under %zu assumptions", SIZE_STACK (kitten->assumptions)); INC (kitten_solved); @@ -1846,11 +1984,17 @@ kitten_solve (kitten * kitten) else INC (kitten_unknown); - LOG ("solving result %d", res); + LOG ("finished solving with result %d", res); return res; } +int +kitten_status (kitten * kitten) +{ + return kitten->status; +} + unsigned kitten_compute_clausal_core (kitten * kitten, uint64_t * learned_ptr) { @@ -1988,8 +2132,7 @@ kitten_traverse_core_clauses (kitten * kitten, void *state, } const size_t size = SIZE_STACK (*eclause); const unsigned *elits = eclause->begin; - ROG (reference_klause (kitten, c), "traversing %s", - (learned ? "learned" : "original")); + ROG (reference_klause (kitten, c), "traversing"); traverse (state, learned, size, elits); CLEAR_STACK (*eclause); traversed++; @@ -2093,6 +2236,20 @@ kitten_value (kitten * kitten, unsigned elit) return kitten->values[ilit]; } +bool +kitten_flip_literal (kitten * kitten, unsigned elit) +{ + REQUIRE_STATUS (10); + const unsigned eidx = elit / 2; + if (eidx >= kitten->evars) + return false; + unsigned iidx = kitten->import[eidx]; + if (!iidx) + return false; + const unsigned ilit = 2 * (iidx - 1) + (elit & 1); + return flip_literal (kitten, ilit); +} + bool kitten_failed (kitten * kitten, unsigned elit) { @@ -2140,7 +2297,7 @@ maximum_resident_set_size (void) #include "attribute.h" -static void msg (const char *, ...) __attribute__ ((format (printf, 1, 2))); +static void msg (const char *, ...) __attribute__((format (printf, 1, 2))); static void msg (const char *fmt, ...) @@ -2713,8 +2870,8 @@ main (int argc, char **argv) else if (!(dimacs_file = fopen (dimacs_path, "r"))) die ("can not open '%s' for reading", dimacs_path); msg ("Kitten SAT Solver"); - msg ("Copyright (c) 2020-2021, Armin Biere, " - "Johannes Kepler University Linz"); + msg ("Copyright (c) 2021-2022 Armin Biere University of Freiburg"); + msg ("Copyright (c) 2020-2021 Armin Biere Johannes Kepler University Linz"); msg ("reading '%s'", dimacs_path); ints originals; INIT_STACK (originals); diff --git a/src/kitten.h b/src/kitten.h index fd9651e0..49b1ed37 100644 --- a/src/kitten.h +++ b/src/kitten.h @@ -12,9 +12,10 @@ void kitten_clear (kitten *); void kitten_release (kitten *); void kitten_track_antecedents (kitten *); + void kitten_shuffle_clauses (kitten *); -void kitten_randomize_phases (kitten *); void kitten_flip_phases (kitten *); +void kitten_randomize_phases (kitten *); void kitten_assume (kitten *, unsigned lit); @@ -26,13 +27,15 @@ void kitten_clause_with_id_and_exception (kitten *, unsigned id, size_t size, const unsigned *, unsigned except); - +void kitten_no_ticks_limit (kitten *); void kitten_set_ticks_limit (kitten *, uint64_t); int kitten_solve (kitten *); +int kitten_status (kitten *); signed char kitten_value (kitten *, unsigned); bool kitten_failed (kitten *, unsigned); +bool kitten_flip_literal (kitten *, unsigned); unsigned kitten_compute_clausal_core (kitten *, uint64_t * learned); void kitten_shrink_to_clausal_core (kitten *); diff --git a/src/learn.c b/src/learn.c index b2fbb3af..64f3639c 100644 --- a/src/learn.c +++ b/src/learn.c @@ -100,7 +100,7 @@ learn_reference (kissat * solver, unsigned not_uip, unsigned glue) const reference ref = kissat_new_redundant_clause (solver, glue); assert (ref != INVALID_REF); clause *c = kissat_dereference_clause (solver, ref); - c->used = 1 + (glue <= (unsigned) GET_OPTION (tier2)); + c->used = 0; //1 + (glue <= (unsigned) GET_OPTION (tier2)); const unsigned new_level = determine_new_level (solver, jump_level); kissat_backtrack_after_conflict (solver, new_level); kissat_assign_reference (solver, not_uip, ref, c); diff --git a/src/logging.c b/src/logging.c index f6f9bcca..8e6b497b 100644 --- a/src/logging.c +++ b/src/logging.c @@ -83,12 +83,16 @@ kissat_log_var (kissat * solver, unsigned idx) } static void -log_lits (kissat * solver, size_t size, const unsigned *lits) +log_lits (kissat * solver, size_t size, + const unsigned *lits, const unsigned *counts) { for (size_t i = 0; i < size; i++) { + const unsigned lit = lits[i]; fputc (' ', stdout); - fputs (LOGLIT (lits[i]), stdout); + if (counts) + printf ("%u*", counts[lit]); + fputs (LOGLIT (lit), stdout); } } @@ -101,7 +105,67 @@ kissat_log_lits (kissat * solver, const char *prefix, size_t size, begin_logging (solver, prefix, fmt, &ap); va_end (ap); printf (" size %zu clause", size); - log_lits (solver, size, lits); + log_lits (solver, size, lits, 0); + end_logging (); +} + +void +kissat_log_litset (kissat * solver, const char *prefix, size_t size, + const unsigned *const lits, const char *fmt, ...) +{ + va_list ap; + va_start (ap, fmt); + begin_logging (solver, prefix, fmt, &ap); + va_end (ap); + printf (" size %zu literal set {", size); + log_lits (solver, size, lits, 0); + fputs (" }", stdout); + end_logging (); +} + +void +kissat_log_litpart (kissat * solver, const char *prefix, size_t size, + const unsigned *const lits, const char *fmt, ...) +{ + va_list ap; + va_start (ap, fmt); + begin_logging (solver, prefix, fmt, &ap); + va_end (ap); + size_t classes = 0; + for (size_t i = 0; i < size; i++) + if (lits[i] == INVALID_LIT) + classes++; + printf (" %zu literals %zu classes literal partition [", + size - classes, classes); + for (size_t i = 0; i < size; i++) + { + const unsigned lit = lits[i]; + if (lit == INVALID_LIT) + { + if (i + 1 != size) + fputs (" |", stdout); + } + else + { + fputc (' ', stdout); + fputs (LOGLIT (lit), stdout); + } + } + fputs (" ]", stdout); + end_logging (); +} + +void +kissat_log_counted_lits (kissat * solver, const char *prefix, + size_t size, const unsigned *const lits, + const unsigned *const counts, const char *fmt, ...) +{ + va_list ap; + va_start (ap, fmt); + begin_logging (solver, prefix, fmt, &ap); + va_end (ap); + printf (" size %zu clause", size); + log_lits (solver, size, lits, counts); end_logging (); } @@ -116,7 +180,7 @@ kissat_log_resolvent (kissat * solver, const char *prefix, const size_t size = SIZE_STACK (solver->resolvent); printf (" size %zu resolvent", size); const unsigned *const lits = BEGIN_STACK (solver->resolvent); - log_lits (solver, size, lits); + log_lits (solver, size, lits, 0); end_logging (); } @@ -212,7 +276,21 @@ kissat_log_clause (kissat * solver, const char *prefix, begin_logging (solver, prefix, fmt, &ap); va_end (ap); log_clause (solver, c); - log_lits (solver, c->size, c->lits); + log_lits (solver, c->size, c->lits, 0); + end_logging (); +} + +void +kissat_log_counted_clause (kissat * solver, const char *prefix, + const clause * c, const unsigned *counts, + const char *fmt, ...) +{ + va_list ap; + va_start (ap, fmt); + begin_logging (solver, prefix, fmt, &ap); + va_end (ap); + log_clause (solver, c); + log_lits (solver, c->size, c->lits, counts); end_logging (); } @@ -251,7 +329,7 @@ log_ref (kissat * solver, reference ref) { clause *c = kissat_dereference_clause (solver, ref); log_clause (solver, c); - log_lits (solver, c->size, c->lits); + log_lits (solver, c->size, c->lits, 0); } void diff --git a/src/logging.h b/src/logging.h index 3b9bcffa..20eb0f95 100644 --- a/src/logging.h +++ b/src/logging.h @@ -19,6 +19,10 @@ ATTRIBUTE_FORMAT (3, 4); void kissat_log_clause (kissat *, const char*, const clause *, const char *, ...) ATTRIBUTE_FORMAT (4, 5); +void kissat_log_counted_clause (kissat *, const char*, const clause *, + const unsigned *, const char *, ...) +ATTRIBUTE_FORMAT (5, 6); + void kissat_log_binary (kissat *, const char*, unsigned, unsigned, const char *, ...) ATTRIBUTE_FORMAT (5, 6); @@ -30,6 +34,19 @@ void kissat_log_lits (kissat *, const char*, size_t, const unsigned *, const char *, ...) ATTRIBUTE_FORMAT (5, 6); +void kissat_log_litset (kissat *, const char*, + size_t, const unsigned *, const char *, ...) +ATTRIBUTE_FORMAT (5, 6); + +void kissat_log_litpart (kissat *, const char*, + size_t, const unsigned *, const char *, ...) +ATTRIBUTE_FORMAT (5, 6); + +void kissat_log_counted_lits (kissat *, const char*, + size_t, const unsigned *, + const unsigned * counts, const char *, ...) +ATTRIBUTE_FORMAT (6, 7); + void kissat_log_unsigneds (kissat *, const char*, size_t, const unsigned *, const char *, ...) ATTRIBUTE_FORMAT (5, 6); @@ -101,6 +118,24 @@ do { \ kissat_log_lits (solver, LOGPREFIX, __VA_ARGS__); \ } while (0) +#define LOGLITSET(...) \ +do { \ + if (solver && GET_OPTION (log)) \ + kissat_log_litset (solver, LOGPREFIX, __VA_ARGS__); \ +} while (0) + +#define LOGLITPART(...) \ +do { \ + if (solver && GET_OPTION (log)) \ + kissat_log_litpart (solver, LOGPREFIX, __VA_ARGS__); \ +} while (0) + +#define LOGCOUNTEDLITS(...) \ +do { \ + if (solver && GET_OPTION (log)) \ + kissat_log_counted_lits (solver, LOGPREFIX, __VA_ARGS__); \ +} while (0) + #define LOGLITS3(...) \ do { \ if (GET_OPTION (log) > 2) \ @@ -155,6 +190,12 @@ do { \ kissat_log_clause (solver, LOGPREFIX, __VA_ARGS__); \ } while (0) +#define LOGCOUNTEDCLS(...) \ +do { \ + if (solver && GET_OPTION (log)) \ + kissat_log_counted_clause (solver, LOGPREFIX, __VA_ARGS__); \ +} while (0) + #define LOGLINE(...) \ do { \ if (solver && GET_OPTION (log)) \ @@ -234,7 +275,10 @@ do { \ #define LOGRES(...) do { } while (0) #define LOGRES2(...) do { } while (0) #define LOGLITS(...) do { } while (0) +#define LOGLITSET(...) do { } while (0) +#define LOGLITPART(...) do { } while (0) #define LOGLITS3(...) do { } while (0) +#define LOGCOUNTEDLITS(...) do { } while (0) #define LOGEXT(...) do { } while (0) #define LOGEXT2(...) do { } while (0) #define LOGINTS(...) do { } while (0) @@ -243,6 +287,7 @@ do { \ #define LOGCLS(...) do { } while (0) #define LOGCLS2(...) do { } while (0) #define LOGCLS3(...) do { } while (0) +#define LOGCOUNTEDCLS(...) do { } while (0) #define LOGLINE(...) do { } while (0) #define LOGREF(...) do { } while (0) #define LOGREF2(...) do { } while (0) diff --git a/src/makefile b/src/makefile deleted file mode 120000 index cc63b08c..00000000 --- a/src/makefile +++ /dev/null @@ -1 +0,0 @@ -../makefile \ No newline at end of file diff --git a/src/mode.c b/src/mode.c index c01ad1dd..40c94f30 100644 --- a/src/mode.c +++ b/src/mode.c @@ -1,3 +1,4 @@ +#include "bump.h" #include "inline.h" #include "inlineheap.h" #include "inlinequeue.h" @@ -31,7 +32,7 @@ new_mode_limit (kissat * solver) assert (interval > 0); const uint64_t count = (statistics->switched_modes + 1) / 2; - const uint64_t scaled = interval * kissat_quadratic (count); + const uint64_t scaled = interval * kissat_nlogpown (count, 4); limits->mode.ticks = statistics->search_ticks + scaled; #ifndef QUIET if (solver->stable) @@ -110,15 +111,6 @@ switch_to_focused_mode (kissat * solver) kissat_new_focused_restart_limit (solver); } -void -kissat_update_scores (kissat * solver) -{ - heap *scores = &solver->scores; - for (all_variables (idx)) - if (ACTIVE (idx) && !kissat_heap_contains (scores, idx)) - kissat_push_heap (solver, scores, idx); -} - static void switch_to_stable_mode (kissat * solver) { diff --git a/src/options.h b/src/options.h index c07c7adb..39ae0ccd 100644 --- a/src/options.h +++ b/src/options.h @@ -5,6 +5,7 @@ #include #define OPTIONS \ +OPTION( acids, 0, 0, 1, "use ACIDS instead of VSIDS") \ OPTION( ands, 1, 0, 1, "extract and eliminate and gates") \ OPTION( autarky, 1, 0, 1, "enable autarky reasoning") \ OPTION( autarkydelay, 0, 0, 1, "delay autarky reasoning") \ @@ -16,10 +17,12 @@ OPTION( backbonekeep, 1, 0, 1, "keep backbone candidates") \ OPTION( backbonemaxrounds, 1e3, 1, INT_MAX, "maximum backbone rounds") \ OPTION( backbonerounds, 100, 1, INT_MAX, "backbone rounds limit") \ OPTION( backward, 1, 0, 1, "backward subsumption in BVE") \ +OPTION( bump, 1, 0, 1, "enable variable bumping") \ OPTION( bumpreasons, 1, 0, 1, "bump reason side literals too") \ OPTION( bumpreasonslimit, 10, 1, INT_MAX, "relative reason literals limit") \ OPTION( bumpreasonsrate, 10, 1, INT_MAX, "decision rate limit") \ OPTION( cachesample, 1, 0, 1, "sample cached assignments") \ +OPTION( chb, 0, 0, 2, "use CHB in stable mode (1=alternating,2=only)") \ DBGOPT( check, 2, 0, 2, "check model (1) and derived clauses (2)") \ OPTION( chrono, 1, 0, 1, "allow chronological backtracking") \ OPTION( chronolevels, 100, 0, INT_MAX, "maximum jumped over levels") \ @@ -28,6 +31,7 @@ OPTION( compactlim, 10, 0, 100, "compact inactive limit (in percent)") \ OPTION( decay, 50, 1, 200, "per mille scores decay") \ OPTION( definitioncores, 2, 1, 100, "how many cores") \ OPTION( definitions, 1, 0, 1, "extract general definitions") \ +OPTION( definitionticks, 1e6, 0, INT_MAX, "kitten ticks limits") \ OPTION( defraglim, 75, 50, 100, "usable defragmentation limit in percent") \ OPTION( defragsize, 1<<18, 10, INT_MAX, "size defragmentation limit") \ OPTION( delay, 2, 0, 10, "maximum delay (autarky, failed, ...)") \ @@ -37,12 +41,11 @@ OPTION( eliminatebound, 16 ,0 , 1<<13, "maximum elimination bound") \ OPTION( eliminateclslim, 100, 1, INT_MAX, "elimination clause size limit") \ OPTION( eliminatedelay, 0, 0, 1, "delay variable elimination") \ OPTION( eliminateeffort, 100, 0, 2e3, "effort in per mille") \ -OPTION( eliminateheap, 0, 0, 1, "use heap to schedule elimination") \ OPTION( eliminateinit, 500, 0, INT_MAX, "initial elimination interval") \ OPTION( eliminateint, 500, 10, INT_MAX, "base elimination interval") \ -OPTION( eliminatekeep, 1, 0, 1, "keep elimination candidates") \ -OPTION( eliminateocclim, 1e3, 0, INT_MAX, "elimination occurrence limit") \ -OPTION( eliminaterounds, 2, 1, 1000, "elimination rounds limit") \ +OPTION( eliminateocclim, 2e3, 0, INT_MAX, "elimination occurrence limit") \ +OPTION( eliminaterounds, 2, 1, 1e4, "elimination rounds limit") \ +OPTION( emachb, 17, 2, 1e6, "CHB moving average window") \ OPTION( emafast, 33, 10, 1e6, "fast exponential moving average window") \ OPTION( emaslow, 1e5, 100, 1e6, "slow exponential moving average window") \ EMBOPT( embedded, 1, 0, 1, "parse and apply embedded options") \ @@ -60,7 +63,7 @@ OPTION( hyper, 1, 0, 1, "on-the-fly hyper binary resolution") \ OPTION( ifthenelse, 1, 0, 1, "extract and eliminate if-then-else gates") \ OPTION( incremental, 0, 0, 1, "enable incremental solving") \ LOGOPT( log, 0, 0, 5, "logging level (1=on,2=more,3=check,4/5=mem)") \ -OPTION( mineffort, 1e4, 0, INT_MAX, "minimum absolute effort") \ +OPTION( mineffort, 10, 0, INT_MAX, "minimum absolute effort") \ OPTION( minimize, 1, 0, 1, "learned clause minimization") \ OPTION( minimizedepth, 1e3, 1, 1e6, "minimization depth") \ OPTION( minimizeticks, 1, 0, 1, "count ticks in minimize and shrink") \ @@ -69,7 +72,7 @@ OPTION( modeticks, 1e8, 1e3, INT_MAX, "initial focused ticks limit") \ OPTION( otfs, 1, 0, 1, "on-the-fly strengthening") \ OPTION( phase, 1, 0, 1, "initial decision phase") \ OPTION( phasesaving, 1, 0, 1, "enable phase saving") \ -OPTION( probe, 1, 0, 1, "enable probing") \ +OPTION( probe, 2, 0, 2, "enable probing (1=alternating,2=all)") \ OPTION( probedelay, 0, 0, 1, "delay probing") \ OPTION( probeinit, 100, 0, INT_MAX, "initial probing interval") \ OPTION( probeint, 100, 2, INT_MAX, "probing interval") \ @@ -82,7 +85,6 @@ OPTION( reduce, 1, 0, 1, "learned clause reduction") \ OPTION( reducefraction, 75, 10, 100, "reduce fraction in percent") \ OPTION( reduceinit, 3e2, 2, 1e5, "initial reduce interval") \ OPTION( reduceint, 1e3, 2, 1e5, "base reduce interval") \ -OPTION( reducerestart, 0, 0, 2, "restart at reduce (1=stable,2=always)") \ OPTION( reluctant, 1, 0, 1, "stable reluctant doubling restarting") \ OPTION( reluctantint, 1<<10, 2, 1<<15, "reluctant interval") \ OPTION( reluctantlim, 1<<20, 0, 1<<30, "reluctant limit (0=unlimited)") \ @@ -97,7 +99,7 @@ OPTION( rephasewalking, 1, 0, 1, "rephase walking phase") \ OPTION( restart, 1, 0, 1, "enable restarts") \ OPTION( restartint, RESTARTINT_DEFAULT, 1, 1e4, "base restart interval") \ OPTION( restartmargin, 10, 0, 25, "fast/slow margin in percent") \ -OPTION( restartreusetrail, 1, 0, 1, "restarts reuse trail") \ +OPTION( reusetrail, 0, 0, 2, "restarts reuse trail (1=focused,2=always)") \ OPTION( seed, 0, 0, INT_MAX, "random seed") \ OPTION( shrink, 3, 0, 3, "learned clauses (1=bin,2=lrg,3=rec)") \ OPTION( shrinkminimize, 1, 0, 1, "minimize during shrinking") \ @@ -110,13 +112,17 @@ OPTION( substituterounds, 2, 1, 100, "maximum substitution rounds") \ OPTION( subsumeclslim, 1e3, 1, INT_MAX, "subsumption clause size limit") \ OPTION( subsumeocclim, 1e3, 0, INT_MAX, "subsumption occurrence limit") \ OPTION( sweep, 1, 0, 1, "enable SAT sweeping") \ -OPTION( sweepclauses, 1000, 0, INT_MAX, "maximum environment clauses") \ -OPTION( sweepdepth, 2, 0, INT_MAX, "environment depth") \ -OPTION( sweepeffort, 20, 0, 1e4, "effort in per mille") \ -OPTION( sweepmaxdepth, 4, 2, INT_MAX, "maximum environment depth") \ -OPTION( sweepvars, 100, 0, INT_MAX, "maximum environment variables") \ +OPTION( sweepboost, 0, 0, 2048, "SAT sweeping boost") \ +OPTION( sweepclauses, 1024, 0, INT_MAX, "environment clauses") \ +OPTION( sweepdepth, 1, 0, INT_MAX, "environment depth") \ +OPTION( sweepeffort, 10, 0, 1e4, "effort in per mille") \ +OPTION( sweepfliprounds, 1, 0, INT_MAX, "flipping rounds") \ +OPTION( sweepmaxclauses, 4096, 2, INT_MAX, "maximum environment clauses") \ +OPTION( sweepmaxdepth, 2, 1, INT_MAX, "maximum environment depth") \ +OPTION( sweepmaxvars, 128, 2, INT_MAX, "maximum environment variables") \ +OPTION( sweepvars, 128, 0, INT_MAX, "environment variables") \ OPTION( target, TARGET_DEFAULT, 0, 2, "target phases (1=stable,2=focused)") \ -OPTION( ternary, 1, 0, 1, "enable hyper ternary resolution") \ +OPTION( ternary, 0, 0, 1, "enable hyper ternary resolution") \ OPTION( ternarydelay, 1, 0, 1, "delay hyper ternary resolution") \ OPTION( ternaryeffort, 70, 0, 2e3, "effort in per mille") \ OPTION( ternaryheap, 1, 0, 1, "use heap to schedule ternary resolution") \ @@ -130,18 +136,18 @@ OPTION( tumble, 1, 0, 1, "tumbled external indices order") \ NQTOPT( verbose, 0, 0, 3, "verbosity level") \ OPTION( vivify, 1, 0, 1, "vivify clauses") \ OPTION( vivifyeffort, 100, 0, 1e3, "effort in per mille") \ -OPTION( vivifyimply, 2, 0, 2, "remove implied redundant clauses") \ +OPTION( vivifyimply, 3, 0, 3, "remove implied redundant clauses") \ OPTION( vivifyirred, 1, 1, 100, "relative irredundant effort") \ -OPTION( vivifykeep, 0, 0, 1, "keep vivification candidates") \ +OPTION( vivifykeep, 1, 0, 1, "keep vivification candidates") \ OPTION( vivifytier1, 3, 1, 100, "relative tier1 effort") \ OPTION( vivifytier2, 6, 1, 100, "relative tier2 effort") \ -OPTION( walkeffort, 5, 0, 1e6, "effort in per mille") \ +OPTION( walkeffort, 50, 0, 1e6, "effort in per mille") \ OPTION( walkfit, 1, 0, 1, "fit CB value to average clause length") \ OPTION( walkinitially, 0, 0, 1, "initial local search") \ OPTION( walkreuse, 1, 0, 2, "reuse walking results (2=always)") \ OPTION( walkweighted, 1, 0, 1, "use clause weights") \ +OPTION( warmup, 1, 0, 1, "initialize phases by unit propagation") \ OPTION( xors, 1, 0, 1, "extract and eliminate XOR gates") \ -OPTION( xorsbound, 1 ,0 , 1<<13, "minimum elimination bound") \ OPTION( xorsclslim, 5, 3, 31, "XOR extraction clause size limit") \ // *INDENT-OFF* diff --git a/src/probe.c b/src/probe.c index 912ae1db..e4261e5a 100644 --- a/src/probe.c +++ b/src/probe.c @@ -28,8 +28,10 @@ probe (kissat * solver) RETURN_IF_DELAYED (probe); kissat_backtrack_propagate_and_flush_trail (solver); assert (!solver->inconsistent); + const uint64_t probings = solver->statistics.probings; + const bool full = GET_OPTION (probe) > 1; STOP_SEARCH_AND_START_SIMPLIFIER (probe); - kissat_phase (solver, "probe", GET (probings), + kissat_phase (solver, "probe", probings, "probing limit hit after %" PRIu64 " conflicts", solver->limits.probe.conflicts); const changes before = kissat_changes (solver); @@ -37,8 +39,19 @@ probe (kissat * solver) kissat_binary_clauses_backbone (solver); kissat_ternary (solver); kissat_transitive_reduction (solver); - kissat_failed_literal_computation (solver); - kissat_vivify (solver); + if (!GET_OPTION (failed)) + kissat_vivify (solver); + else if (!GET_OPTION (vivify)) + kissat_failed_literal_computation (solver); + else if (full) + { + kissat_failed_literal_computation (solver); + kissat_vivify (solver); + } + else if (probings & 1) + kissat_failed_literal_computation (solver); + else + kissat_vivify (solver); kissat_sweep (solver); kissat_substitute (solver); kissat_binary_clauses_backbone (solver); diff --git a/src/profile.h b/src/profile.h index 269ba3be..c429282a 100644 --- a/src/profile.h +++ b/src/profile.h @@ -46,6 +46,7 @@ PROF(total,0) \ PROF(transitive,2) \ PROF(vivify,2) \ PROF(walking,2) \ +PROF(warmup,2) \ struct profile { diff --git a/src/promote.c b/src/promote.c index b7911c8f..c6f84404 100644 --- a/src/promote.c +++ b/src/promote.c @@ -19,7 +19,7 @@ kissat_promote_clause (kissat * solver, clause * c, unsigned new_glue) { assert (tier1 < old_glue); assert (new_glue <= tier1); - LOGCLS (c, "promoting to new glue %u to tier1", new_glue); + LOGCLS (c, "promoting with new glue %u to tier1", new_glue); INC (clauses_promoted1); c->keep = true; } @@ -27,7 +27,7 @@ kissat_promote_clause (kissat * solver, clause * c, unsigned new_glue) { assert (tier2 < old_glue); assert (tier1 < new_glue && new_glue <= tier2); - LOGCLS (c, "promoting to new glue %u to tier2", new_glue); + LOGCLS (c, "promoting with new glue %u to tier2", new_glue); INC (clauses_promoted2); c->used = 2; } @@ -36,14 +36,14 @@ kissat_promote_clause (kissat * solver, clause * c, unsigned new_glue) INC (clauses_kept2); assert (tier1 < old_glue && old_glue <= tier2); assert (tier1 < new_glue && new_glue <= tier2); - LOGCLS (c, "keeping to new glue %u in tier2", new_glue); + LOGCLS (c, "keeping with new glue %u in tier2", new_glue); } else { INC (clauses_kept3); assert (tier2 < old_glue); assert (tier2 < new_glue); - LOGCLS (c, "keeping to new glue %u in tier3", new_glue); + LOGCLS (c, "keeping with new glue %u in tier3", new_glue); } INC (clauses_improved); c->glue = new_glue; diff --git a/src/promote.h b/src/promote.h index e7d60bad..9fc79547 100644 --- a/src/promote.h +++ b/src/promote.h @@ -6,9 +6,11 @@ void kissat_promote_clause (struct kissat *, clause *, unsigned new_glue); static inline unsigned -kissat_recompute_glue (kissat * solver, clause * c) +kissat_recompute_glue (kissat * solver, clause * c, unsigned limit) { + assert (limit); assert (EMPTY_STACK (solver->promote)); + unsigned res = 0; for (all_literals_in_clause (lit, c)) { assert (VALUE (lit)); @@ -16,6 +18,8 @@ kissat_recompute_glue (kissat * solver, clause * c) frame *frame = &FRAME (level); if (frame->promote) continue; + if (++res == limit) + break; frame->promote = true; PUSH_STACK (solver->promote, level); } @@ -25,7 +29,6 @@ kissat_recompute_glue (kissat * solver, clause * c) assert (frame->promote); frame->promote = false; } - unsigned res = SIZE_STACK (solver->promote); CLEAR_STACK (solver->promote); return res; } diff --git a/src/propbeyond.c b/src/propbeyond.c new file mode 100644 index 00000000..366d1919 --- /dev/null +++ b/src/propbeyond.c @@ -0,0 +1,35 @@ +#include "fastassign.h" +#include "propbeyond.h" +#include "trail.h" + +#define PROPAGATE_LITERAL propagate_literal_beyond_conflicts +#define CONTINUE_PROPAGATING_AFTER_CONFLICT +#define PROPAGATION_TYPE "beyond conflict" + +#include "proplit.h" + +static void +propagate_literals_beyond_conflicts (kissat * solver) +{ + unsigned *propagate = solver->propagate; + while (propagate != END_ARRAY (solver->trail)) + (void) propagate_literal_beyond_conflicts (solver, *propagate++); + solver->propagate = propagate; +} + +void +kissat_propagate_beyond_conflicts (kissat * solver) +{ + assert (!solver->probing); + assert (solver->watching); + assert (!solver->inconsistent); + + START (propagate); + + solver->ticks = 0; + const unsigned *saved_propagate = solver->propagate; + propagate_literals_beyond_conflicts (solver); + kissat_update_search_propagation_statistics (solver, saved_propagate); + + STOP (propagate); +} diff --git a/src/propbeyond.h b/src/propbeyond.h new file mode 100644 index 00000000..09eaf1b4 --- /dev/null +++ b/src/propbeyond.h @@ -0,0 +1,9 @@ +#ifndef _propall_h_INCLUDED +#define _propall_h_INCLUDED + +struct kissat; +struct clause; + +void kissat_propagate_beyond_conflicts (struct kissat *); + +#endif diff --git a/src/proplit.h b/src/proplit.h index a1ecda1d..03a3b986 100644 --- a/src/proplit.h +++ b/src/proplit.h @@ -68,6 +68,36 @@ kissat_update_probing_propagation_statistics (kissat * solver, ADD (ticks, ticks); } +#else + +static inline void +kissat_update_search_propagation_statistics (kissat * solver, + const unsigned *saved_propagate) +{ + assert (saved_propagate <= solver->propagate); + const unsigned propagated = solver->propagate - saved_propagate; + + LOG ("propagated %u literals", propagated); + LOG ("propagation took %" PRIu64 " ticks", solver->ticks); + + ADD (propagations, propagated); + ADD (ticks, solver->ticks); + + ADD (search_propagations, propagated); + ADD (search_ticks, solver->ticks); + + if (solver->stable) + { + ADD (stable_propagations, propagated); + ADD (stable_ticks, solver->ticks); + } + else + { + ADD (focused_propagations, propagated); + ADD (focused_ticks, solver->ticks); + } +} + #endif static inline void @@ -112,6 +142,7 @@ PROPAGATE_LITERAL (kissat * solver, const watch *p = q; unsigneds *const delayed = &solver->delayed; + assert (EMPTY_STACK (*delayed)); const size_t size_watches = SIZE_WATCHES (*watches); uint64_t ticks = 1 + kissat_cache_lines (size_watches, sizeof (watch)); @@ -129,19 +160,25 @@ PROPAGATE_LITERAL (kissat * solver, const unsigned blocking = head.blocking.lit; assert (VALID_INTERNAL_LITERAL (blocking)); const value blocking_value = values[blocking]; - if (head.type.binary) + const bool binary = head.type.binary; + watch tail; + if (!binary) + tail = *q++ = *p++; + if (blocking_value > 0) + continue; + if (binary) { #ifdef HYPER_PROPAGATION assert (blocking_value > 0); #else - if (blocking_value > 0) - continue; const bool redundant = head.binary.redundant; if (blocking_value < 0) { res = kissat_binary_conflict (solver, redundant, not_lit, blocking); +#ifndef CONTINUE_PROPAGATING_AFTER_CONFLICT break; +#endif } else { @@ -155,9 +192,6 @@ PROPAGATE_LITERAL (kissat * solver, } else { - const watch tail = *q++ = *p++; - if (blocking_value > 0) - continue; const reference ref = tail.raw; assert (ref < SIZE_STACK (solver->arena)); clause *const c = (clause *) (arena + ref); @@ -179,16 +213,27 @@ PROPAGATE_LITERAL (kissat * solver, assert (lit != other); const value other_value = values[other]; if (other_value > 0) - q[-2].blocking.lit = other; - else { - const unsigned *const end_lits = lits + c->size; - unsigned *const searched = lits + c->searched; - assert (c->lits + 2 <= searched); - assert (searched < end_lits); - unsigned *r, replacement = INVALID_LIT; - value replacement_value = -1; - for (r = searched; r != end_lits; r++) + q[-2].blocking.lit = other; + continue; + } + const unsigned *const end_lits = lits + c->size; + unsigned *const searched = lits + c->searched; + assert (c->lits + 2 <= searched); + assert (searched < end_lits); + unsigned *r, replacement = INVALID_LIT; + value replacement_value = -1; + for (r = searched; r != end_lits; r++) + { + replacement = *r; + assert (VALID_INTERNAL_LITERAL (replacement)); + replacement_value = values[replacement]; + if (replacement_value >= 0) + break; + } + if (replacement_value < 0) + { + for (r = lits + 2; r != searched; r++) { replacement = *r; assert (VALID_INTERNAL_LITERAL (replacement)); @@ -196,92 +241,76 @@ PROPAGATE_LITERAL (kissat * solver, if (replacement_value >= 0) break; } - if (replacement_value < 0) + } + + if (replacement_value >= 0) + { + c->searched = r - lits; + assert (replacement != INVALID_LIT); + LOGREF (ref, "unwatching %s in", LOGLIT (not_lit)); + q -= 2; + lits[0] = other; + lits[1] = replacement; + assert (lits[0] != lits[1]); + *r = not_lit; + kissat_delay_watching_large (solver, delayed, + replacement, other, ref); + ticks++; + } + else if (other_value) + { + assert (replacement_value < 0); + assert (blocking_value < 0); + assert (other_value < 0); + LOGREF (ref, "conflicting"); + res = c; +#ifndef CONTINUE_PROPAGATING_AFTER_CONFLICT + break; +#endif + } +#ifdef HYPER_PROPAGATION + else if (hyper) + { + assert (replacement_value < 0); + unsigned dom = kissat_find_dominator (solver, other, c); + if (dom != INVALID_LIT) { - for (r = lits + 2; r != searched; r++) - { - replacement = *r; - assert (VALID_INTERNAL_LITERAL (replacement)); - replacement_value = values[replacement]; - if (replacement_value >= 0) - break; - } - } + LOGBINARY (dom, other, "hyper binary resolvent"); - if (replacement_value >= 0) - c->searched = r - lits; + INC (hyper_binary_resolved); + INC (clauses_added); + + INC (hyper_binaries); + INC (clauses_redundant); + + CHECK_AND_ADD_BINARY (dom, other); + ADD_BINARY_TO_PROOF (dom, other); + + kissat_assign_binary_at_level_one (solver, + values, assigned, + true, other, dom); + + delay_watching_hyper (solver, delayed, dom, other); + delay_watching_hyper (solver, delayed, other, dom); + + kissat_delay_watching_large (solver, delayed, + not_lit, other, ref); - if (replacement_value > 0) - { - assert (replacement != INVALID_LIT); - q[-2].blocking.lit = replacement; - } - else if (!replacement_value) - { - assert (replacement != INVALID_LIT); LOGREF (ref, "unwatching %s in", LOGLIT (not_lit)); q -= 2; - lits[0] = other; - lits[1] = replacement; - assert (lits[0] != lits[1]); - *r = not_lit; - kissat_delay_watching_large (solver, delayed, - replacement, other, ref); - ticks++; - } - else if (other_value) - { - assert (replacement_value < 0); - assert (blocking_value < 0); - assert (other_value < 0); - LOGREF (ref, "conflicting"); - res = c; - break; - } -#ifdef HYPER_PROPAGATION - else if (hyper) - { - assert (replacement_value < 0); - unsigned dom = kissat_find_dominator (solver, other, c); - if (dom != INVALID_LIT) - { - LOGBINARY (dom, other, "hyper binary resolvent"); - - INC (hyper_binary_resolved); - INC (clauses_added); - - INC (hyper_binaries); - INC (clauses_redundant); - - CHECK_AND_ADD_BINARY (dom, other); - ADD_BINARY_TO_PROOF (dom, other); - - kissat_assign_binary_at_level_one (solver, - values, assigned, - true, other, dom); - - delay_watching_hyper (solver, delayed, dom, other); - delay_watching_hyper (solver, delayed, other, dom); - - kissat_delay_watching_large (solver, delayed, - not_lit, other, ref); - - LOGREF (ref, "unwatching %s in", LOGLIT (not_lit)); - q -= 2; - } - else - kissat_fast_assign_reference (solver, values, - assigned, other, ref, c); - ticks++; } -#endif else - { - assert (replacement_value < 0); - kissat_fast_assign_reference (solver, values, - assigned, other, ref, c); - ticks++; - } + kissat_fast_assign_reference (solver, values, + assigned, other, ref, c); + ticks++; + } +#endif + else + { + assert (replacement_value < 0); + kissat_fast_assign_reference (solver, values, + assigned, other, ref, c); + ticks++; } } } @@ -309,9 +338,9 @@ kissat_update_conflicts_and_trail (kissat * solver, if (conflict) { INC (conflicts); - LOG (PROPAGATION_TYPE " propagation on root-level failed"); if (!solver->level) { + LOG (PROPAGATION_TYPE " propagation on root-level failed"); solver->inconsistent = true; CHECK_AND_ADD_EMPTY (); ADD_EMPTY_TO_PROOF (); diff --git a/src/propsearch.c b/src/propsearch.c index 29cf3f9e..d80c97bb 100644 --- a/src/propsearch.c +++ b/src/propsearch.c @@ -1,3 +1,4 @@ +#include "bump.h" #include "fastassign.h" #include "propsearch.h" #include "trail.h" @@ -60,6 +61,8 @@ kissat_search_propagate (kissat * solver) clause *conflict = search_propagate (solver); update_search_propagation_statistics (solver, saved_propagate); kissat_update_conflicts_and_trail (solver, conflict, true); + if (solver->stable && solver->branching) + kissat_bump_propagated (solver); STOP (propagate); diff --git a/src/reduce.c b/src/reduce.c index 1a36b3db..88e7b2da 100644 --- a/src/reduce.c +++ b/src/reduce.c @@ -191,17 +191,6 @@ compacting (kissat * solver) return compact; } -static void -force_restart_before_reduction (kissat * solver) -{ - if (!GET_OPTION (reducerestart)) - return; - if (!solver->stable && (GET_OPTION (reducerestart) < 2)) - return; - LOG ("forcing restart before reduction"); - kissat_restart_and_flush_trail (solver); -} - int kissat_reduce (kissat * solver) { @@ -210,7 +199,6 @@ kissat_reduce (kissat * solver) kissat_phase (solver, "reduce", GET (reductions), "reduce limit %" PRIu64 " hit after %" PRIu64 " conflicts", solver->limits.reduce.conflicts, CONFLICTS); - force_restart_before_reduction (solver); bool compact = compacting (solver); reference start = compact ? 0 : solver->first_reducible; if (start != INVALID_REF) diff --git a/src/rephase.c b/src/rephase.c index f7c41ada..2e4ad439 100644 --- a/src/rephase.c +++ b/src/rephase.c @@ -152,9 +152,9 @@ reset_phases (kissat * solver) // Since 'enabled.rephase' is true one of the rephase methods is enabled. // However 'rephasewalking' could be the only one and the derived 'walking' - // depends also on the size of the formula, i.e., 'kissat_walking' could - // return 'false'. As a consequence there is no candidate if only the - // 'rephasewalking' is true but the formula is too big. + // depends also on the size of the formula. As a consequence there is no + // candidate if only the option 'rephasewalking' is true but the formula is + // too big in which case however 'kissat_walking' and 'walking' are false. // if (candidates) { @@ -185,7 +185,7 @@ reset_phases (kissat * solver) solver->rephased.last = type; LOG ("copying saved phases as target phases"); memcpy (solver->phases.target, solver->phases.saved, VARS); - UPDATE_CONFLICT_LIMIT (rephase, rephased, NLOGNLOGNLOGN, false); + UPDATE_CONFLICT_LIMIT (rephase, rephased, NLOG3N, false); kissat_reset_target_assigned (solver); if (type == 'B') kissat_reset_best_assigned (solver); diff --git a/src/resize.c b/src/resize.c index 82928853..a246262f 100644 --- a/src/resize.c +++ b/src/resize.c @@ -62,6 +62,7 @@ kissat_increase_size (kissat * solver, unsigned new_size) FORMAT_BYTES (kissat_allocated (solver)), old_size, new_size); #endif CREALLOC_VARIABLE_INDEXED (assigned, assigned); + CREALLOC_VARIABLE_INDEXED (uint64_t, conflicted); CREALLOC_VARIABLE_INDEXED (flags, flags); NREALLOC_VARIABLE_INDEXED (links, links); @@ -71,7 +72,9 @@ kissat_increase_size (kissat * solver, unsigned new_size) reallocate_trail (solver, old_size, new_size); - kissat_resize_heap (solver, &solver->scores, new_size); + for (all_scores (scores)) + kissat_resize_heap (solver, scores, new_size); + kissat_increase_phases (solver, new_size); solver->size = new_size; @@ -94,6 +97,7 @@ kissat_decrease_size (kissat * solver) #endif NREALLOC_VARIABLE_INDEXED (assigned, assigned); + NREALLOC_VARIABLE_INDEXED (uint64_t, conflicted); NREALLOC_VARIABLE_INDEXED (flags, flags); NREALLOC_VARIABLE_INDEXED (links, links); @@ -103,7 +107,9 @@ kissat_decrease_size (kissat * solver) reallocate_trail (solver, old_size, new_size); - kissat_resize_heap (solver, &solver->scores, new_size); + for (all_scores (scores)) + kissat_resize_heap (solver, scores, new_size); + kissat_decrease_phases (solver, new_size); solver->size = new_size; diff --git a/src/resolve.c b/src/resolve.c index 0dd87e7b..cfb6fdc1 100644 --- a/src/resolve.c +++ b/src/resolve.c @@ -9,7 +9,7 @@ #include static inline unsigned -occurrences_literal (kissat * solver, unsigned lit, bool * update) +occurrences_literal (kissat * solver, unsigned lit, bool *update) { assert (!solver->watching); @@ -18,7 +18,7 @@ occurrences_literal (kissat * solver, unsigned lit, bool * update) const size_t size_watches = SIZE_WATCHES (*watches); LOG ("literal %s has %zu watches", LOGLIT (lit), size_watches); #endif - const unsigned clslim = solver->bounds.eliminate.clause_size; + const unsigned clslim = GET_OPTION (eliminateclslim); watch *const begin = BEGIN_WATCHES (*watches), *q = begin; const watch *const end = END_WATCHES (*watches), *p = q; @@ -118,7 +118,7 @@ generate_resolvents (kissat * solver, unsigned lit, const value *const values = solver->values; value *const marks = solver->marks; - const unsigned clslim = solver->bounds.eliminate.clause_size; + const unsigned clslim = GET_OPTION (eliminateclslim); for (all_stack (watch, watch0, *watches0)) { @@ -143,7 +143,7 @@ generate_resolvents (kissat * solver, unsigned lit, { first_antecedent_satisfied = true; if (c != &tmp0) - kissat_eliminate_clause (solver, c, other); + kissat_mark_clause_as_garbage (solver, c); break; } } @@ -191,7 +191,7 @@ generate_resolvents (kissat * solver, unsigned lit, if (value > 0) { if (d != &tmp1) - kissat_eliminate_clause (solver, d, other); + kissat_mark_clause_as_garbage (solver, d); resolvent_satisfied_or_tautological = true; break; } @@ -316,16 +316,16 @@ kissat_generate_resolvents (kissat * solver, unsigned idx, unsigned *lit_ptr) SWAP (size_t, pos_count, neg_count); } - const unsigned occlim = solver->bounds.eliminate.occurrences; - if (pos_count && neg_count > occlim) + const unsigned occlim = GET_OPTION (eliminateocclim); + limit = pos_count + (uint64_t) neg_count; + + if (pos_count && limit > occlim) { LOG ("no elimination of variable %u " - "since its literal %s has %u > %u occurrences", - idx, LOGLIT (not_lit), neg_count, occlim); + "since it has %" PRIu64 " > %u occurrences", idx, limit, occlim); return false; } - limit = pos_count + (uint64_t) neg_count; if (pos_count) { const uint64_t bound = solver->bounds.eliminate.additional_clauses; @@ -403,11 +403,8 @@ kissat_generate_resolvents (kissat * solver, unsigned idx, unsigned *lit_ptr) if (failed) { - const unsigned idx = IDX (lit); - LOG ("elimination of %s failed", LOGVAR (idx)); + LOG ("elimination of %s failed", LOGVAR (IDX (lit))); CLEAR_STACK (solver->resolvents); - if (update) - kissat_update_variable_score (solver, &solver->schedule, idx); } LOG ("resolved %" PRIu64 " resolvents", resolved); diff --git a/src/resources.c b/src/resources.c index 8feb4c15..0ebf1713 100644 --- a/src/resources.c +++ b/src/resources.c @@ -18,6 +18,7 @@ kissat_wall_clock_time (void) #include "utilities.h" #include +#include #include #include #include @@ -83,7 +84,12 @@ kissat_print_resources (kissat * solver) "max-allocated:", max_allocated, "bytes", kissat_percent (max_allocated, rss)); #endif - printf ("c process-time: %30s %18.2f seconds\n", FORMAT_TIME (t), t); + { + format buffer; + memset (&buffer, 0, sizeof buffer); + printf ("c process-time: %30s %18.2f seconds\n", + kissat_format_time (&buffer, t), t); + } fflush (stdout); } diff --git a/src/restart.c b/src/restart.c index 097d7a1f..3e3bc3c7 100644 --- a/src/restart.c +++ b/src/restart.c @@ -1,9 +1,10 @@ #include "backtrack.h" +#include "branching.h" #include "bump.h" #include "decide.h" #include "internal.h" -#include "limits.h" #include "logging.h" +#include "kimits.h" #include "print.h" #include "reluctant.h" #include "report.h" @@ -54,7 +55,7 @@ reuse_stable_trail (kissat * solver) { const unsigned next_idx = kissat_next_decision_variable (solver); const struct assigned *assigned = solver->assigned; - const heap *const scores = &solver->scores; + const heap *const scores = SCORES; const unsigned next_idx_score = kissat_get_heap_score (scores, next_idx); LOG ("next decision variable score %u", next_idx_score); double decision_score = MAX_SCORE; @@ -130,7 +131,10 @@ reuse_trail (kissat * solver) assert (solver->level); assert (!EMPTY_STACK (solver->trail)); - if (!GET_OPTION (restartreusetrail)) + const int option = GET_OPTION (reusetrail); + if (!option) + return 0; + if (option < 2 && solver->stable) return 0; unsigned res; @@ -179,6 +183,8 @@ kissat_restart (kissat * solver) kissat_backtrack_in_consistent_state (solver, level); if (!solver->stable) kissat_new_focused_restart_limit (solver); + else if (kissat_toggle_branching (solver)) + kissat_update_scores (solver); REPORT (1, 'R'); STOP (restart); } diff --git a/src/search.c b/src/search.c index 5c305930..776bc747 100644 --- a/src/search.c +++ b/src/search.c @@ -1,4 +1,5 @@ #include "analyze.h" +#include "branching.h" #include "bump.h" #include "decide.h" #include "eliminate.h" @@ -35,8 +36,14 @@ start_search (kissat * solver) kissat_init_averages (solver, &AVERAGES); + if (GET_OPTION (stable)) + kissat_init_branching (solver); + if (solver->stable) - kissat_init_reluctant (solver); + { + kissat_init_reluctant (solver); + kissat_update_scores (solver); + } kissat_init_limits (solver); diff --git a/src/shrink.c b/src/shrink.c index 9025620d..0c4eb253 100644 --- a/src/shrink.c +++ b/src/shrink.c @@ -210,7 +210,7 @@ shrink_along_binary (kissat * solver, assigned * assigned, reap * reap, static inline unsigned shrink_along_large (kissat * solver, assigned * assigned, reap * reap, unsigned level, unsigned max_trail, - unsigned uip, reference ref, bool * failed_ptr) + unsigned uip, reference ref, bool *failed_ptr) { unsigned open = 0; LOGREF2 (ref, "shrinking along %s reason", LOGLIT (uip)); @@ -238,7 +238,7 @@ shrink_along_large (kissat * solver, assigned * assigned, reap * reap, static inline unsigned shrink_along_reason (kissat * solver, assigned * assigned, reap * reap, unsigned level, unsigned uip, unsigned max_trail, - bool resolve_large_clauses, bool * failed_ptr) + bool resolve_large_clauses, bool *failed_ptr) { unsigned open = 0; const unsigned uip_idx = IDX (uip); diff --git a/src/statistics.c b/src/statistics.c index 2ae11ada..13371a71 100644 --- a/src/statistics.c +++ b/src/statistics.c @@ -155,6 +155,9 @@ kissat_statistics_print (kissat * solver, bool verbose) #define PCNT_EXTRACTED(NAME) \ PERCENT (NAME, gates_extracted) +#define PCNT_KITTEN_FLIP(NAME) \ + PERCENT (NAME, kitten_flip) + #define PCNT_KITTEN_SOLVED(NAME) \ PERCENT (NAME, kitten_solved) diff --git a/src/statistics.h b/src/statistics.h index 52a420ea..6362d3a3 100644 --- a/src/statistics.h +++ b/src/statistics.h @@ -9,7 +9,7 @@ METRIC( allocated_collected, 2, PCNT_RESIDENT_SET, "%", "resident set") \ METRIC( allocated_current, 2, PCNT_RESIDENT_SET, "%", "resident set") \ METRIC( allocated_max, 2, PCNT_RESIDENT_SET, "%", "resident set") \ -METRIC( ands_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( ands_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( ands_extracted, 1, PCNT_EXTRACTED, "%", "extracted") \ METRIC( arena_enlarged, 1, PCNT_ARENA_RESIZED, "%", "resize") \ METRIC( arena_garbage, 1, PCNT_RESIDENT_SET, "%", "resident set") \ @@ -50,7 +50,7 @@ METRIC( compacted, 1, PCNT_REDUCTIONS, "%", "reductions") \ COUNTER( conflicts, 0, PER_SECOND, 0, "per second") \ COUNTER( decisions, 0, PER_CONFLICT, 0, "per conflict") \ METRIC( definitions_checked, 1, PCNT_ELIM_ATTEMPTS, "%", "attempts") \ -METRIC( definitions_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( definitions_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( definitions_extracted, 1, PCNT_EXTRACTED, "%", "extracted") \ COUNTER( definition_units, 1, PCNT_VARIABLES, "%", "variables") \ METRIC( defragmentations, 1, CONF_INT, "", "interval") \ @@ -59,12 +59,12 @@ METRIC( dense_propagations, 1, PCNT_PROPS, "%", "propagations") \ METRIC( dense_ticks, 1, PCNT_TICKS, "%", "ticks") \ METRIC( duplicated, 1, PCNT_CLS_ADDED, "%", "added") \ METRIC( eager_subsumed, 1, PCNT_SUB, "%", "subsumed") \ -STATISTIC( eliminated, 1, PCNT_VARIABLES, "%", "variables") \ +COUNTER( eliminated, 1, PCNT_VARIABLES, "%", "variables") \ COUNTER( eliminations, 2, CONF_INT, "", "interval") \ -METRIC( eliminate_attempted, 1, PER_VARIABLE, 0, "per variable") \ +STATISTIC( eliminate_attempted, 1, PER_VARIABLE, 0, "per variable") \ COUNTER( eliminate_resolutions, 2, PER_SECOND, 0, "per second") \ COUNTER( eliminate_units, 1, PCNT_VARIABLES, "%", "variables") \ -METRIC( equivalences_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( equivalences_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( equivalences_extracted, 1, PCNT_EXTRACTED, "%", "extracted") \ METRIC( extensions, 1, PCNT_SEARCHES, "%", "searches") \ METRIC( failed_computations, 1, CONF_INT, "", "interval") \ @@ -86,28 +86,30 @@ COUNTER( forward_subsumed, 1, PCNT_SUB, "%", "subsumed") \ METRIC( forward_subsumptions, 1, CONF_INT, "", "interval") \ METRIC( garbage_collections, 2, CONF_INT, "", "interval") \ METRIC( gates_checked, 1, PCNT_ELIM_ATTEMPTS, "%", "attempts") \ -METRIC( gates_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( gates_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( gates_extracted, 1, PCNT_ELIM_ATTEMPTS, "%", "attempts") \ METRIC( hyper_binaries, 2, PCNT_REDUNDANT_CLAUSES, "%", "redundant") \ METRIC( hyper_binary_resolved, 1, NO_SECONDARY, 0, 0) \ METRIC( hyper_propagations, 2, PCNT_PROPS, "%", "propagations") \ -METRIC( hyper_ternaries, 2, PCNT_REDUNDANT_CLAUSES, "%", "redundant") \ -METRIC( hyper_ternary2_resolved, 2, PCNT_TRN_RESOLVED, "%", "resolved") \ -METRIC( hyper_ternary3_resolved, 2, PCNT_TRN_RESOLVED, "%", "resolved") \ -METRIC( hyper_ternary_phases, 1, CONF_INT, "", "interval") \ -METRIC( hyper_ternary_resolutions, 2, PCNT_TRN_RESOLVED, "", "per resolved") \ -METRIC( hyper_ternary_resolved, 1, NO_SECONDARY, 0, 0) \ +COUNTER( hyper_ternaries, 1, PCNT_REDUNDANT_CLAUSES, "%", "redundant") \ +COUNTER( hyper_ternary2_resolved, 2, PCNT_TRN_RESOLVED, "%", "resolved") \ +COUNTER( hyper_ternary3_resolved, 2, PCNT_TRN_RESOLVED, "%", "resolved") \ +COUNTER( hyper_ternary_phases, 1, CONF_INT, "", "interval") \ +COUNTER( hyper_ternary_resolutions, 2, PCNT_TRN_RESOLVED, "", "per resolved") \ +COUNTER( hyper_ternary_resolved, 1, NO_SECONDARY, 0, 0) \ COUNTER( hyper_ternary_steps, 2, PER_TRN_RESOLVED, 0, "resolved") \ METRIC( hyper_ticks, 2, PCNT_TICKS, "%", "ticks") \ -METRIC( if_then_else_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( if_then_else_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( if_then_else_extracted, 1, PCNT_EXTRACTED, "%", "extracted") \ METRIC( initial_decisions, 1, PCNT_DECISIONS, "%", "decisions") \ COUNTER( kitten_conflicts, 1, PER_KITTEN_SOLVED, 0, "per solved") \ COUNTER( kitten_decisions, 1, PER_KITTEN_SOLVED, 0, "per solved") \ COUNTER( kitten_propagations, 1, PER_KITTEN_SOLVED, 0, "per solved") \ +COUNTER( kitten_flip, 1, NO_SECONDARY, 0, 0) \ +COUNTER( kitten_flipped, 1, PCNT_KITTEN_FLIP, "%", "per flip") \ COUNTER( kitten_sat, 1, PCNT_KITTEN_SOLVED, "%", "solved") \ COUNTER( kitten_solved, 1, NO_SECONDARY, 0, 0) \ -COUNTER( kitten_ticks, 1, PER_KITTEN_PROP, 0, "per propagation") \ +COUNTER( kitten_ticks, 1, PER_KITTEN_PROP, 0, "per prop") \ COUNTER( kitten_unknown, 1, PCNT_KITTEN_SOLVED, "%", "solved") \ COUNTER( kitten_unsat, 1, PCNT_KITTEN_SOLVED, "%", "solved") \ COUNTER( learned_units, 1, PCNT_VARIABLES, "%", "variables") \ @@ -137,7 +139,7 @@ COUNTER( reused_levels, 2, PER_REUSED_TRAIL, 0, "per reused") \ METRIC( saved_decisions, 1, PCNT_DECISIONS, "%", "decisions") \ COUNTER( searches, 2, CONF_INT, "", "interval") \ METRIC( search_propagations, 2, PCNT_PROPS, "%", "propagations") \ -COUNTER( search_ticks, 2, PCNT_TICKS, "%", "ticks") \ +COUNTER( search_ticks, 1, PCNT_TICKS, "%", "ticks") \ METRIC( sparse_garbage_collections, 2, PCNT_COLLECTIONS, "%", "collections") \ METRIC( stable_decisions, 1, PCNT_DECISIONS, "%", "decisions") \ METRIC( stable_modes, 2, CONF_INT, "", "interval") \ @@ -153,7 +155,7 @@ STATISTIC( substitutions, 2, CONF_INT, "", "interval") \ COUNTER( subsumed, 1, PCNT_SUBSUMPTION_CHECK, "%", "checks") \ COUNTER( sweep, 1, CONF_INT, "", "interval") \ COUNTER( sweep_completed, 0, SWEEPS_PER_COMPLETED, "", "sweeps") \ -COUNTER( sweep_equivalences, 0, PCNT_VARIABLES, "", "variables") \ +COUNTER( sweep_equivalences, 0, PCNT_VARIABLES, "%", "variables") \ COUNTER( sweep_sat, 0, PCNT_SWEEP_SOLVED, "%", "sweep_solved") \ COUNTER( sweep_solved, 0, PCNT_KITTEN_SOLVED, "%", "kitten_solved") \ COUNTER( sweep_units, 0, PCNT_VARIABLES, "%", "variables") \ @@ -176,29 +178,30 @@ COUNTER( variables_removed, 2, PER_VARIABLE, 0, "variables") \ METRIC( vectors_defrags_needed, 1, PCNT_DEFRAGS, "%", "defrags") \ METRIC( vectors_enlarged, 2, CONF_INT, "", "interval") \ STATISTIC( vivifications, 2, CONF_INT, "", "interval") \ -METRIC( vivified, 1, PCNT_VIVIFY_CHECK, "%", "checks") \ +STATISTIC( vivified, 1, PCNT_VIVIFY_CHECK, "%", "checks") \ STATISTIC( vivify_checks, 2, PER_VIVIFICATION, "", "per vivify") \ -METRIC( vivify_implied, 1, PCNT_VIVIFIED, "%", "vivified") \ -METRIC( vivify_irredundant, 1, PCNT_VIVIFIED, "%", "vivified") \ -METRIC( vivify_probes, 1, PER_VIVIFY_CHECK, "", "checks") \ -METRIC( vivify_propagations, 2, PCNT_PROPS, "%", "propagations") \ -METRIC( vivify_redundant, 1, PCNT_VIVIFIED, "%", "vivified") \ -METRIC( vivify_reused, 1, PCNT_VIVIFY_PROBES, "%", "probes") \ -METRIC( vivify_strengthened, 1, PCNT_STR, "%", "strengthened") \ -METRIC( vivify_str_irr, 1, PCNT_VIVIFY_STR, "%", "strengthened") \ -METRIC( vivify_str_red, 1, PCNT_VIVIFY_STR, "%", "strengthened") \ -METRIC( vivify_sub_irr, 1, PCNT_VIVIFY_SUB, "%", "subsumed") \ -METRIC( vivify_sub_red, 1, PCNT_VIVIFY_SUB, "%", "subsumed") \ -METRIC( vivify_subsumed, 1, PCNT_SUB, "%", "subsumed") \ -METRIC( vivify_ticks, 2, PCNT_TICKS, "%", "ticks") \ +STATISTIC( vivify_implied, 1, PCNT_VIVIFIED, "%", "vivified") \ +STATISTIC( vivify_irredundant, 1, PCNT_VIVIFIED, "%", "vivified") \ +STATISTIC( vivify_probes, 1, PER_VIVIFY_CHECK, "", "checks") \ +STATISTIC( vivify_propagations, 2, PCNT_PROPS, "%", "propagations") \ +STATISTIC( vivify_redundant, 1, PCNT_VIVIFIED, "%", "vivified") \ +STATISTIC( vivify_reused, 1, PCNT_VIVIFY_PROBES, "%", "probes") \ +STATISTIC( vivify_strengthened, 1, PCNT_STR, "%", "strengthened") \ +STATISTIC( vivify_str_irr, 1, PCNT_VIVIFY_STR, "%", "strengthened") \ +STATISTIC( vivify_str_red, 1, PCNT_VIVIFY_STR, "%", "strengthened") \ +STATISTIC( vivify_sub_irr, 1, PCNT_VIVIFY_SUB, "%", "subsumed") \ +STATISTIC( vivify_sub_red, 1, PCNT_VIVIFY_SUB, "%", "subsumed") \ +STATISTIC( vivify_subsumed, 1, PCNT_SUB, "%", "subsumed") \ +STATISTIC( vivify_ticks, 2, PCNT_TICKS, "%", "ticks") \ COUNTER( vivify_units, 1, PCNT_VARIABLES, "%", "variables") \ METRIC( walk_decisions, 1, PCNT_WALKS, "%", "walks") \ METRIC( walk_improved, 1, PCNT_WALKS, "%", "walks") \ METRIC( walk_previous, 1, PCNT_WALKS, "%", "walks") \ COUNTER( walks, 1, CONF_INT, "", "interval") \ COUNTER( walk_steps, 2, PER_FLIPPED, 0, "per flipped") \ +COUNTER( warmups, 1, PCNT_WALKS, "%", "walks") \ METRIC( weakened, 1, PCNT_CLS_ADDED, "%", "added") \ -METRIC( xors_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ +STATISTIC( xors_eliminated, 1, PCNT_ELIMINATED, "%", "eliminated") \ METRIC( xors_extracted, 1, PCNT_EXTRACTED, "%", "extracted") \ /*------------------------------------------------------------------------*/ diff --git a/src/strengthen.c b/src/strengthen.c index 742b0d1d..227e7819 100644 --- a/src/strengthen.c +++ b/src/strengthen.c @@ -174,7 +174,16 @@ kissat_on_the_fly_subsume (kissat * solver, clause * c, clause * d) kissat_mark_clause_as_garbage (solver, d); INC (on_the_fly_subsumed); if (d->redundant) - return; + { + if (c->redundant && !c->keep) + { + if (c->glue > d->glue) + kissat_promote_clause (solver, c, d->glue); + if (c->glue <= (unsigned) GET_OPTION (tier2) && c->used <= 1) + c->used = 2; + } + return; + } if (!c->redundant) return; if (c->size == 2) diff --git a/src/substitute.c b/src/substitute.c index 664996f2..f3ff1731 100644 --- a/src/substitute.c +++ b/src/substitute.c @@ -266,7 +266,7 @@ add_representative_equivalences (kissat * solver, unsigned *repr) static void remove_representative_equivalences (kissat * solver, - unsigned *repr, bool * eliminate) + unsigned *repr, bool *eliminate) { if (!solver->inconsistent) { diff --git a/src/sweep.c b/src/sweep.c index 559674b8..57c914c7 100644 --- a/src/sweep.c +++ b/src/sweep.c @@ -3,40 +3,49 @@ #include "logging.h" #include "kitten.h" #include "print.h" +#include "promote.h" #include "propdense.h" +#include "proprobe.h" #include "report.h" +#include "rank.h" #include "sweep.h" #include "terminate.h" #include +#include typedef struct sweeper sweeper; struct sweeper { kissat *solver; - unsigned encoded; unsigned *depths; unsigned *reprs; + unsigned *prev; + unsigned *next; + unsigned first; + unsigned last; + unsigned encoded; + unsigned save; unsigneds vars; references refs; unsigneds clause; - unsigneds schedule; unsigneds backbone; unsigneds partition; - unsigneds core; - uint64_t limit; - uint64_t solved; + unsigneds core[2]; + struct + { + uint64_t ticks; + unsigned clauses, depth, vars; + } limit; }; static int -sweep_solve (kissat * solver, sweeper * sweeper) +sweep_solve (sweeper * sweeper) { + kissat *solver = sweeper->solver; kitten *kitten = solver->kitten; - if ((sweeper->solved++) % 3) - kitten_flip_phases (kitten); - else - kitten_randomize_phases (kitten); + kitten_randomize_phases (kitten); INC (sweep_solved); int res = kitten_solve (kitten); if (res == 10) @@ -47,23 +56,25 @@ sweep_solve (kissat * solver, sweeper * sweeper) } static void -set_kitten_ticks_limit (kissat * solver, sweeper * sweeper) +set_kitten_ticks_limit (sweeper * sweeper) { uint64_t remaining = 0; - if (solver->statistics.kitten_ticks < sweeper->limit) - remaining = sweeper->limit - solver->statistics.kitten_ticks; + kissat *solver = sweeper->solver; + if (solver->statistics.kitten_ticks < sweeper->limit.ticks) + remaining = sweeper->limit.ticks - solver->statistics.kitten_ticks; LOG ("'kitten_ticks' remaining %" PRIu64, remaining); kitten_set_ticks_limit (solver->kitten, remaining); } static bool -kitten_ticks_limit_hit (kissat * solver, sweeper * sweeper, const char *when) +kitten_ticks_limit_hit (sweeper * sweeper, const char *when) { - if (solver->statistics.kitten_ticks >= sweeper->limit) + kissat *solver = sweeper->solver; + if (solver->statistics.kitten_ticks >= sweeper->limit.ticks) { LOG ("'kitten_ticks' limit of %" PRIu64 " ticks hit after %" PRIu64 " ticks during %s", - sweeper->limit, solver->statistics.kitten_ticks, when); + sweeper->limit.ticks, solver->statistics.kitten_ticks, when); return true; } #ifndef LOGGING @@ -77,32 +88,78 @@ init_sweeper (kissat * solver, sweeper * sweeper) { sweeper->solver = solver; sweeper->encoded = 0; - sweeper->solved = 0; CALLOC (sweeper->depths, VARS); - CALLOC (sweeper->reprs, LITS); + NALLOC (sweeper->reprs, LITS); for (all_literals (lit)) sweeper->reprs[lit] = lit; + NALLOC (sweeper->prev, VARS); + NALLOC (sweeper->next, VARS); + for (all_variables (idx)) + sweeper->prev[idx] = sweeper->next[idx] = INVALID_IDX; + sweeper->first = sweeper->last = INVALID_IDX; INIT_STACK (sweeper->vars); INIT_STACK (sweeper->refs); INIT_STACK (sweeper->clause); - INIT_STACK (sweeper->schedule); INIT_STACK (sweeper->backbone); INIT_STACK (sweeper->partition); - INIT_STACK (sweeper->core); + INIT_STACK (sweeper->core[0]); + INIT_STACK (sweeper->core[1]); assert (!solver->kitten); solver->kitten = kitten_embedded (solver); kitten_track_antecedents (solver->kitten); kissat_enter_dense_mode (solver, 0, 0); kissat_connect_irredundant_large_clauses (solver); - SET_EFFORT_LIMIT (limit, sweep, kitten_ticks, - kissat_linear (1 + solver->active)); - sweeper->limit = limit; - set_kitten_ticks_limit (solver, sweeper); + + unsigned completed = solver->statistics.sweep_completed; + if (completed > 32) + completed = 32; + + uint64_t vars_limit = GET_OPTION (sweepvars); + vars_limit <<= completed; + const unsigned max_vars_limit = GET_OPTION (sweepmaxvars); + if (vars_limit > max_vars_limit) + vars_limit = max_vars_limit; + sweeper->limit.vars = vars_limit; + kissat_extremely_verbose (solver, "sweeper variable limit %u", + sweeper->limit.vars); + + uint64_t depth_limit = solver->statistics.sweep_completed; + depth_limit += GET_OPTION (sweepdepth); + const unsigned max_depth = GET_OPTION (sweepmaxdepth); + if (depth_limit > max_depth) + depth_limit = max_depth; + sweeper->limit.depth = depth_limit; + kissat_extremely_verbose (solver, "sweeper depth limit %u", + sweeper->limit.depth); + + uint64_t clause_limit = GET_OPTION (sweepclauses); + clause_limit <<= completed; + const unsigned max_clause_limit = GET_OPTION (sweepmaxclauses); + if (clause_limit > max_clause_limit) + clause_limit = max_clause_limit; + sweeper->limit.clauses = clause_limit; + kissat_extremely_verbose (solver, "sweeper clause limit %u", + sweeper->limit.clauses); + + SET_EFFORT_LIMIT (ticks_limit, sweep, kitten_ticks, + 10 * (1 + solver->active)); + unsigned boost = GET_OPTION (sweepboost); + assert (solver->statistics.sweep >= completed); + boost >>= solver->statistics.sweep - completed; + if (boost) + { + kissat_extremely_verbose (solver, "sweeping boost %u", boost); + ticks_limit *= boost; + } + sweeper->limit.ticks = ticks_limit; + set_kitten_ticks_limit (sweeper); } static unsigned -release_sweeper (kissat * solver, sweeper * sweeper) +release_sweeper (sweeper * sweeper) { + kissat *solver = sweeper->solver; + unsigned merged = 0; for (all_variables (idx)) { @@ -114,13 +171,15 @@ release_sweeper (kissat * solver, sweeper * sweeper) } DEALLOC (sweeper->depths, VARS); DEALLOC (sweeper->reprs, LITS); + DEALLOC (sweeper->prev, VARS); + DEALLOC (sweeper->next, VARS); RELEASE_STACK (sweeper->vars); RELEASE_STACK (sweeper->refs); RELEASE_STACK (sweeper->clause); - RELEASE_STACK (sweeper->schedule); RELEASE_STACK (sweeper->backbone); RELEASE_STACK (sweeper->partition); - RELEASE_STACK (sweeper->core); + RELEASE_STACK (sweeper->core[0]); + RELEASE_STACK (sweeper->core[1]); kitten_release (solver->kitten); solver->kitten = 0; kissat_resume_sparse_mode (solver, false, 0, 0); @@ -128,8 +187,9 @@ release_sweeper (kissat * solver, sweeper * sweeper) } static void -clear_sweeper (kissat * solver, sweeper * sweeper) +clear_sweeper (sweeper * sweeper) { + kissat *solver = sweeper->solver; LOG ("clearing sweeping environment"); kitten_clear (solver->kitten); kitten_track_antecedents (solver->kitten); @@ -149,11 +209,11 @@ clear_sweeper (kissat * solver, sweeper * sweeper) CLEAR_STACK (sweeper->backbone); CLEAR_STACK (sweeper->partition); sweeper->encoded = 0; - set_kitten_ticks_limit (solver, sweeper); + set_kitten_ticks_limit (sweeper); } static unsigned -sweep_repr (kissat * solver, sweeper * sweeper, unsigned lit) +sweep_repr (sweeper * sweeper, unsigned lit) { unsigned res; { @@ -163,6 +223,9 @@ sweep_repr (kissat * solver, sweeper * sweeper, unsigned lit) } if (res == lit) return res; +#if defined(LOGGING) || !defined(NDEBUG) + kissat *solver = sweeper->solver; +#endif LOG ("sweeping repr[%s] = %s", LOGLIT (lit), LOGLIT (res)); { const unsigned not_res = NOT (res); @@ -176,42 +239,46 @@ sweep_repr (kissat * solver, sweeper * sweeper, unsigned lit) } assert (sweeper->reprs[NOT (prev)] == not_res); } -#ifndef LOGGING - (void) solver; -#endif return res; } static void -add_literal_to_environment (kissat * solver, sweeper * sweeper, - unsigned depth, unsigned lit) +add_literal_to_environment (sweeper * sweeper, unsigned depth, unsigned lit) { - for (;;) - { - const unsigned idx = IDX (lit); - if (!sweeper->depths[idx]) - { - assert (depth < UINT_MAX); - sweeper->depths[idx] = depth + 1; - PUSH_STACK (sweeper->vars, idx); - LOG ("sweeping[%u] adding literal %s", depth, LOGLIT (lit)); - } - const unsigned repr = sweep_repr (solver, sweeper, lit); - if (repr == lit) - break; - const unsigned not_lit = NOT (lit); - const unsigned not_repr = NOT (repr); - LOG ("adding equivalence %s = %s", LOGLIT (lit), LOGLIT (repr)); - kitten_binary (solver->kitten, not_lit, repr); - kitten_binary (solver->kitten, lit, not_repr); - lit = repr; - } + const unsigned repr = sweep_repr (sweeper, lit); + if (repr != lit) + return; + kissat *solver = sweeper->solver; + const unsigned idx = IDX (lit); + if (sweeper->depths[idx]) + return; + assert (depth < UINT_MAX); + sweeper->depths[idx] = depth + 1; + PUSH_STACK (sweeper->vars, idx); + LOG ("sweeping[%u] adding literal %s", depth, LOGLIT (lit)); } static void -sweep_binary (kissat * solver, sweeper * sweeper, - unsigned depth, unsigned lit, unsigned other) +sweep_clause (sweeper * sweeper, unsigned depth) { + kissat *solver = sweeper->solver; + assert (SIZE_STACK (sweeper->clause) > 1); + for (all_stack (unsigned, lit, sweeper->clause)) + add_literal_to_environment (sweeper, depth, lit); + kitten_clause (solver->kitten, SIZE_STACK (sweeper->clause), + BEGIN_STACK (sweeper->clause)); + CLEAR_STACK (sweeper->clause); + sweeper->encoded++; +} + +static void +sweep_binary (sweeper * sweeper, unsigned depth, unsigned lit, unsigned other) +{ + if (sweep_repr (sweeper, lit) != lit) + return; + if (sweep_repr (sweeper, other) != other) + return; + kissat *solver = sweeper->solver; LOGBINARY (lit, other, "sweeping[%u]", depth); value *values = solver->values; assert (!values[lit]); @@ -224,23 +291,25 @@ sweep_binary (kissat * solver, sweeper * sweeper, const unsigned *depths = sweeper->depths; const unsigned other_idx = IDX (other); const unsigned other_depth = depths[other_idx]; - if (other_depth < depth) + const unsigned lit_idx = IDX (lit); + const unsigned lit_depth = depths[lit_idx]; + if (other_depth && other_depth < lit_depth) { LOGBINARY (lit, other, "skipping depth %u copied", other_depth); return; } assert (!other_value); - add_literal_to_environment (solver, sweeper, depth, lit); - add_literal_to_environment (solver, sweeper, depth, other); - kitten_binary (solver->kitten, lit, other); - sweeper->encoded++; + assert (EMPTY_STACK (sweeper->clause)); + PUSH_STACK (sweeper->clause, lit); + PUSH_STACK (sweeper->clause, other); + sweep_clause (sweeper, depth); } static void -sweep_reference (kissat * solver, sweeper * sweeper, - unsigned depth, reference ref) +sweep_reference (sweeper * sweeper, unsigned depth, reference ref) { assert (EMPTY_STACK (sweeper->clause)); + kissat *solver = sweeper->solver; clause *c = kissat_dereference_clause (solver, ref); if (c->sweeped) return; @@ -263,28 +332,22 @@ sweep_reference (kissat * solver, sweeper * sweeper, } PUSH_STACK (sweeper->refs, ref); c->sweeped = true; - assert (SIZE_STACK (sweeper->clause) > 1); - for (all_stack (unsigned, repr, sweeper->clause)) - add_literal_to_environment (solver, sweeper, depth, repr); - kitten_clause (solver->kitten, SIZE_STACK (sweeper->clause), - BEGIN_STACK (sweeper->clause)); - CLEAR_STACK (sweeper->clause); - sweeper->encoded++; + sweep_clause (sweeper, depth); } static void -add_core_clause (void *state, bool learned, size_t size, const unsigned *lits) +save_core_clause (void *state, bool learned, + size_t size, const unsigned *lits) { sweeper *sweeper = state; kissat *solver = sweeper->solver; if (solver->inconsistent) return; const value *const values = solver->values; - unsigned unit = INVALID_LIT; - bool satisfied = false; - unsigned non_false = 0; - size_t saved = SIZE_STACK (sweeper->core); + unsigneds *core = sweeper->core + sweeper->save; + size_t saved = SIZE_STACK (*core); const unsigned *end = lits + size; + unsigned non_false = 0; for (const unsigned *p = lits; p != end; p++) { const unsigned lit = *p; @@ -292,94 +355,173 @@ add_core_clause (void *state, bool learned, size_t size, const unsigned *lits) if (value > 0) { LOGLITS (size, lits, "extracted %s satisfied lemma", LOGLIT (lit)); - satisfied = true; - break; + RESIZE_STACK (*core, saved); + return; } - PUSH_STACK (sweeper->core, lit); + PUSH_STACK (*core, lit); if (value < 0) continue; - non_false++; - unit = lit; + if (!learned && ++non_false > 1) + { + LOGLITS (size, lits, "ignoring extracted original clause"); + RESIZE_STACK (*core, saved); + return; + } } +#ifdef LOGGING + unsigned *saved_lits = BEGIN_STACK (*core) + saved; + size_t saved_size = SIZE_STACK (*core) - saved; + LOGLITS (saved_size, saved_lits, "saved core[%u]", sweeper->save); +#endif + PUSH_STACK (*core, INVALID_LIT); +} - bool reset = true; +static void +add_core (sweeper * sweeper, unsigned core_idx) +{ + kissat *solver = sweeper->solver; + if (solver->inconsistent) + return; + LOG ("check and add extracted core[%u] lemmas to proof", core_idx); + assert (core_idx == 0 || core_idx == 1); + unsigneds *core = sweeper->core + core_idx; + const value *const values = solver->values; + + unsigned *q = BEGIN_STACK (*core); + const unsigned *const end_core = END_STACK (*core), *p = q; - if (satisfied) - ; - else if (!non_false) + while (p != end_core) { - if (!solver->inconsistent) + const unsigned *c = p; + while (*p != INVALID_LIT) + p++; +#ifdef LOGGING + size_t old_size = p - c; + LOGLITS (old_size, c, "simplifying extracted core[%u] lemma", core_idx); +#endif + bool satisfied = false; + unsigned unit = INVALID_LIT; + + unsigned *d = q; + + for (const unsigned *l = c; !satisfied && l != p; l++) + { + const unsigned lit = *l; + const value value = values[lit]; + if (value > 0) + { + satisfied = true; + break; + } + if (!value) + unit = *q++ = lit; + } + + size_t new_size = q - d; + p++; + + if (satisfied) + { + q = d; + LOG ("not adding satisfied clause"); + continue; + } + + if (!new_size) { LOG ("sweeping produced empty clause"); CHECK_AND_ADD_EMPTY (); ADD_EMPTY_TO_PROOF (); solver->inconsistent = true; + CLEAR_STACK (*core); + return; } + + if (new_size == 1) + { + q = d; + assert (unit != INVALID_LIT); + LOG ("sweeping produced unit %s", LOGLIT (unit)); + CHECK_AND_ADD_UNIT (unit); + ADD_UNIT_TO_PROOF (unit); + kissat_assign_unit (solver, unit, "sweeping backbone reason"); + INC (sweep_units); + continue; + } + + *q++ = INVALID_LIT; + + assert (new_size > 1); + LOGLITS (new_size, d, "adding extracted core[%u] lemma", core_idx); + CHECK_AND_ADD_LITS (new_size, d); + ADD_LITS_TO_PROOF (new_size, d); } - else if (non_false == 1) - { - assert (unit != INVALID_LIT); - LOGLITS (size, lits, "unit %s forcing %s", LOGLIT (unit), - (learned ? "extracted lemma" : "original")); - CHECK_AND_ADD_UNIT (unit); - ADD_UNIT_TO_PROOF (unit); - kissat_assign_unit (solver, unit, "sweeping backbone reason"); - INC (sweep_units); - } - else if (learned) - { - assert (non_false > 1); -#ifdef LOGGING - if (non_false == size) - LOGLITS (size, lits, "extracted lemma"); - else - LOGLITS (size, lits, "actual size %u extracted lemma", non_false); + SET_END_OF_STACK (*core, q); +#ifndef LOGGING + (void) core_idx; #endif - CHECK_AND_ADD_LITS (size, lits); - ADD_LITS_TO_PROOF (size, lits); - PUSH_STACK (sweeper->core, INVALID_LIT); - reset = false; - } - else - LOGLITS (size, lits, "skipping original"); - - if (reset) - RESIZE_STACK (sweeper->core, saved); } static void -add_core (kissat * solver, sweeper * sweeper) +save_core (sweeper * sweeper, unsigned core) { - LOG ("adding sub-solver core clauses"); - assert (EMPTY_STACK (sweeper->core)); + kissat *solver = sweeper->solver; + LOG ("saving extracted core[%u] lemmas", core); + assert (core == 0 || core == 1); + assert (EMPTY_STACK (sweeper->core[core])); + sweeper->save = core; kitten_compute_clausal_core (solver->kitten, 0); - kitten_traverse_core_clauses (solver->kitten, sweeper, add_core_clause); + kitten_traverse_core_clauses (solver->kitten, sweeper, save_core_clause); } static void -delete_core (kissat * solver, sweeper * sweeper) +clear_core (sweeper * sweeper, unsigned core_idx) { + kissat *solver = sweeper->solver; + if (solver->inconsistent) + return; +#if defined(LOGGING) || !defined(NDEBUG) || !defined(NPROOFS) + assert (core_idx == 0 || core_idx == 1); + LOG ("clearing core[%u] lemmas", core_idx); +#endif + unsigneds *core = sweeper->core + core_idx; #ifdef CHECKING_OR_PROVING LOG ("deleting sub-solver core clauses"); - const unsigned *const end = END_STACK (sweeper->core); - const unsigned *c = BEGIN_STACK (sweeper->core); + const unsigned *const end = END_STACK (*core); + const unsigned *c = BEGIN_STACK (*core); for (const unsigned *p = c; c != end; c = ++p) { while (*p != INVALID_LIT) p++; const size_t size = p - c; + assert (size > 1); REMOVE_CHECKER_LITS (size, c); DELETE_LITS_FROM_PROOF (size, c); } -#else - (void) solver; #endif - CLEAR_STACK (sweeper->core); + CLEAR_STACK (*core); +} + +static void +save_add_clear_core (sweeper * sweeper) +{ + save_core (sweeper, 0); + add_core (sweeper, 0); + clear_core (sweeper, 0); } +#define LOGBACKBONE(MESSAGE) \ + LOGLITSET (SIZE_STACK (sweeper->backbone), \ + BEGIN_STACK (sweeper->backbone), MESSAGE) + +#define LOGPARTITION(MESSAGE) \ + LOGLITPART (SIZE_STACK (sweeper->partition), \ + BEGIN_STACK (sweeper->partition), MESSAGE) + static void -init_backbone_and_partition (kissat * solver, sweeper * sweeper) +init_backbone_and_partition (sweeper * sweeper) { + kissat *solver = sweeper->solver; LOG ("initializing backbone and equivalent literals candidates"); for (all_stack (unsigned, idx, sweeper->vars)) { @@ -393,21 +535,24 @@ init_backbone_and_partition (kissat * solver, sweeper * sweeper) PUSH_STACK (sweeper->backbone, candidate); PUSH_STACK (sweeper->partition, candidate); } - LOG ("initialized %zu literals", SIZE_STACK (sweeper->backbone)); PUSH_STACK (sweeper->partition, INVALID_LIT); + + LOGBACKBONE ("initialized backbone candidates"); + LOGPARTITION ("initialized equivalence candidates"); } static void -sweep_empty_clause (kissat * solver, sweeper * sweeper) +sweep_empty_clause (sweeper * sweeper) { - assert (!solver->inconsistent); - add_core (solver, sweeper); - assert (solver->inconsistent); + assert (!sweeper->solver->inconsistent); + save_add_clear_core (sweeper); + assert (sweeper->solver->inconsistent); } static void -sweep_refine_partition (kissat * solver, sweeper * sweeper) +sweep_refine_partition (sweeper * sweeper) { + kissat *solver = sweeper->solver; LOG ("refining partition"); kitten *kitten = solver->kitten; unsigneds old_partition = sweeper->partition; @@ -425,7 +570,7 @@ sweep_refine_partition (kissat * solver, sweeper * sweeper) unsigned assigned_true = 0, other; for (q = p; (other = *q) != INVALID_LIT; q++) { - if (sweep_repr (solver, sweeper, other) != other) + if (sweep_repr (sweeper, other) != other) continue; if (values[other]) continue; @@ -466,7 +611,7 @@ sweep_refine_partition (kissat * solver, sweeper * sweeper) unsigned assigned_false = 0; for (q = p; (other = *q) != INVALID_LIT; q++) { - if (sweep_repr (solver, sweeper, other) != other) + if (sweep_repr (sweeper, other) != other) continue; if (values[other]) continue; @@ -502,19 +647,18 @@ sweep_refine_partition (kissat * solver, sweeper * sweeper) RELEASE_STACK (old_partition); sweeper->partition = new_partition; LOG ("refined %u classes into %u", old_classes, new_classes); + LOGPARTITION ("refined equivalence candidates"); } static void -sweep_refine_backbone (kissat * solver, sweeper * sweeper) +sweep_refine_backbone (sweeper * sweeper) { - LOG ("refining backbone"); + kissat *solver = sweeper->solver; + LOG ("refining backbone candidates"); const unsigned *const end = END_STACK (sweeper->backbone); unsigned *q = BEGIN_STACK (sweeper->backbone); const value *const values = solver->values; kitten *kitten = solver->kitten; -#ifdef LOGGING - size_t old_size = SIZE_STACK (sweeper->backbone); -#endif for (const unsigned *p = q; p != end; p++) { const unsigned lit = *p; @@ -527,146 +671,702 @@ sweep_refine_backbone (kissat * solver, sweeper * sweeper) *q++ = lit; } SET_END_OF_STACK (sweeper->backbone, q); -#ifdef LOGGING - size_t new_size = SIZE_STACK (sweeper->backbone); - LOG ("refined %zu backbone candidates into %zu", old_size, new_size); -#endif + LOGBACKBONE ("refined backbone candidates"); } static void -sweep_refine (kissat * solver, sweeper * sweeper) +sweep_refine (sweeper * sweeper) { +#ifdef LOGGING + kissat *solver = sweeper->solver; +#endif if (EMPTY_STACK (sweeper->backbone)) LOG ("no need to refine empty backbone candidates"); else - sweep_refine_backbone (solver, sweeper); + sweep_refine_backbone (sweeper); if (EMPTY_STACK (sweeper->partition)) LOG ("no need to refine empty partition candidates"); else - sweep_refine_partition (solver, sweeper); + sweep_refine_partition (sweeper); +} + +static void +flip_backbone_literals (struct sweeper *sweeper) +{ + struct kissat *solver = sweeper->solver; + const unsigned max_rounds = GET_OPTION (sweepfliprounds); + if (!max_rounds) + return; + assert (!EMPTY_STACK (sweeper->backbone)); + struct kitten *kitten = solver->kitten; + if (kitten_status (kitten) != 10) + return; + unsigned total_flipped = 0, flipped, round = 0; + do + { + round++; + flipped = 0; + unsigned *begin = BEGIN_STACK (sweeper->backbone), *q = begin; + const unsigned *const end = END_STACK (sweeper->backbone), *p = q; + while (p != end) + { + const unsigned lit = *p++; + if (kitten_flip_literal (kitten, lit)) + { + LOG ("flipping backbone candidate %s succeeded", LOGLIT (lit)); + total_flipped++; + flipped++; + } + else + { + LOG ("flipping backbone candidate %s failed", LOGLIT (lit)); + *q++ = lit; + } + } + SET_END_OF_STACK (sweeper->backbone, q); + LOG ("flipped %u backbone candidates in round %u", flipped, round); + + if (TERMINATED (sweep_terminated_1)) + break; + if (solver->statistics.kitten_ticks > sweeper->limit.ticks) + break; + } + while (flipped && round < max_rounds); + LOG ("flipped %u backbone candidates in total in %u rounds", + total_flipped, round); } static void -sweep_backbone_candidate (kissat * solver, sweeper * sweeper, unsigned lit) +sweep_backbone_candidate (sweeper * sweeper, unsigned lit) { + kissat *solver = sweeper->solver; LOG ("trying backbone candidate %s", LOGLIT (lit)); - const unsigned not_lit = NOT (lit); kitten *kitten = solver->kitten; + if (kitten_status (kitten) == 10 && kitten_flip_literal (kitten, lit)) + { + LOG ("flipping %s succeeded", LOGLIT (lit)); + LOGBACKBONE ("refined backbone candidates"); + return; + } + LOG ("flipping %s failed", LOGLIT (lit)); + const unsigned not_lit = NOT (lit); kitten_assume (kitten, not_lit); - int res = sweep_solve (solver, sweeper); + int res = sweep_solve (sweeper); if (res == 10) { LOG ("sweeping backbone candidate %s failed", LOGLIT (lit)); - sweep_refine (solver, sweeper); + sweep_refine (sweeper); } else if (res == 20) { LOG ("sweep unit %s", LOGLIT (lit)); - add_core (solver, sweeper); - delete_core (solver, sweeper); + save_add_clear_core (sweeper); } + else + LOG ("sweeping backbone candidate %s failed", LOGLIT (lit)); } static void add_binary (kissat * solver, unsigned lit, unsigned other) { - kissat_new_binary_clause (solver, true, lit, other); + kissat_new_binary_clause (solver, false, lit, other); } -static unsigned -sweep_equivalence_candidates (kissat * solver, sweeper * sweeper, - unsigned lit, unsigned other) +static void +enqueue_variable_last (sweeper * sweeper, unsigned idx) +{ + assert (sweeper->prev[idx] == INVALID_IDX); + assert (sweeper->next[idx] == INVALID_IDX); + + const unsigned last = sweeper->last; + if (last == INVALID_IDX) + { + assert (sweeper->first == INVALID_IDX); + sweeper->first = idx; + } + else + { + assert (sweeper->next[last] == INVALID_IDX); + sweeper->next[last] = idx; + } + sweeper->prev[idx] = last; + sweeper->last = idx; +} + +static void +enqueue_variable_first (sweeper * sweeper, unsigned idx) +{ + assert (sweeper->prev[idx] == INVALID_IDX); + assert (sweeper->next[idx] == INVALID_IDX); + + const unsigned first = sweeper->first; + if (first == INVALID_IDX) + { + assert (sweeper->last == INVALID_IDX); + sweeper->last = idx; + } + else + { + assert (sweeper->prev[first] == INVALID_IDX); + sweeper->prev[first] = idx; + } + sweeper->next[idx] = first; + sweeper->first = idx; +} + +static void +dequeue_variable (sweeper * sweeper, unsigned idx) +{ + const unsigned prev = sweeper->prev[idx]; + const unsigned next = sweeper->next[idx]; + if (prev == INVALID_IDX) + { + assert (sweeper->first == idx); + sweeper->first = next; + } + else + { + assert (sweeper->next[prev] == idx); + sweeper->next[prev] = next; + sweeper->prev[idx] = INVALID_IDX; + } + if (next == INVALID_IDX) + { + assert (sweeper->last == idx); + sweeper->last = prev; + } + else + { + assert (sweeper->prev[next] == idx); + sweeper->prev[next] = prev; + sweeper->next[idx] = INVALID_IDX; + } +} + +static bool +scheduled_variable (sweeper * sweeper, unsigned idx) +{ + if (sweeper->last == idx) + return true; + return sweeper->next[idx] != INVALID_IDX; +} + +static bool +schedule_variable (sweeper * sweeper, unsigned idx) +{ + kissat *solver = sweeper->solver; + assert (idx < VARS); + if (!ACTIVE (idx)) + return false; + if (sweeper->last == idx) + return true; + if (sweeper->next[idx] == INVALID_IDX) + { + LOG ("front scheduling sweeping candidate %s", LOGVAR (idx)); + enqueue_variable_last (sweeper, idx); + } + else + { + LOG ("moving sweeping candidate %s to front", LOGVAR (idx)); + dequeue_variable (sweeper, idx); + enqueue_variable_last (sweeper, idx); + } + return true; +} + +static void +schedule_literal (sweeper * sweeper, unsigned lit) +{ +#ifndef NDEBUG + kissat *solver = sweeper->solver; +#endif + assert (lit < LITS); + schedule_variable (sweeper, IDX (lit)); +} + +static void +substitute_connected_clauses (sweeper * sweeper, unsigned lit, unsigned repr) +{ + kissat *solver = sweeper->solver; + if (solver->inconsistent) + return; + value *const values = solver->values; + if (values[lit]) + return; + if (values[repr]) + return; + LOG ("substituting %s with %s in all irredundant clauses", + LOGLIT (lit), LOGLIT (repr)); + + assert (lit != repr); + assert (lit != NOT (repr)); + +#ifdef CHECKING_OR_PROVING + const bool checking_or_proving = kissat_checking_or_proving (solver); + assert (EMPTY_STACK (solver->added)); + assert (EMPTY_STACK (solver->removed)); +#endif + + unsigneds *const delayed = &solver->delayed; + assert (EMPTY_STACK (*delayed)); + + { + watches *lit_watches = &WATCHES (lit); + watch *const begin_watches = BEGIN_WATCHES (*lit_watches); + const watch *const end_watches = END_WATCHES (*lit_watches); + + watch *q = begin_watches; + const watch *p = q; + + while (p != end_watches) + { + const watch head = *q++ = *p++; + if (head.type.binary) + { + const unsigned other = head.binary.lit; + const value other_value = values[other]; + if (other == NOT (repr)) + continue; + if (other_value < 0) + break; + if (other_value > 0) + continue; + if (other == repr) + { + CHECK_AND_ADD_UNIT (lit); + ADD_UNIT_TO_PROOF (lit); + kissat_assign_unit (solver, lit, "substituted binary clause"); + INC (sweep_units); + break; + } + CHECK_AND_ADD_BINARY (repr, other); + ADD_BINARY_TO_PROOF (repr, other); + REMOVE_CHECKER_BINARY (lit, other); + DELETE_BINARY_FROM_PROOF (lit, other); + PUSH_STACK (*delayed, head.raw); + watch src = {.raw = head.raw }; + watch dst = {.raw = head.raw }; + src.binary.lit = lit; + dst.binary.lit = repr; + watches *other_watches = &WATCHES (other); + kissat_substitute_large_watch (solver, other_watches, src, dst); + q--; + } + else + { + const reference ref = head.large.ref; + assert (EMPTY_STACK (sweeper->clause)); + clause *c = kissat_dereference_clause (solver, ref); + if (c->garbage) + continue; + + bool satisfied = false; + bool repr_already_watched = false; + const unsigned not_repr = NOT (repr); +#ifndef NDEBUG + bool found = false; +#endif + for (all_literals_in_clause (other, c)) + { + if (other == lit) + { +#ifndef NDEBUG + assert (!found); + found = true; +#endif + PUSH_STACK (solver->clause, repr); + continue; + } + assert (other != NOT (lit)); + if (other == repr) + { + assert (!repr_already_watched); + repr_already_watched = true; + continue; + } + if (other == not_repr) + { + satisfied = true; + break; + } + const value tmp = values[other]; + if (tmp < 0) + continue; + if (tmp > 0) + { + satisfied = true; + break; + } + PUSH_STACK (solver->clause, other); + } + + if (satisfied) + { + CLEAR_STACK (solver->clause); + kissat_mark_clause_as_garbage (solver, c); + continue; + } + assert (found); + + const unsigned new_size = SIZE_STACK (solver->clause); + + if (new_size == 0) + { + LOGCLS (c, "substituted empty clause"); + assert (!solver->inconsistent); + solver->inconsistent = true; + CHECK_AND_ADD_EMPTY (); + ADD_EMPTY_TO_PROOF (); + break; + } + + if (new_size == 1) + { + LOGCLS (c, "reduces to unit"); + const unsigned unit = POP_STACK (solver->clause); + CHECK_AND_ADD_UNIT (unit); + ADD_UNIT_TO_PROOF (unit); + kissat_assign_unit (solver, unit, "substituted large clause"); + INC (sweep_units); + break; + } + + CHECK_AND_ADD_STACK (solver->clause); + ADD_STACK_TO_PROOF (solver->clause); + REMOVE_CHECKER_CLAUSE (c); + DELETE_CLAUSE_FROM_PROOF (c); + + if (!c->redundant) + kissat_mark_added_literals (solver, new_size, + BEGIN_STACK (solver->clause)); + + if (new_size == 2) + { + const unsigned second = POP_STACK (solver->clause); + const unsigned first = POP_STACK (solver->clause); + LOGCLS (c, "reduces to binary clause %s %s", + LOGLIT (first), LOGLIT (second)); + assert (first == repr || second == repr); + const unsigned other = first ^ second ^ repr; + const watch src = {.raw = head.raw }; + const bool redundant = c->redundant; + const bool hyper = c->hyper; + watch dst = kissat_binary_watch (repr, redundant, hyper); + watches *other_watches = &WATCHES (other); + kissat_substitute_large_watch (solver, other_watches, + src, dst); + dst.binary.lit = other; + PUSH_STACK (*delayed, dst.raw); + const size_t bytes = kissat_actual_bytes_of_clause (c); + ADD (arena_garbage, bytes); + c->garbage = true; + q--; + continue; + } + + assert (2 < new_size); + const unsigned old_size = c->size; + assert (new_size <= old_size); + + const unsigned *const begin = BEGIN_STACK (solver->clause); + const unsigned *const end = END_STACK (solver->clause); + + unsigned *q = c->lits; + + for (const unsigned *p = begin; p != end; p++) + { + const unsigned other = *p; + *q++ = other; + } + + if (new_size < old_size) + { + c->size = new_size; + c->searched = 2; + if (c->redundant && c->glue >= new_size) + kissat_promote_clause (solver, c, new_size - 1); + if (!c->shrunken) + { + c->shrunken = true; + c->lits[old_size - 1] = INVALID_LIT; + } + } + + LOGCLS (c, "substituted"); + + if (!repr_already_watched) + PUSH_STACK (*delayed, head.raw); + CLEAR_STACK (solver->clause); + q--; + } + } + while (p != end_watches) + *q++ = *p++; + SET_END_OF_WATCHES (*lit_watches, q); + } + { + const unsigned *const begin_delayed = BEGIN_STACK (*delayed); + const unsigned *const end_delayed = END_STACK (*delayed); + for (const unsigned *p = begin_delayed; p != end_delayed; p++) + { + const watch head = {.raw = *p }; + watches *repr_watches = &WATCHES (repr); + PUSH_WATCHES (*repr_watches, head); + } + + CLEAR_STACK (*delayed); + } + +#ifdef CHECKING_OR_PROVING + if (checking_or_proving) + { + CLEAR_STACK (solver->added); + CLEAR_STACK (solver->removed); + } +#endif +} + +static void +sweep_remove (sweeper * sweeper, unsigned lit) +{ + kissat *solver = sweeper->solver; + assert (sweeper->reprs[lit] != lit); + unsigneds *partition = &sweeper->partition; + unsigned *const begin_partition = BEGIN_STACK (*partition), *p; + const unsigned *const end_partition = END_STACK (*partition); + for (p = begin_partition; *p != lit; p++) + assert (p + 1 != end_partition); + unsigned *begin_class = p; + while (begin_class != begin_partition && begin_class[-1] != INVALID_LIT) + begin_class--; + const unsigned *end_class = p; + while (*end_class != INVALID_LIT) + end_class++; + const unsigned size = end_class - begin_class; + LOG ("removing non-representative %s from equivalence class of size %u", + LOGLIT (lit), size); + assert (size > 1); + unsigned *q = begin_class; + if (size == 2) + { + LOG ("completely squashing equivalence class of %s", LOGLIT (lit)); + for (const unsigned *r = end_class + 1; r != end_partition; r++) + *q++ = *r; + } + else + { + for (const unsigned *r = begin_class; r != end_partition; r++) + if (r != p) + *q++ = *r; + } + SET_END_OF_STACK (*partition, q); +#ifndef LOGGING + (void) solver; +#endif +} + +static void +flip_partition_literals (struct sweeper *sweeper) +{ + struct kissat *solver = sweeper->solver; + const unsigned max_rounds = GET_OPTION (sweepfliprounds); + if (!max_rounds) + return; + assert (!EMPTY_STACK (sweeper->partition)); + struct kitten *kitten = solver->kitten; + if (kitten_status (kitten) != 10) + return; + unsigned total_flipped = 0, flipped, round = 0;; + do + { + round++; + flipped = 0; + unsigned *begin = BEGIN_STACK (sweeper->partition), *dst = begin; + const unsigned *const end = END_STACK (sweeper->partition), *src = dst; + while (src != end) + { + const unsigned *end_src = src; + while (assert (end_src != end), *end_src != INVALID_LIT) + end_src++; + unsigned size = end_src - src; + assert (size > 1); + unsigned *q = dst; + for (const unsigned *p = src; p != end_src; p++) + { + const unsigned lit = *p; + if (kitten_flip_literal (kitten, lit)) + { + LOG ("flipping equivalence candidate %s succeeded", + LOGLIT (lit)); + total_flipped++; + flipped++; + if (--size < 2) + break; + } + else + { + LOG ("flipping equivalence candidate %s failed", + LOGLIT (lit)); + *q++ = lit; + } + } + if (size > 1) + { + *q++ = INVALID_LIT; + dst = q; + } + src = end_src + 1; + } + SET_END_OF_STACK (sweeper->partition, dst); + LOG ("flipped %u equivalence candidates in round %u", flipped, round); + + if (TERMINATED (sweep_terminated_2)) + break; + if (solver->statistics.kitten_ticks > sweeper->limit.ticks) + break; + } + while (flipped && round < max_rounds); + LOG ("flipped %u equivalence candidates in total in %u rounds", + total_flipped, round); +} + +static void +sweep_equivalence_candidates (sweeper * sweeper, unsigned lit, unsigned other) { + kissat *solver = sweeper->solver; LOG ("trying equivalence candidates %s = %s", LOGLIT (lit), LOGLIT (other)); const unsigned not_other = NOT (other); const unsigned not_lit = NOT (lit); kitten *kitten = solver->kitten; + const unsigned *const begin = BEGIN_STACK (sweeper->partition); + unsigned *const end = END_STACK (sweeper->partition); + assert (begin + 3 <= end); + assert (end[-3] == lit); + assert (end[-2] == other); + const unsigned third = (end - begin == 3) ? INVALID_LIT : end[-4]; + const int status = kitten_status (kitten); + if (status == 10 && kitten_flip_literal (kitten, lit)) + { + LOG ("flipping %s succeeded", LOGLIT (lit)); + if (third == INVALID_LIT) + { + LOG ("squashing equivalence class of %s", LOGLIT (lit)); + SET_END_OF_STACK (sweeper->partition, end - 3); + } + else + { + LOG ("removing %s from equivalence class of %s", + LOGLIT (lit), LOGLIT (other)); + end[-3] = other; + end[-2] = INVALID_LIT; + SET_END_OF_STACK (sweeper->partition, end - 1); + } + LOGPARTITION ("refined equivalence candidates"); + return; + } + else if (status == 10 && kitten_flip_literal (kitten, other)) + { + LOG ("flipping %s succeeded", LOGLIT (other)); + if (third == INVALID_LIT) + { + LOG ("squashing equivalence class of %s", LOGLIT (lit)); + SET_END_OF_STACK (sweeper->partition, end - 3); + } + else + { + LOG ("removing %s from equivalence class of %s", + LOGLIT (other), LOGLIT (lit)); + end[-2] = INVALID_LIT; + SET_END_OF_STACK (sweeper->partition, end - 1); + } + LOGPARTITION ("refined equivalence candidates"); + return; + } + LOG ("flipping %s and %s both failed", LOGLIT (lit), LOGLIT (other)); kitten_assume (kitten, not_lit); kitten_assume (kitten, other); - int res = sweep_solve (solver, sweeper); + int res = sweep_solve (sweeper); if (res == 10) { LOG ("first sweeping implication %s -> %s failed", - LOGLIT (lit), LOGLIT (other)); - sweep_refine (solver, sweeper); + LOGLIT (other), LOGLIT (lit)); + sweep_refine (sweeper); } else if (!res) { LOG ("first sweeping implication %s -> %s hit ticks limit", - LOGLIT (lit), LOGLIT (other)); + LOGLIT (other), LOGLIT (lit)); } if (res != 20) - return INVALID_LIT; + return; LOG ("first sweeping implication %s -> %s succeeded", - LOGLIT (lit), LOGLIT (other)); + LOGLIT (other), LOGLIT (lit)); + + save_core (sweeper, 0); + kitten_assume (kitten, lit); kitten_assume (kitten, not_other); - res = sweep_solve (solver, sweeper); + res = sweep_solve (sweeper); if (res == 10) { LOG ("second sweeping implication %s <- %s failed", - LOGLIT (lit), LOGLIT (other)); - sweep_refine (solver, sweeper); + LOGLIT (other), LOGLIT (lit)); + sweep_refine (sweeper); } else if (!res) { LOG ("second sweeping implication %s <- %s hit ticks limit", - LOGLIT (lit), LOGLIT (other)); + LOGLIT (other), LOGLIT (lit)); } if (res != 20) - return INVALID_LIT; - - LOG ("second sweeping implication %s <- %s succeeded too", - LOGLIT (lit), LOGLIT (other)); - - add_core (solver, sweeper); - LOG ("need to resolve first implication for proof again"); - kitten_assume (kitten, not_lit); - kitten_assume (kitten, other); - - res = sweep_solve (solver, sweeper); - - if (!res) { - LOG ("resolving first implication hits ticks limit"); - delete_core (solver, sweeper); - return INVALID_LIT; + CLEAR_STACK (sweeper->core[0]); + return; } - assert (res == 20); + LOG ("second sweeping implication %s <- %s succeeded too", + LOGLIT (other), LOGLIT (lit)); + + save_core (sweeper, 1); LOG ("sweep equivalence %s = %s", LOGLIT (lit), LOGLIT (other)); INC (sweep_equivalences); - add_binary (solver, not_lit, other); - delete_core (solver, sweeper); - add_core (solver, sweeper); + + add_core (sweeper, 0); add_binary (solver, lit, not_other); - delete_core (solver, sweeper); - assert (lit != other); - assert (lit != not_other); - LOG ("adding equivalences to sub-solver"); - kitten_binary (kitten, not_lit, other); - kitten_binary (kitten, lit, not_other); + clear_core (sweeper, 0); + + add_core (sweeper, 1); + add_binary (solver, not_lit, other); + clear_core (sweeper, 1); + + unsigned repr; if (lit < other) { - sweeper->reprs[other] = lit; + repr = sweeper->reprs[other] = lit; sweeper->reprs[not_other] = not_lit; - return lit; + substitute_connected_clauses (sweeper, other, lit); + substitute_connected_clauses (sweeper, not_other, not_lit); + sweep_remove (sweeper, other); } else { - sweeper->reprs[lit] = other; + repr = sweeper->reprs[lit] = other; sweeper->reprs[not_lit] = not_other; - return other; + substitute_connected_clauses (sweeper, lit, other); + substitute_connected_clauses (sweeper, not_lit, not_other); + sweep_remove (sweeper, lit); } + schedule_literal (sweeper, repr); } static void -sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) +sweep_variable (sweeper * sweeper, unsigned idx) { + kissat *solver = sweeper->solver; assert (!solver->inconsistent); if (!ACTIVE (idx)) return; @@ -678,24 +1378,24 @@ sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) assert (EMPTY_STACK (sweeper->backbone)); assert (EMPTY_STACK (sweeper->partition)); assert (!sweeper->encoded); + INC (sweep_variables); + LOG ("sweeping %s", LOGVAR (idx)); assert (!VALUE (start)); LOG ("starting sweeping[0]"); - add_literal_to_environment (solver, sweeper, 0, start); + add_literal_to_environment (sweeper, 0, start); LOG ("finished sweeping[0]"); LOG ("starting sweeping[1]"); + bool variable_limit_reached = false; size_t expand = 0, next = 1; - uint64_t depth_limit = solver->statistics.sweep_completed; - depth_limit += GET_OPTION (sweepdepth); - const unsigned max_depth = GET_OPTION (sweepmaxdepth); - if (depth_limit > max_depth) - depth_limit = max_depth; + unsigned depth = 1; + while (!variable_limit_reached) { - if (sweeper->encoded == (unsigned) GET_OPTION (sweepclauses)) + if (sweeper->encoded >= sweeper->limit.clauses) { LOG ("environment clause limit reached"); break; @@ -703,7 +1403,7 @@ sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) if (expand == next) { LOG ("finished sweeping[%u]", depth); - if (depth == (unsigned) GET_OPTION (sweepdepth)) + if (depth >= sweeper->limit.depth) { LOG ("environment depth limit reached"); break; @@ -718,6 +1418,7 @@ sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) LOG ("starting sweeping[%u]", depth); } const unsigned idx = PEEK_STACK (sweeper->vars, expand); + LOG ("traversing and adding clauses of %s", LOGVAR (idx)); for (unsigned sign = 0; sign < 2; sign++) { const unsigned lit = LIT (idx) + sign; @@ -727,15 +1428,14 @@ sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) if (watch.type.binary) { const unsigned other = watch.binary.lit; - sweep_binary (solver, sweeper, depth, lit, other); + sweep_binary (sweeper, depth, lit, other); } else { reference ref = watch.large.ref; - sweep_reference (solver, sweeper, depth, ref); + sweep_reference (sweeper, depth, ref); } - if (SIZE_STACK (sweeper->vars) >= - (unsigned) GET_OPTION (sweepvars)) + if (SIZE_STACK (sweeper->vars) >= sweeper->limit.vars) { LOG ("environment variable limit reached"); variable_limit_reached = true; @@ -747,219 +1447,278 @@ sweep_variable (kissat * solver, sweeper * sweeper, unsigned idx) } expand++; } -#if 0 - LOG ("sweeper environment has %zu variables", SIZE_STACK (sweeper->vars)); - LOG ("sweeper environment has %u clauses", sweeper->encoded); - LOG ("sweeper environment depth of %u generations", depth); -#elif !defined(QUIET) - { - int elit = kissat_export_literal (solver, LIT (idx)); - kissat_extremely_verbose (solver, - "variable %d environment of " - "%zu variables %u clauses depth %u", - elit, SIZE_STACK (sweeper->vars), - sweeper->encoded, depth); - } -#endif - int res = sweep_solve (solver, sweeper); + kissat_extremely_verbose (solver, + "variable %d environment of " + "%zu variables %u clauses depth %u", + kissat_export_literal (solver, LIT (idx)), + SIZE_STACK (sweeper->vars), + sweeper->encoded, depth); + int res = sweep_solve (sweeper); LOG ("sub-solver returns '%d'", res); if (res == 10) { - init_backbone_and_partition (solver, sweeper); + init_backbone_and_partition (sweeper); #ifndef QUIET uint64_t units = solver->statistics.sweep_units; uint64_t solved = solver->statistics.sweep_solved; #endif - bool done = false; while (!EMPTY_STACK (sweeper->backbone)) { if (solver->inconsistent || - TERMINATED (sweep_terminated_1) || - kitten_ticks_limit_hit (solver, sweeper, "backbone refinement")) - { - done = true; - break; - } + TERMINATED (sweep_terminated_3) || + kitten_ticks_limit_hit (sweeper, "backbone refinement")) + goto DONE; + flip_backbone_literals (sweeper); + if (TERMINATED (sweep_terminated_4) || + kitten_ticks_limit_hit (sweeper, "backbone refinement")) + goto DONE; + if (EMPTY_STACK (sweeper->backbone)) + break; const unsigned lit = POP_STACK (sweeper->backbone); if (!ACTIVE (IDX (lit))) continue; - sweep_backbone_candidate (solver, sweeper, lit); + sweep_backbone_candidate (sweeper, lit); } #ifndef QUIET units = solver->statistics.sweep_units - units; solved = solver->statistics.sweep_solved - solved; - // if (units) - { - int elit = kissat_export_literal (solver, LIT (idx)); - kissat_extremely_verbose (solver, - "%scomplete variable %d backbone with %" - PRIu64 " units in %" PRIu64 " solver calls", - done ? "in" : "", elit, units, solved); - } + kissat_extremely_verbose (solver, + "complete variable %d backbone with %" + PRIu64 " units in %" PRIu64 " solver calls", + kissat_export_literal (solver, LIT (idx)), + units, solved); #endif - if (!done) - { - assert (EMPTY_STACK (sweeper->backbone)); + assert (EMPTY_STACK (sweeper->backbone)); #ifndef QUIET - uint64_t equivalences = solver->statistics.sweep_equivalences; + uint64_t equivalences = solver->statistics.sweep_equivalences; #endif - while (!EMPTY_STACK (sweeper->partition)) + while (!EMPTY_STACK (sweeper->partition)) + { + if (solver->inconsistent || + TERMINATED (sweep_terminated_5) || + kitten_ticks_limit_hit (sweeper, "partition refinement")) + goto DONE; + flip_partition_literals (sweeper); + if (TERMINATED (sweep_terminated_6) || + kitten_ticks_limit_hit (sweeper, "backbone refinement")) + goto DONE; + if (EMPTY_STACK (sweeper->partition)) + break; + if (SIZE_STACK (sweeper->partition) > 2) { - if (solver->inconsistent || - TERMINATED (sweep_terminated_2) || - kitten_ticks_limit_hit (solver, sweeper, - "partition refinement")) - { - done = true; - break; - } - if (SIZE_STACK (sweeper->partition) > 2) - { - const unsigned *end = END_STACK (sweeper->partition); - assert (end[-1] == INVALID_LIT); - unsigned lit = end[-2]; - unsigned other = end[-3]; - unsigned repr = - sweep_equivalence_candidates (solver, sweeper, lit, - other); - if (repr != INVALID_LIT) - { - unsigned tmp = POP_STACK (sweeper->partition); - assert (tmp == INVALID_LIT); - tmp = POP_STACK (sweeper->partition); - assert (tmp == lit); - tmp = POP_STACK (sweeper->partition); - assert (tmp == other); -#ifdef NDEBUG - (void) tmp; -#endif - if (!EMPTY_STACK (sweeper->partition) && - TOP_STACK (sweeper->partition) != INVALID_LIT) - { - LOG ("merged %s and %s into %s", - LOGLIT (lit), LOGLIT (other), LOGLIT (repr)); - PUSH_STACK (sweeper->partition, repr); - PUSH_STACK (sweeper->partition, INVALID_LIT); - } - else - LOG ("squashed binary candidate class with %s %s", - LOGLIT (lit), LOGLIT (other)); - } - } - else - CLEAR_STACK (sweeper->partition); + const unsigned *end = END_STACK (sweeper->partition); + assert (end[-1] == INVALID_LIT); + unsigned lit = end[-3]; + unsigned other = end[-2]; + sweep_equivalence_candidates (sweeper, lit, other); } + else + CLEAR_STACK (sweeper->partition); + } #ifndef QUIET - equivalences = solver->statistics.sweep_equivalences - equivalences; - solved = solver->statistics.sweep_solved - solved; - // if (equivalences) - { - int elit = kissat_export_literal (solver, LIT (idx)); - kissat_extremely_verbose (solver, - "%scomplete variable %d partition with %" - PRIu64 " equivalences in %" PRIu64 - " solver calls", done ? "in" : "", elit, - equivalences, solved); - } + equivalences = solver->statistics.sweep_equivalences - equivalences; + solved = solver->statistics.sweep_solved - solved; + if (equivalences) + kissat_extremely_verbose (solver, + "complete variable %d partition with %" + PRIu64 " equivalences in %" PRIu64 + " solver calls", + kissat_export_literal (solver, LIT (idx)), + equivalences, solved); #endif - } } else if (res == 20) - sweep_empty_clause (solver, sweeper); + sweep_empty_clause (sweeper); + +DONE: + clear_sweeper (sweeper); if (!solver->inconsistent && !kissat_propagated (solver)) - kissat_dense_propagate (solver); + (void) kissat_dense_propagate (solver); +} + +typedef struct sweep_candidate sweep_candidate; + +struct sweep_candidate +{ + unsigned rank; + unsigned idx; +}; + +// *INDENT-OFF* + +typedef STACK(sweep_candidate) sweep_candidates; + +// *INDENT-ON* - clear_sweeper (solver, sweeper); +#define RANK_SWEEP_CANDIDATE(CAND) (CAND).rank + +static size_t +occurrences_variables (kissat * solver, unsigned idx) +{ + const unsigned lit = LIT (idx); + const unsigned not_lit = NOT (lit); + const size_t pos = SIZE_WATCHES (WATCHES (lit)); + const size_t neg = SIZE_WATCHES (WATCHES (not_lit)); + return pos + neg; } static unsigned -schedule_sweeping (kissat * solver, sweeper * sweeper) +schedule_fresh (sweeper * sweeper) { - assert (EMPTY_STACK (sweeper->schedule)); - const size_t max_occurrences = GET_OPTION (sweepclauses); -#ifndef QUIET + const unsigned max_occurrences = sweeper->limit.clauses; + kissat *solver = sweeper->solver; + flags *flags = solver->flags; + sweep_candidates fresh; + INIT_STACK (fresh); + const unsigned variables = VARS; + for (unsigned idx = 0; idx != variables; idx++) + { + struct flags *f = flags + idx; + if (!f->active) + continue; + if (f->sweep) + continue; + if (scheduled_variable (sweeper, idx)) + continue; + const size_t occ = occurrences_variables (solver, idx); + if (occ > max_occurrences) + continue; + sweep_candidate cand; + cand.rank = occ; + cand.idx = idx; + PUSH_STACK (fresh, cand); + } + unsigned size = SIZE_STACK (fresh); + RADIX_STACK (sweep_candidate, unsigned, fresh, RANK_SWEEP_CANDIDATE); + for (all_stack (sweep_candidate, cand, fresh)) + enqueue_variable_first (sweeper, cand.idx); + RELEASE_STACK (fresh); + return size; +} + +static unsigned +reschedule_previously_remaining (sweeper * sweeper) +{ + kissat *solver = sweeper->solver; + flags *flags = solver->flags; + const unsigned max_occurrences = sweeper->limit.clauses; unsigned rescheduled = 0; -#endif - for (unsigned reschedule = 0; reschedule < 2; reschedule++) + for (all_stack (unsigned, idx, solver->sweep)) { - for (unsigned idx = VARS; idx--;) - { - if (!ACTIVE (idx)) - continue; - const unsigned sweep = FLAGS (idx)->sweep; - if (reschedule != sweep) - continue; - const unsigned lit = LIT (idx); - const unsigned not_lit = NOT (lit); - const size_t pos = SIZE_WATCHES (WATCHES (lit)); - const size_t neg = SIZE_WATCHES (WATCHES (not_lit)); - if (pos + neg > max_occurrences) - continue; - LOG ("scheduling %s with %zu + %zu occurrences", - LOGVAR (idx), pos, neg); - PUSH_STACK (sweeper->schedule, idx); -#ifndef QUIET - if (reschedule) - rescheduled++; -#endif - } + struct flags *f = flags + idx; + if (!f->active) + continue; + const size_t occ = occurrences_variables (solver, idx); + if (occ > max_occurrences) + continue; + assert (!scheduled_variable (sweeper, idx)); + enqueue_variable_last (sweeper, idx); + rescheduled++; } - const unsigned scheduled = SIZE_STACK (sweeper->schedule); + CLEAR_STACK (solver->sweep); + return rescheduled; +} + +static unsigned +incomplete_variables (sweeper * sweeper) +{ + kissat *solver = sweeper->solver; + flags *flags = solver->flags; + unsigned res = 0; + for (unsigned idx = sweeper->first; idx != INVALID_IDX; + idx = sweeper->next[idx]) + if (flags[idx].sweep) + res++; + return res; +} + +static void +mark_all_scheduled_variables_as_incomplete (sweeper * sweeper) +{ + kissat *solver = sweeper->solver; + kissat_extremely_verbose (solver, + "marking scheduled variables as incomplete"); + flags *flags = solver->flags; + for (unsigned idx = sweeper->first; idx != INVALID_IDX; + idx = sweeper->next[idx]) + flags[idx].sweep = true; +} + +static unsigned +schedule_sweeping (sweeper * sweeper) +{ + assert (sweeper->first == INVALID_IDX); + assert (sweeper->last == INVALID_IDX); + unsigned rescheduled = reschedule_previously_remaining (sweeper); + unsigned fresh = schedule_fresh (sweeper); + unsigned scheduled = fresh + rescheduled; + unsigned incomplete = incomplete_variables (sweeper); #ifndef QUIET + kissat *solver = sweeper->solver; kissat_phase (solver, "sweep", GET (sweep), - "scheduled %u variables %.0f%% (%u rescheduled %.0f%%)", - scheduled, kissat_percent (scheduled, solver->active), - rescheduled, kissat_percent (rescheduled, scheduled)); + "scheduled %u variables " + "(%u rescheduled %.0f%%, %u incomplete %.0f%%)", + scheduled, rescheduled, + kissat_percent (rescheduled, scheduled), + incomplete, kissat_percent (incomplete, scheduled)); #endif + if (!incomplete) + mark_all_scheduled_variables_as_incomplete (sweeper); return scheduled; } static void -unschedule_sweeping (kissat * solver, sweeper * sweeper, unsigned scheduled) +unschedule_sweeping (sweeper * sweeper, unsigned swept, unsigned scheduled) { - if (EMPTY_STACK (sweeper->schedule)) - { - INC (sweep_completed); - kissat_phase (solver, "sweep", GET (sweep), - "all scheduled variables swept"); - return; - } - unsigned rescheduled = 0; - unsigned notrescheduled = 0; - for (all_stack (unsigned, idx, sweeper->schedule)) + kissat *solver = sweeper->solver; +#ifdef QUIET + (void) scheduled, (void) swept; +#endif + assert (EMPTY_STACK (solver->sweep)); + flags *flags = solver->flags; + for (unsigned idx = sweeper->first; + idx != INVALID_IDX; idx = sweeper->next[idx]) + if (flags[idx].active) + PUSH_STACK (solver->sweep, idx); + unsigned remain = SIZE_STACK (solver->sweep); + if (remain) { - if (!ACTIVE (idx)) - continue; - struct flags *f = FLAGS (idx); - const bool sweep = f->sweep; - if (sweep) - rescheduled++; + const unsigned incomplete = incomplete_variables (sweeper); + if (incomplete) + kissat_extremely_verbose (solver, + "need to sweep %u more variables " + "for completion", incomplete); else - notrescheduled++; - } - if (!rescheduled && !notrescheduled) - { - kissat_phase (solver, "sweep", GET (sweep), - "actually all scheduled variables swept"); - return; + { + kissat_extremely_verbose (solver, + "no variables needed to complete sweep"); + INC (sweep_completed); + } } - if (!rescheduled) + else { + kissat_extremely_verbose (solver, "all variables swept"); INC (sweep_completed); - for (all_stack (unsigned, idx, sweeper->schedule)) - if (ACTIVE (idx)) - FLAGS (idx)->sweep = true; } -#ifndef QUIET - const unsigned total = rescheduled + notrescheduled; kissat_phase (solver, "sweep", GET (sweep), - "%u variables remain %.0f%% (%u rescheduled %.0f%%)", - total, kissat_percent (total, scheduled), - rescheduled, kissat_percent (rescheduled, total)); -#else - (void) scheduled; -#endif + "swept %u variables (%u remain %.0f%%)", + swept, remain, kissat_percent (remain, scheduled)); +} + +static bool +empty_schedule (sweeper * sweeper) +{ + return sweeper->last == INVALID_IDX; +} + +static unsigned +pop_schedule (sweeper * sweeper) +{ + unsigned res = sweeper->last; + if (res != INVALID_IDX) + dequeue_variable (sweeper, res); + return res; } void @@ -978,37 +1737,40 @@ kissat_sweep (kissat * solver) uint64_t units = statistics->sweep_units; sweeper sweeper; init_sweeper (solver, &sweeper); - const unsigned scheduled = schedule_sweeping (solver, &sweeper); -#ifndef QUIET + const unsigned scheduled = schedule_sweeping (&sweeper); unsigned swept = 0; -#endif - while (!EMPTY_STACK (sweeper.schedule)) + while (!empty_schedule (&sweeper)) { if (solver->inconsistent) break; - if (TERMINATED (sweep_terminated_3)) + if (TERMINATED (sweep_terminated_7)) break; - if (solver->statistics.kitten_ticks > sweeper.limit) + if (solver->statistics.kitten_ticks > sweeper.limit.ticks) break; - const unsigned idx = POP_STACK (sweeper.schedule); + const unsigned idx = pop_schedule (&sweeper); + assert (idx != INVALID_IDX); FLAGS (idx)->sweep = false; - sweep_variable (solver, &sweeper, idx); -#ifndef QUIET - int elit = kissat_export_literal (solver, LIT (idx)); + sweep_variable (&sweeper, idx); kissat_extremely_verbose (solver, - "swept[%u] external variable %d", - ++swept, elit); -#endif + "swept[%u] external variable %d", swept, + kissat_export_literal (solver, LIT (idx))); + swept++; } - unschedule_sweeping (solver, &sweeper, scheduled); - unsigned inactive = release_sweeper (solver, &sweeper); equivalences = statistics->sweep_equivalences - equivalences; units = solver->statistics.sweep_units - units; kissat_phase (solver, "sweep", GET (sweep), - "found %" PRIu64 " equivalences and %" PRIu64 - " units sweeping %u variables %.0f%%", - equivalences, units, swept, - kissat_percent (swept, scheduled)); + "found %" PRIu64 " equivalences and %" PRIu64 " units", + equivalences, units); + + unschedule_sweeping (&sweeper, swept, scheduled); + unsigned inactive = release_sweeper (&sweeper); + + if (!solver->inconsistent) + { + solver->propagate = solver->trail.begin; + kissat_probing_propagate (solver, 0, true); + } + #ifndef QUIET uint64_t eliminated = equivalences + units; assert (solver->active >= inactive); diff --git a/src/terminate.h b/src/terminate.h index c12acc92..1bb36a0d 100644 --- a/src/terminate.h +++ b/src/terminate.h @@ -56,23 +56,29 @@ kissat_terminated (kissat * solver, int bit, const char *name, #define kitten_terminated_1 13 #define rephase_terminated_1 14 #define rephase_terminated_2 15 -#define search_terminated_1 16 -#define substitute_terminated_1 17 -#define sweep_terminated_1 18 -#define sweep_terminated_2 19 -#define sweep_terminated_3 20 -#define ternary_terminated_1 21 -#define ternary_terminated_2 22 -#define ternary_terminated_3 23 -#define transitive_terminated_1 24 -#define transitive_terminated_2 25 -#define transitive_terminated_3 26 -#define vivify_terminated_1 27 -#define vivify_terminated_2 28 -#define vivify_terminated_3 29 -#define vivify_terminated_4 30 -#define walk_terminated_1 31 -#define walk_terminated_2 32 -#define xors_terminated_1 33 +#define rephase_terminated_3 16 +#define search_terminated_1 17 +#define substitute_terminated_1 18 +#define sweep_terminated_1 19 +#define sweep_terminated_2 20 +#define sweep_terminated_3 21 +#define sweep_terminated_4 22 +#define sweep_terminated_5 23 +#define sweep_terminated_6 24 +#define sweep_terminated_7 25 +#define ternary_terminated_1 26 +#define ternary_terminated_2 27 +#define ternary_terminated_3 28 +#define transitive_terminated_1 29 +#define transitive_terminated_2 30 +#define transitive_terminated_3 31 +#define vivify_terminated_1 32 +#define vivify_terminated_2 33 +#define vivify_terminated_3 34 +#define vivify_terminated_4 35 +#define walk_terminated_1 36 +#define walk_terminated_2 37 +#define warmup_terminated_1 38 +#define xors_terminated_1 39 #endif diff --git a/src/ternary.c b/src/ternary.c index c4cb9894..104fe0e1 100644 --- a/src/ternary.c +++ b/src/ternary.c @@ -445,7 +445,7 @@ really_ternary (kissat * solver) if (!GET_OPTION (really)) return true; - const uint64_t limit = 2 * CLAUSES + kissat_nlogn (1 + CLAUSES); + const uint64_t limit = 2 * CLAUSES + NLOGN (1 + CLAUSES); const uint64_t search_ticks = solver->statistics.search_ticks; if (limit >= search_ticks) @@ -589,7 +589,7 @@ kissat_ternary (kissat * solver) if (scheduled) { SET_EFFORT_LIMIT (steps_limit, ternary, hyper_ternary_steps, - 2 * CLAUSES + kissat_nlogn (1 + scheduled)); + 2 * CLAUSES + NLOGN (1 + scheduled)); resolved = ternary_round (solver, resolved_limit, steps_limit, scheduled); diff --git a/src/trail.c b/src/trail.c index 5d7b6ddf..7ca1feec 100644 --- a/src/trail.c +++ b/src/trail.c @@ -49,28 +49,6 @@ kissat_mark_reason_clauses (kissat * solver, reference start) LOG ("marked %u reason clauses", reasons); } -// TODO check whether this can be merged with -// 'kissat_backtrack_propagate_and_flush_trail'. - -void -kissat_restart_and_flush_trail (kissat * solver) -{ - if (solver->level) - { - LOG ("forced restart"); - kissat_backtrack_in_consistent_state (solver, 0); - } - -#ifndef NDEBUG - clause *conflict = -#endif - kissat_search_propagate (solver); - assert (!conflict); - - assert (kissat_propagated (solver)); - assert (kissat_trail_flushed (solver)); -} - bool kissat_flush_and_mark_reason_clauses (kissat * solver, reference start) { @@ -81,7 +59,7 @@ kissat_flush_and_mark_reason_clauses (kissat * solver, reference start) if (solver->unflushed) { LOG ("need to flush %u units from trail", solver->unflushed); - kissat_restart_and_flush_trail (solver); + kissat_backtrack_propagate_and_flush_trail (solver); } else { diff --git a/src/trail.h b/src/trail.h index 897dabf7..6c816ddf 100644 --- a/src/trail.h +++ b/src/trail.h @@ -8,7 +8,6 @@ struct kissat; void kissat_flush_trail (struct kissat *); -void kissat_restart_and_flush_trail (struct kissat *); bool kissat_flush_and_mark_reason_clauses (struct kissat *, reference start); void kissat_unmark_reason_clauses (struct kissat *, reference start); void kissat_mark_reason_clauses (struct kissat *, reference start); diff --git a/src/transitive.c b/src/transitive.c index 7917e222..a7ac24cb 100644 --- a/src/transitive.c +++ b/src/transitive.c @@ -301,7 +301,7 @@ static void sort_stable_transitive (kissat * solver, unsigneds * probes) { const flags *const flags = solver->flags; - const heap *const scores = &solver->scores; + const heap *const scores = SCORES; SORT_STACK (unsigned, *probes, LESS_STABLE_PROBE); } diff --git a/src/utilities.h b/src/utilities.h index 106f6390..c12844db 100644 --- a/src/utilities.h +++ b/src/utilities.h @@ -121,7 +121,7 @@ kissat_log2_ceiling_of_word (word x) if (!x) return 0; unsigned tmp = kissat_log2_floor_of_word (x); - return tmp + ! !(x ^ (((word) 1) << tmp)); + return tmp + !!(x ^ (((word) 1) << tmp)); } static inline unsigned @@ -149,7 +149,7 @@ kissat_log2_ceiling_of_uint64 (uint64_t x) if (!x) return 0; unsigned tmp = kissat_log2_floor_of_uint64 (x); - return tmp + ! !(x ^ (((uint64_t) 1) << tmp)); + return tmp + !!(x ^ (((uint64_t) 1) << tmp)); } #define SWAP(TYPE,A,B) \ diff --git a/src/vector.c b/src/vector.c index 86efc81d..a10682e3 100644 --- a/src/vector.c +++ b/src/vector.c @@ -24,15 +24,17 @@ fix_vector_pointers_after_moving_stack (kissat * solver, ptrdiff_t moved) struct vector *end_watches = begin_watches + LITS; for (struct vector * p = begin_watches; p != end_watches; p++) { + #define FIX_POINTER(PTR) \ do { \ -char * old_char_ptr_value = (char*) (PTR); \ -if (!old_char_ptr_value) \ -break; \ -char * new_char_ptr_value = old_char_ptr_value + moved; \ -unsigned * new_unsigned_ptr_value = (unsigned *) new_char_ptr_value; \ -(PTR) = new_unsigned_ptr_value; \ + char * old_char_ptr_value = (char*) (PTR); \ + if (!old_char_ptr_value) \ + break; \ + char * new_char_ptr_value = old_char_ptr_value + moved; \ + unsigned * new_unsigned_ptr_value = (unsigned *) new_char_ptr_value; \ + (PTR) = new_unsigned_ptr_value; \ } while (0) + FIX_POINTER (p->begin); FIX_POINTER (p->end); } diff --git a/src/vivify.c b/src/vivify.c index 20d745c3..001c5a49 100644 --- a/src/vivify.c +++ b/src/vivify.c @@ -18,13 +18,8 @@ static inline bool more_occurrences (unsigned *counts, unsigned a, unsigned b) { - const unsigned s = counts[a]; - const unsigned t = counts[b]; - if (s > t) - return true; - if (s < t) - return false; - return a < b; + const unsigned s = counts[a], t = counts[b]; + return ((t - s) | ((b - a) & ~(s - t))) >> 31; } #define MORE_OCCURRENCES(A,B) \ @@ -55,10 +50,7 @@ vivify_sort_clause_by_counts (kissat * solver, clause * c, unsigned *counts) static void count_literal (unsigned lit, unsigned *counts) { - const unsigned old_count = counts[lit]; - const unsigned new_count = - (old_count < UINT_MAX) ? old_count + 1 : UINT_MAX; - counts[lit] = new_count; + counts[lit] += counts[lit] < (unsigned) INT_MAX; } static void @@ -174,6 +166,8 @@ schedule_vivification_candidates (kissat * solver, { if (c->garbage) continue; + if (prioritize) + count_clause (c, counts); if (redundant) { if (!c->redundant) @@ -193,7 +187,6 @@ schedule_vivification_candidates (kissat * solver, continue; if (prioritize) prioritized++; - count_clause (c, counts); const reference ref = (ward *) c - arena; PUSH_STACK (*schedule, ref); } @@ -221,12 +214,6 @@ schedule_vivification_candidates (kissat * solver, } } -static unsigned * -new_vivification_candidates_counts (kissat * solver) -{ - return kissat_calloc (solver, LITS, sizeof (unsigned)); -} - static inline bool worse_candidate (kissat * solver, unsigned *counts, reference r, reference s) { @@ -248,22 +235,24 @@ worse_candidate (kissat * solver, unsigned *counts, reference r, reference s) { const unsigned a = *p++; const unsigned b = *q++; - if (a == b) - continue; const unsigned u = counts[a]; const unsigned v = counts[b]; if (u < v) return true; if (u > v) return false; - return a < b; + if (a < b) + return true; + if (a > b) + return false; } if (p != e && q == f) - return true; - if (p == e && q != f) return false; + if (p == e && q != f) + return true; + return r < s; } @@ -335,7 +324,7 @@ vivify_binary_or_large_conflict (kissat * solver, clause * conflict) static bool vivify_analyze (kissat * solver, clause * c, - clause * conflict, bool * irredundant_ptr) + clause * conflict, bool *irredundant_ptr) { assert (conflict); assert (!EMPTY_STACK (solver->analyzed)); @@ -691,8 +680,17 @@ vivify_learn (kissat * solver, clause * c, return res; } +enum round +{ + REDUNDANT_TIER1_ROUND = 1, + REDUNDANT_TIER2_ROUND = 2, + IRREDUNDANT_ROUND = 3 +}; + +typedef enum round round; + static bool -vivify_clause (kissat * solver, clause * c, +vivify_clause (kissat * solver, round round, clause * c, unsigneds * sorted, unsigned *counts) { assert (!c->garbage); @@ -700,7 +698,7 @@ vivify_clause (kissat * solver, clause * c, assert (solver->watching); assert (!solver->inconsistent); - LOGCLS (c, "trying to vivify candidate"); + LOGCOUNTEDCLS (c, counts, "vivifying unsorted candidate"); CLEAR_STACK (*sorted); @@ -790,6 +788,8 @@ vivify_clause (kissat * solver, clause * c, assert (EMPTY_STACK (solver->clause)); vivify_sort_stack_by_counts (solver, sorted, counts); + LOGCOUNTEDLITS (SIZE_STACK (*sorted), sorted->begin, counts, + "vivifying sorted candidate"); #if defined(LOGGING) && !defined(NOPTIONS) if (solver->options.log) @@ -798,7 +798,7 @@ vivify_clause (kissat * solver, clause * c, COLOR (MAGENTA); printf ("c LOG %u vivify sorted size %zu candidate clause", solver->level, SIZE_STACK (*sorted)); - heap *scores = &solver->scores; + heap *scores = SCORES; links *links = solver->links; for (all_stack (unsigned, lit, *sorted)) { @@ -880,14 +880,15 @@ vivify_clause (kissat * solver, clause * c, assert (value > 0); assert (LEVEL (lit)); LOG ("literal %s already satisfied", LOGLIT (lit)); - if (!c->redundant || GET_OPTION (vivifyimply) == 1) + if (!c->redundant || GET_OPTION (vivifyimply) == 1 || + (GET_OPTION (vivifyimply) == 2 && round == REDUNDANT_TIER1_ROUND)) { implied = lit; conflict = vivify_unit_conflict (solver, lit); assert (!EMPTY_STACK (solver->analyzed)); assert (conflict); } - else if (GET_OPTION (vivifyimply) == 2) + else if (GET_OPTION (vivifyimply) == 3) { LOGCLS (c, "vivify implied"); kissat_mark_clause_as_garbage (solver, c); @@ -965,15 +966,6 @@ vivify_clause (kissat * solver, clause * c, return true; } -enum round -{ - REDUNDANT_TIER1_ROUND = 1, - REDUNDANT_TIER2_ROUND = 2, - IRREDUNDANT_ROUND = 3 -}; - -typedef enum round round; - static size_t vivify_round (kissat * solver, round round, bool sort, uint64_t delta, double effort) @@ -1006,23 +998,13 @@ vivify_round (kissat * solver, round round, } #endif - const uint64_t scaled = effort * delta; - kissat_extremely_verbose (solver, "%s effort delta %" PRIu64 - " = %g * %" PRIu64 " 'probing_ticks'", - mode, scaled, effort, delta); - uint64_t start = solver->statistics.probing_ticks; - const uint64_t ticks_limit = start + scaled; - kissat_very_verbose (solver, - "%s effort limit %" PRIu64 - " = %" PRIu64 " + %" PRIu64 " 'probing_ticks'", - mode, ticks_limit, start, scaled); references schedule; INIT_STACK (schedule); - unsigned *counts = 0; kissat_flush_large_watches (solver); - counts = new_vivification_candidates_counts (solver); + unsigned *counts = kissat_calloc (solver, LITS, sizeof (unsigned)); + { bool redundant, tier2; @@ -1048,6 +1030,17 @@ vivify_round (kissat * solver, round round, kissat_watch_large_clauses (solver); const size_t scheduled = SIZE_STACK (schedule); + const size_t adjusted = NLOGN (scheduled + 1); + const uint64_t scaled = effort * delta; + kissat_extremely_verbose (solver, "%s effort delta %" PRIu64 + " = %g * %" PRIu64 " 'probing_ticks'", + mode, scaled, effort, delta); + uint64_t start = solver->statistics.probing_ticks; + uint64_t ticks_limit = start + scaled + adjusted; + kissat_very_verbose (solver, + "%s effort limit %" PRIu64 + " = %" PRIu64 " + %" PRIu64 " + %zu 'probing_ticks'", + mode, ticks_limit, start, scaled, adjusted); #ifndef QUIET const size_t total = (round == IRREDUNDANT_ROUND) ? IRREDUNDANT_CLAUSES : REDUNDANT_CLAUSES; @@ -1075,7 +1068,7 @@ vivify_round (kissat * solver, round round, if (c->garbage) continue; tried++; - if (vivify_clause (solver, c, &sorted, counts)) + if (vivify_clause (solver, round, c, &sorted, counts)) vivified++; c->vivify = false; if (solver->inconsistent) @@ -1217,7 +1210,7 @@ vivify_irredundant (kissat * solver, uint64_t redundant_scheduled, static uint64_t vivify_adjustment (kissat * solver) { - return kissat_nlogn (1 + CLAUSES); + return 1 + CLAUSES; } static bool diff --git a/src/walk.c b/src/walk.c index 8e7f055b..c4bb8617 100644 --- a/src/walk.c +++ b/src/walk.c @@ -8,6 +8,7 @@ #include "rephase.h" #include "terminate.h" #include "walk.h" +#include "warmup.h" #include @@ -228,10 +229,10 @@ import_decision_phases (walker * walker) kissat *solver = walker->solver; INC (walk_decisions); value *const saved = solver->phases.saved; - const value *const target = solver->phases.target; + const value *const target = + (solver->stable && !GET_OPTION (warmup)) ? solver->phases.target : 0; const value initial_phase = INITIAL_PHASE; const flags *const flags = solver->flags; - const bool stable = solver->stable; value *values = solver->values; #ifndef QUIET unsigned imported = 0; @@ -242,7 +243,7 @@ import_decision_phases (walker * walker) if (!flags[idx].active) continue; value value = 0; - if (stable) + if (target) value = target[idx]; if (!value) value = saved[idx]; @@ -1179,6 +1180,9 @@ walk (kissat * solver, bool first_time, bool use_previous_phase) return; } + if (!use_previous_phase && GET_OPTION (warmup)) + kissat_warmup (solver); + STOP_SEARCH_AND_START_SIMPLIFIER (walking); walking_phase (solver, first_time, use_previous_phase); STOP_SIMPLIFIER_AND_RESUME_SEARCH (walking); @@ -1205,7 +1209,7 @@ kissat_walk (kissat * solver) const uint64_t walks = GET (walks); const bool first_time = !walks; const int reuse = GET_OPTION (walkreuse); - const bool decisions_used = ! !(solver->walked & mask); + const bool decisions_used = !!(solver->walked & mask); bool use_previous_phases; diff --git a/src/warmup.c b/src/warmup.c new file mode 100644 index 00000000..903e183c --- /dev/null +++ b/src/warmup.c @@ -0,0 +1,48 @@ +#include "backtrack.h" +#include "decide.h" +#include "internal.h" +#include "print.h" +#include "propbeyond.h" +#include "terminate.h" +#include "warmup.h" + +void +kissat_warmup (kissat * solver) +{ + assert (!solver->level); + assert (solver->watching); + assert (!solver->inconsistent); + assert (GET_OPTION (warmup)); + START (warmup); + INC (warmups); +#ifndef QUIET + const statistics *stats = &solver->statistics; + uint64_t propagations = stats->propagations; + uint64_t decisions = stats->decisions; +#endif + while (solver->unassigned) + { + if (TERMINATED (warmup_terminated_1)) + break; + kissat_decide (solver); + kissat_propagate_beyond_conflicts (solver); + } + assert (!solver->inconsistent); +#ifndef QUIET + decisions = stats->decisions - decisions; + propagations = stats->propagations - propagations; + + kissat_very_verbose (solver, + "warming-up needed %" PRIu64 " decisions and %" + PRIu64 " propagations", decisions, propagations); + + if (solver->unassigned) + kissat_verbose (solver, "reached decision level %u " + "during warming-up saved phases", solver->level); + else + kissat_verbose (solver, "all variables assigned at decision level %u " + "during warming-up saved phases", solver->level); +#endif + kissat_backtrack_without_updating_phases (solver, 0); + STOP (warmup); +} diff --git a/src/warmup.h b/src/warmup.h new file mode 100644 index 00000000..e0fd4712 --- /dev/null +++ b/src/warmup.h @@ -0,0 +1,8 @@ +#ifndef _warmup_h_INCLUDED +#define _warmup_h_INCLUDED + +struct kissat; + +void kissat_warmup (struct kissat *); + +#endif diff --git a/src/watch.c b/src/watch.c index c304c58a..2ac8eccf 100644 --- a/src/watch.c +++ b/src/watch.c @@ -43,6 +43,30 @@ kissat_remove_blocking_watch (kissat * solver, kissat_check_vectors (solver); } +void +kissat_substitute_large_watch (kissat * solver, + watches * watches, watch src, watch dst) +{ + assert (!solver->watching); + watch *const begin = BEGIN_WATCHES (*watches); + const watch *const end = END_WATCHES (*watches); +#ifndef NDEBUG + bool found = false; +#endif + for (watch * p = begin; p != end; p++) + { + const watch head = *p; + if (head.raw != src.raw) + continue; +#ifndef NDEBUG + found = true; +#endif + *p = dst; + break; + } + assert (found); +} + void kissat_flush_large_watches (kissat * solver) { diff --git a/src/watch.h b/src/watch.h index 473bc582..9524b495 100644 --- a/src/watch.h +++ b/src/watch.h @@ -206,6 +206,9 @@ do { \ void kissat_remove_blocking_watch (struct kissat *, watches *, reference); +void kissat_substitute_large_watch (struct kissat *, watches *, + watch src, watch dst); + void kissat_flush_large_watches (struct kissat *); void kissat_watch_large_clauses (struct kissat *); diff --git a/src/xors.c b/src/xors.c index 188b57c1..f2b54d67 100644 --- a/src/xors.c +++ b/src/xors.c @@ -67,7 +67,7 @@ copy_literals (kissat * solver, unsigned lit, const value value = values[other]; if (value > 0) { - kissat_eliminate_clause (solver, c, other); + kissat_mark_clause_as_garbage (solver, c); LOG ("found satisfied %s", LOGLIT (other)); return UINT_MAX; } @@ -160,7 +160,7 @@ match_lits_ref (kissat * solver, const value * marks, const value * values, const value value = values[lit]; if (value > 0) { - kissat_eliminate_clause (solver, c, INVALID_LIT); + kissat_mark_clause_as_garbage (solver, c); return false; } if (value < 0) @@ -229,7 +229,7 @@ kissat_find_xor_gate (kissat * solver, unsigned lit, unsigned negative) if (!GET_OPTION (xors)) return false; - const unsigned size_limit = solver->bounds.xor.clause_size; + const unsigned size_limit = GET_OPTION (xorsclslim); if (size_limit < 3) return false; assert (size_limit < 32); @@ -264,7 +264,7 @@ kissat_find_xor_gate (kissat * solver, unsigned lit, unsigned negative) const value *const values = solver->values; value *marks = solver->marks; - const unsigned steps_limit = solver->bounds.eliminate.occurrences; + const unsigned steps_limit = GET_OPTION (eliminateocclim); uint64_t steps = 0; diff --git a/test/cnf/miter1.cnf b/test/cnf/miter1.cnf new file mode 100644 index 00000000..0495f719 --- /dev/null +++ b/test/cnf/miter1.cnf @@ -0,0 +1,2495 @@ +c --backbone=0 +c --failed=0 +c --mineffort=1000000 +c --probeinit=0 +c --ternary=0 +c --transitive=0 +p cnf 865 2488 +-37 -1 0 +-37 2 0 +37 1 -2 0 +-38 -3 0 +-38 37 0 +38 3 -37 0 +-39 13 0 +-39 -38 0 +39 -13 38 0 +-40 18 0 +-40 32 0 +40 -18 -32 0 +-41 26 0 +-41 40 0 +41 -26 -40 0 +-42 36 0 +-42 41 0 +42 -36 -41 0 +-43 20 0 +-43 42 0 +43 -20 -42 0 +-44 28 0 +-44 43 0 +44 -28 -43 0 +-45 13 0 +-45 -44 0 +45 -13 44 0 +-46 -13 0 +-46 44 0 +46 13 -44 0 +-47 -45 0 +-47 -46 0 +47 45 46 0 +-48 38 0 +-48 -47 0 +48 -38 47 0 +-49 -39 0 +-49 -48 0 +49 39 48 0 +-50 -1 0 +-50 2 0 +50 1 -2 0 +-51 -3 0 +-51 50 0 +51 3 -50 0 +-52 13 0 +-52 -51 0 +52 -13 51 0 +-53 18 0 +-53 32 0 +53 -18 -32 0 +-54 26 0 +-54 53 0 +54 -26 -53 0 +-55 36 0 +-55 54 0 +55 -36 -54 0 +-56 20 0 +-56 55 0 +56 -20 -55 0 +-57 28 0 +-57 56 0 +57 -28 -56 0 +-58 13 0 +-58 -57 0 +58 -13 57 0 +-59 -13 0 +-59 57 0 +59 13 -57 0 +-60 -58 0 +-60 -59 0 +60 58 59 0 +-61 51 0 +-61 -60 0 +61 -51 60 0 +-62 -52 0 +-62 -61 0 +62 52 61 0 +-63 49 0 +-63 -62 0 +63 -49 62 0 +-64 -49 0 +-64 62 0 +64 49 -62 0 +-65 -63 0 +-65 -64 0 +65 63 64 0 +-66 -1 0 +-66 -3 0 +66 1 3 0 +-67 1 0 +-67 -3 0 +67 -1 3 0 +-68 -3 0 +-68 -67 0 +68 3 67 0 +-69 -66 0 +-69 68 0 +69 66 -68 0 +-70 -2 0 +-70 -14 0 +70 2 14 0 +-71 25 0 +-71 34 0 +71 -25 -34 0 +-72 16 0 +-72 71 0 +72 -16 -71 0 +-73 31 0 +-73 72 0 +73 -31 -72 0 +-74 23 0 +-74 73 0 +74 -23 -73 0 +-75 14 0 +-75 74 0 +75 -14 -74 0 +-76 -14 0 +-76 -74 0 +76 14 74 0 +-77 -75 0 +-77 -76 0 +77 75 76 0 +-78 2 0 +-78 -77 0 +78 -2 77 0 +-79 -70 0 +-79 -78 0 +79 70 78 0 +-80 -1 0 +-80 -79 0 +80 1 79 0 +-81 1 0 +-81 9 0 +81 -1 -9 0 +-82 -80 0 +-82 -81 0 +82 80 81 0 +-83 -3 0 +-83 -82 0 +83 3 82 0 +-84 -3 0 +-84 -83 0 +84 3 83 0 +-85 -69 0 +-85 -84 0 +85 69 84 0 +-86 -14 0 +-86 69 0 +86 14 -69 0 +-87 -85 0 +-87 -86 0 +87 85 86 0 +-88 -1 0 +-88 -3 0 +88 1 3 0 +-89 1 0 +-89 -3 0 +89 -1 3 0 +-90 -3 0 +-90 -89 0 +90 3 89 0 +-91 -88 0 +-91 90 0 +91 88 -90 0 +-92 -2 0 +-92 -14 0 +92 2 14 0 +-93 25 0 +-93 34 0 +93 -25 -34 0 +-94 16 0 +-94 93 0 +94 -16 -93 0 +-95 31 0 +-95 94 0 +95 -31 -94 0 +-96 23 0 +-96 95 0 +96 -23 -95 0 +-97 14 0 +-97 96 0 +97 -14 -96 0 +-98 -14 0 +-98 -96 0 +98 14 96 0 +-99 -97 0 +-99 -98 0 +99 97 98 0 +-100 2 0 +-100 -99 0 +100 -2 99 0 +-101 -92 0 +-101 -100 0 +101 92 100 0 +-102 -1 0 +-102 -101 0 +102 1 101 0 +-103 1 0 +-103 9 0 +103 -1 -9 0 +-104 -102 0 +-104 -103 0 +104 102 103 0 +-105 -3 0 +-105 -104 0 +105 3 104 0 +-106 -3 0 +-106 -105 0 +106 3 105 0 +-107 -91 0 +-107 -106 0 +107 91 106 0 +-108 -14 0 +-108 91 0 +108 14 -91 0 +-109 -107 0 +-109 -108 0 +109 107 108 0 +-110 -87 0 +-110 109 0 +110 87 -109 0 +-111 87 0 +-111 -109 0 +111 -87 109 0 +-112 -110 0 +-112 -111 0 +112 110 111 0 +-113 65 0 +-113 112 0 +113 -65 -112 0 +-114 -1 0 +-114 -15 0 +114 1 15 0 +-115 4 0 +-115 32 0 +115 -4 -32 0 +-116 18 0 +-116 115 0 +116 -18 -115 0 +-117 -18 0 +-117 -115 0 +117 18 115 0 +-118 -116 0 +-118 -117 0 +118 116 117 0 +-119 5 0 +-119 -118 0 +119 -5 118 0 +-120 -18 0 +-120 115 0 +120 18 -115 0 +-121 18 0 +-121 -115 0 +121 -18 115 0 +-122 -120 0 +-122 -121 0 +122 120 121 0 +-123 -5 0 +-123 -122 0 +123 5 122 0 +-124 -119 0 +-124 -123 0 +124 119 123 0 +-125 1 0 +-125 -124 0 +125 -1 124 0 +-126 -114 0 +-126 -125 0 +126 114 125 0 +-127 -3 0 +-127 -126 0 +127 3 126 0 +-128 -18 0 +-128 -32 0 +128 18 32 0 +-129 -40 0 +-129 -128 0 +129 40 128 0 +-130 3 0 +-130 -129 0 +130 -3 129 0 +-131 -127 0 +-131 -130 0 +131 127 130 0 +-132 -1 0 +-132 -15 0 +132 1 15 0 +-133 4 0 +-133 32 0 +133 -4 -32 0 +-134 18 0 +-134 133 0 +134 -18 -133 0 +-135 -18 0 +-135 -133 0 +135 18 133 0 +-136 -134 0 +-136 -135 0 +136 134 135 0 +-137 5 0 +-137 -136 0 +137 -5 136 0 +-138 -18 0 +-138 133 0 +138 18 -133 0 +-139 18 0 +-139 -133 0 +139 -18 133 0 +-140 -138 0 +-140 -139 0 +140 138 139 0 +-141 -5 0 +-141 -140 0 +141 5 140 0 +-142 -137 0 +-142 -141 0 +142 137 141 0 +-143 1 0 +-143 -142 0 +143 -1 142 0 +-144 -132 0 +-144 -143 0 +144 132 143 0 +-145 -3 0 +-145 -144 0 +145 3 144 0 +-146 -18 0 +-146 -32 0 +146 18 32 0 +-147 -53 0 +-147 -146 0 +147 53 146 0 +-148 3 0 +-148 -147 0 +148 -3 147 0 +-149 -145 0 +-149 -148 0 +149 145 148 0 +-150 -131 0 +-150 149 0 +150 131 -149 0 +-151 131 0 +-151 -149 0 +151 -131 149 0 +-152 -150 0 +-152 -151 0 +152 150 151 0 +-153 113 0 +-153 152 0 +153 -113 -152 0 +-154 -2 0 +-154 -16 0 +154 2 16 0 +-155 -16 0 +-155 -71 0 +155 16 71 0 +-156 -72 0 +-156 -155 0 +156 72 155 0 +-157 2 0 +-157 -156 0 +157 -2 156 0 +-158 -154 0 +-158 -157 0 +158 154 157 0 +-159 -1 0 +-159 -158 0 +159 1 158 0 +-160 1 0 +-160 6 0 +160 -1 -6 0 +-161 -159 0 +-161 -160 0 +161 159 160 0 +-162 -3 0 +-162 -161 0 +162 3 161 0 +-163 -3 0 +-163 -162 0 +163 3 162 0 +-164 -69 0 +-164 -163 0 +164 69 163 0 +-165 -16 0 +-165 69 0 +165 16 -69 0 +-166 -164 0 +-166 -165 0 +166 164 165 0 +-167 -2 0 +-167 -16 0 +167 2 16 0 +-168 -16 0 +-168 -93 0 +168 16 93 0 +-169 -94 0 +-169 -168 0 +169 94 168 0 +-170 2 0 +-170 -169 0 +170 -2 169 0 +-171 -167 0 +-171 -170 0 +171 167 170 0 +-172 -1 0 +-172 -171 0 +172 1 171 0 +-173 1 0 +-173 6 0 +173 -1 -6 0 +-174 -172 0 +-174 -173 0 +174 172 173 0 +-175 -3 0 +-175 -174 0 +175 3 174 0 +-176 -3 0 +-176 -175 0 +176 3 175 0 +-177 -91 0 +-177 -176 0 +177 91 176 0 +-178 -16 0 +-178 91 0 +178 16 -91 0 +-179 -177 0 +-179 -178 0 +179 177 178 0 +-180 -166 0 +-180 179 0 +180 166 -179 0 +-181 166 0 +-181 -179 0 +181 -166 179 0 +-182 -180 0 +-182 -181 0 +182 180 181 0 +-183 153 0 +-183 182 0 +183 -153 -182 0 +-184 -1 0 +-184 -17 0 +184 1 17 0 +-185 -18 0 +-185 -120 0 +185 18 120 0 +-186 5 0 +-186 -185 0 +186 -5 185 0 +-187 -5 0 +-187 116 0 +187 5 -116 0 +-188 -186 0 +-188 -187 0 +188 186 187 0 +-189 -26 0 +-189 -188 0 +189 26 188 0 +-190 -26 0 +-190 -189 0 +190 26 189 0 +-191 6 0 +-191 -190 0 +191 -6 190 0 +-192 26 0 +-192 -188 0 +192 -26 188 0 +-193 -6 0 +-193 192 0 +193 6 -192 0 +-194 -191 0 +-194 -193 0 +194 191 193 0 +-195 -36 0 +-195 -194 0 +195 36 194 0 +-196 -36 0 +-196 -195 0 +196 36 195 0 +-197 7 0 +-197 -196 0 +197 -7 196 0 +-198 36 0 +-198 -194 0 +198 -36 194 0 +-199 -7 0 +-199 198 0 +199 7 -198 0 +-200 -197 0 +-200 -199 0 +200 197 199 0 +-201 20 0 +-201 -200 0 +201 -20 200 0 +-202 -20 0 +-202 200 0 +202 20 -200 0 +-203 -201 0 +-203 -202 0 +203 201 202 0 +-204 8 0 +-204 -203 0 +204 -8 203 0 +-205 -20 0 +-205 -200 0 +205 20 200 0 +-206 20 0 +-206 200 0 +206 -20 -200 0 +-207 -205 0 +-207 -206 0 +207 205 206 0 +-208 -8 0 +-208 -207 0 +208 8 207 0 +-209 -204 0 +-209 -208 0 +209 204 208 0 +-210 1 0 +-210 -209 0 +210 -1 209 0 +-211 -184 0 +-211 -210 0 +211 184 210 0 +-212 -3 0 +-212 -211 0 +212 3 211 0 +-213 -26 0 +-213 128 0 +213 26 -128 0 +-214 -36 0 +-214 213 0 +214 36 -213 0 +-215 20 0 +-215 -214 0 +215 -20 214 0 +-216 -20 0 +-216 214 0 +216 20 -214 0 +-217 -215 0 +-217 -216 0 +217 215 216 0 +-218 3 0 +-218 -217 0 +218 -3 217 0 +-219 -212 0 +-219 -218 0 +219 212 218 0 +-220 -1 0 +-220 -17 0 +220 1 17 0 +-221 -18 0 +-221 -138 0 +221 18 138 0 +-222 5 0 +-222 -221 0 +222 -5 221 0 +-223 -5 0 +-223 134 0 +223 5 -134 0 +-224 -222 0 +-224 -223 0 +224 222 223 0 +-225 -26 0 +-225 -224 0 +225 26 224 0 +-226 -26 0 +-226 -225 0 +226 26 225 0 +-227 6 0 +-227 -226 0 +227 -6 226 0 +-228 26 0 +-228 -224 0 +228 -26 224 0 +-229 -6 0 +-229 228 0 +229 6 -228 0 +-230 -227 0 +-230 -229 0 +230 227 229 0 +-231 -36 0 +-231 -230 0 +231 36 230 0 +-232 -36 0 +-232 -231 0 +232 36 231 0 +-233 7 0 +-233 -232 0 +233 -7 232 0 +-234 36 0 +-234 -230 0 +234 -36 230 0 +-235 -7 0 +-235 234 0 +235 7 -234 0 +-236 -233 0 +-236 -235 0 +236 233 235 0 +-237 20 0 +-237 -236 0 +237 -20 236 0 +-238 -20 0 +-238 236 0 +238 20 -236 0 +-239 -237 0 +-239 -238 0 +239 237 238 0 +-240 8 0 +-240 -239 0 +240 -8 239 0 +-241 -20 0 +-241 -236 0 +241 20 236 0 +-242 20 0 +-242 236 0 +242 -20 -236 0 +-243 -241 0 +-243 -242 0 +243 241 242 0 +-244 -8 0 +-244 -243 0 +244 8 243 0 +-245 -240 0 +-245 -244 0 +245 240 244 0 +-246 1 0 +-246 -245 0 +246 -1 245 0 +-247 -220 0 +-247 -246 0 +247 220 246 0 +-248 -3 0 +-248 -247 0 +248 3 247 0 +-249 -26 0 +-249 146 0 +249 26 -146 0 +-250 -36 0 +-250 249 0 +250 36 -249 0 +-251 20 0 +-251 -250 0 +251 -20 250 0 +-252 -20 0 +-252 250 0 +252 20 -250 0 +-253 -251 0 +-253 -252 0 +253 251 252 0 +-254 3 0 +-254 -253 0 +254 -3 253 0 +-255 -248 0 +-255 -254 0 +255 248 254 0 +-256 -219 0 +-256 255 0 +256 219 -255 0 +-257 219 0 +-257 -255 0 +257 -219 255 0 +-258 -256 0 +-258 -257 0 +258 256 257 0 +-259 183 0 +-259 258 0 +259 -183 -258 0 +-260 18 0 +-260 -38 0 +260 -18 38 0 +-261 18 0 +-261 -32 0 +261 -18 32 0 +-262 -18 0 +-262 32 0 +262 18 -32 0 +-263 -261 0 +-263 -262 0 +263 261 262 0 +-264 38 0 +-264 -263 0 +264 -38 263 0 +-265 -260 0 +-265 -264 0 +265 260 264 0 +-266 18 0 +-266 -51 0 +266 -18 51 0 +-267 18 0 +-267 -32 0 +267 -18 32 0 +-268 -18 0 +-268 32 0 +268 18 -32 0 +-269 -267 0 +-269 -268 0 +269 267 268 0 +-270 51 0 +-270 -269 0 +270 -51 269 0 +-271 -266 0 +-271 -270 0 +271 266 270 0 +-272 265 0 +-272 -271 0 +272 -265 271 0 +-273 -265 0 +-273 271 0 +273 265 -271 0 +-274 -272 0 +-274 -273 0 +274 272 273 0 +-275 259 0 +-275 274 0 +275 -259 -274 0 +-276 -1 0 +-276 -19 0 +276 1 19 0 +-277 -20 0 +-277 -205 0 +277 20 205 0 +-278 8 0 +-278 -277 0 +278 -8 277 0 +-279 -8 0 +-279 201 0 +279 8 -201 0 +-280 -278 0 +-280 -279 0 +280 278 279 0 +-281 -28 0 +-281 -280 0 +281 28 280 0 +-282 -28 0 +-282 -281 0 +282 28 281 0 +-283 9 0 +-283 -282 0 +283 -9 282 0 +-284 28 0 +-284 -280 0 +284 -28 280 0 +-285 -9 0 +-285 284 0 +285 9 -284 0 +-286 -283 0 +-286 -285 0 +286 283 285 0 +-287 -13 0 +-287 -286 0 +287 13 286 0 +-288 -13 0 +-288 -287 0 +288 13 287 0 +-289 10 0 +-289 -288 0 +289 -10 288 0 +-290 13 0 +-290 -286 0 +290 -13 286 0 +-291 -10 0 +-291 290 0 +291 10 -290 0 +-292 -289 0 +-292 -291 0 +292 289 291 0 +-293 22 0 +-293 -292 0 +293 -22 292 0 +-294 -22 0 +-294 292 0 +294 22 -292 0 +-295 -293 0 +-295 -294 0 +295 293 294 0 +-296 11 0 +-296 -295 0 +296 -11 295 0 +-297 -22 0 +-297 -292 0 +297 22 292 0 +-298 22 0 +-298 292 0 +298 -22 -292 0 +-299 -297 0 +-299 -298 0 +299 297 298 0 +-300 -11 0 +-300 -299 0 +300 11 299 0 +-301 -296 0 +-301 -300 0 +301 296 300 0 +-302 1 0 +-302 -301 0 +302 -1 301 0 +-303 -276 0 +-303 -302 0 +303 276 302 0 +-304 -3 0 +-304 -303 0 +304 3 303 0 +-305 -28 0 +-305 216 0 +305 28 -216 0 +-306 -13 0 +-306 305 0 +306 13 -305 0 +-307 22 0 +-307 -306 0 +307 -22 306 0 +-308 -22 0 +-308 306 0 +308 22 -306 0 +-309 -307 0 +-309 -308 0 +309 307 308 0 +-310 3 0 +-310 -309 0 +310 -3 309 0 +-311 -304 0 +-311 -310 0 +311 304 310 0 +-312 -1 0 +-312 -19 0 +312 1 19 0 +-313 -20 0 +-313 -241 0 +313 20 241 0 +-314 8 0 +-314 -313 0 +314 -8 313 0 +-315 -8 0 +-315 237 0 +315 8 -237 0 +-316 -314 0 +-316 -315 0 +316 314 315 0 +-317 -28 0 +-317 -316 0 +317 28 316 0 +-318 -28 0 +-318 -317 0 +318 28 317 0 +-319 9 0 +-319 -318 0 +319 -9 318 0 +-320 28 0 +-320 -316 0 +320 -28 316 0 +-321 -9 0 +-321 320 0 +321 9 -320 0 +-322 -319 0 +-322 -321 0 +322 319 321 0 +-323 -13 0 +-323 -322 0 +323 13 322 0 +-324 -13 0 +-324 -323 0 +324 13 323 0 +-325 10 0 +-325 -324 0 +325 -10 324 0 +-326 13 0 +-326 -322 0 +326 -13 322 0 +-327 -10 0 +-327 326 0 +327 10 -326 0 +-328 -325 0 +-328 -327 0 +328 325 327 0 +-329 22 0 +-329 -328 0 +329 -22 328 0 +-330 -22 0 +-330 328 0 +330 22 -328 0 +-331 -329 0 +-331 -330 0 +331 329 330 0 +-332 11 0 +-332 -331 0 +332 -11 331 0 +-333 -22 0 +-333 -328 0 +333 22 328 0 +-334 22 0 +-334 328 0 +334 -22 -328 0 +-335 -333 0 +-335 -334 0 +335 333 334 0 +-336 -11 0 +-336 -335 0 +336 11 335 0 +-337 -332 0 +-337 -336 0 +337 332 336 0 +-338 1 0 +-338 -337 0 +338 -1 337 0 +-339 -312 0 +-339 -338 0 +339 312 338 0 +-340 -3 0 +-340 -339 0 +340 3 339 0 +-341 -28 0 +-341 252 0 +341 28 -252 0 +-342 -13 0 +-342 341 0 +342 13 -341 0 +-343 22 0 +-343 -342 0 +343 -22 342 0 +-344 -22 0 +-344 342 0 +344 22 -342 0 +-345 -343 0 +-345 -344 0 +345 343 344 0 +-346 3 0 +-346 -345 0 +346 -3 345 0 +-347 -340 0 +-347 -346 0 +347 340 346 0 +-348 -311 0 +-348 347 0 +348 311 -347 0 +-349 311 0 +-349 -347 0 +349 -311 347 0 +-350 -348 0 +-350 -349 0 +350 348 349 0 +-351 275 0 +-351 350 0 +351 -275 -350 0 +-352 20 0 +-352 -38 0 +352 -20 38 0 +-353 20 0 +-353 -42 0 +353 -20 42 0 +-354 -20 0 +-354 42 0 +354 20 -42 0 +-355 -353 0 +-355 -354 0 +355 353 354 0 +-356 38 0 +-356 -355 0 +356 -38 355 0 +-357 -352 0 +-357 -356 0 +357 352 356 0 +-358 20 0 +-358 -51 0 +358 -20 51 0 +-359 20 0 +-359 -55 0 +359 -20 55 0 +-360 -20 0 +-360 55 0 +360 20 -55 0 +-361 -359 0 +-361 -360 0 +361 359 360 0 +-362 51 0 +-362 -361 0 +362 -51 361 0 +-363 -358 0 +-363 -362 0 +363 358 362 0 +-364 357 0 +-364 -363 0 +364 -357 363 0 +-365 -357 0 +-365 363 0 +365 357 -363 0 +-366 -364 0 +-366 -365 0 +366 364 365 0 +-367 351 0 +-367 366 0 +367 -351 -366 0 +-368 -2 0 +-368 -21 0 +368 2 21 0 +-369 29 0 +-369 75 0 +369 -29 -75 0 +-370 21 0 +-370 369 0 +370 -21 -369 0 +-371 -21 0 +-371 -369 0 +371 21 369 0 +-372 -370 0 +-372 -371 0 +372 370 371 0 +-373 2 0 +-373 -372 0 +373 -2 372 0 +-374 -368 0 +-374 -373 0 +374 368 373 0 +-375 -1 0 +-375 -374 0 +375 1 374 0 +-376 1 0 +-376 11 0 +376 -1 -11 0 +-377 -375 0 +-377 -376 0 +377 375 376 0 +-378 -3 0 +-378 -377 0 +378 3 377 0 +-379 -3 0 +-379 -378 0 +379 3 378 0 +-380 -69 0 +-380 -379 0 +380 69 379 0 +-381 -21 0 +-381 69 0 +381 21 -69 0 +-382 -380 0 +-382 -381 0 +382 380 381 0 +-383 -2 0 +-383 -21 0 +383 2 21 0 +-384 29 0 +-384 97 0 +384 -29 -97 0 +-385 21 0 +-385 384 0 +385 -21 -384 0 +-386 -21 0 +-386 -384 0 +386 21 384 0 +-387 -385 0 +-387 -386 0 +387 385 386 0 +-388 2 0 +-388 -387 0 +388 -2 387 0 +-389 -383 0 +-389 -388 0 +389 383 388 0 +-390 -1 0 +-390 -389 0 +390 1 389 0 +-391 1 0 +-391 11 0 +391 -1 -11 0 +-392 -390 0 +-392 -391 0 +392 390 391 0 +-393 -3 0 +-393 -392 0 +393 3 392 0 +-394 -3 0 +-394 -393 0 +394 3 393 0 +-395 -91 0 +-395 -394 0 +395 91 394 0 +-396 -21 0 +-396 91 0 +396 21 -91 0 +-397 -395 0 +-397 -396 0 +397 395 396 0 +-398 -382 0 +-398 397 0 +398 382 -397 0 +-399 382 0 +-399 -397 0 +399 -382 397 0 +-400 -398 0 +-400 -399 0 +400 398 399 0 +-401 367 0 +-401 400 0 +401 -367 -400 0 +-402 22 0 +-402 -38 0 +402 -22 38 0 +-403 13 0 +-403 44 0 +403 -13 -44 0 +-404 22 0 +-404 -403 0 +404 -22 403 0 +-405 -22 0 +-405 403 0 +405 22 -403 0 +-406 -404 0 +-406 -405 0 +406 404 405 0 +-407 38 0 +-407 -406 0 +407 -38 406 0 +-408 -402 0 +-408 -407 0 +408 402 407 0 +-409 22 0 +-409 -51 0 +409 -22 51 0 +-410 13 0 +-410 57 0 +410 -13 -57 0 +-411 22 0 +-411 -410 0 +411 -22 410 0 +-412 -22 0 +-412 410 0 +412 22 -410 0 +-413 -411 0 +-413 -412 0 +413 411 412 0 +-414 51 0 +-414 -413 0 +414 -51 413 0 +-415 -409 0 +-415 -414 0 +415 409 414 0 +-416 408 0 +-416 -415 0 +416 -408 415 0 +-417 -408 0 +-417 415 0 +417 408 -415 0 +-418 -416 0 +-418 -417 0 +418 416 417 0 +-419 401 0 +-419 418 0 +419 -401 -418 0 +-420 -2 0 +-420 -23 0 +420 2 23 0 +-421 -23 0 +-421 -73 0 +421 23 73 0 +-422 -74 0 +-422 -421 0 +422 74 421 0 +-423 2 0 +-423 -422 0 +423 -2 422 0 +-424 -420 0 +-424 -423 0 +424 420 423 0 +-425 -1 0 +-425 -424 0 +425 1 424 0 +-426 1 0 +-426 8 0 +426 -1 -8 0 +-427 -425 0 +-427 -426 0 +427 425 426 0 +-428 -3 0 +-428 -427 0 +428 3 427 0 +-429 -3 0 +-429 -428 0 +429 3 428 0 +-430 -69 0 +-430 -429 0 +430 69 429 0 +-431 -23 0 +-431 69 0 +431 23 -69 0 +-432 -430 0 +-432 -431 0 +432 430 431 0 +-433 -2 0 +-433 -23 0 +433 2 23 0 +-434 -23 0 +-434 -95 0 +434 23 95 0 +-435 -96 0 +-435 -434 0 +435 96 434 0 +-436 2 0 +-436 -435 0 +436 -2 435 0 +-437 -433 0 +-437 -436 0 +437 433 436 0 +-438 -1 0 +-438 -437 0 +438 1 437 0 +-439 1 0 +-439 8 0 +439 -1 -8 0 +-440 -438 0 +-440 -439 0 +440 438 439 0 +-441 -3 0 +-441 -440 0 +441 3 440 0 +-442 -3 0 +-442 -441 0 +442 3 441 0 +-443 -91 0 +-443 -442 0 +443 91 442 0 +-444 -23 0 +-444 91 0 +444 23 -91 0 +-445 -443 0 +-445 -444 0 +445 443 444 0 +-446 -432 0 +-446 445 0 +446 432 -445 0 +-447 432 0 +-447 -445 0 +447 -432 445 0 +-448 -446 0 +-448 -447 0 +448 446 447 0 +-449 419 0 +-449 448 0 +449 -419 -448 0 +-450 -1 0 +-450 -24 0 +450 1 24 0 +-451 -26 0 +-451 188 0 +451 26 -188 0 +-452 -192 0 +-452 -451 0 +452 192 451 0 +-453 6 0 +-453 -452 0 +453 -6 452 0 +-454 26 0 +-454 188 0 +454 -26 -188 0 +-455 -189 0 +-455 -454 0 +455 189 454 0 +-456 -6 0 +-456 -455 0 +456 6 455 0 +-457 -453 0 +-457 -456 0 +457 453 456 0 +-458 1 0 +-458 -457 0 +458 -1 457 0 +-459 -450 0 +-459 -458 0 +459 450 458 0 +-460 -3 0 +-460 -459 0 +460 3 459 0 +-461 26 0 +-461 -128 0 +461 -26 128 0 +-462 -213 0 +-462 -461 0 +462 213 461 0 +-463 3 0 +-463 -462 0 +463 -3 462 0 +-464 -460 0 +-464 -463 0 +464 460 463 0 +-465 -1 0 +-465 -24 0 +465 1 24 0 +-466 -26 0 +-466 224 0 +466 26 -224 0 +-467 -228 0 +-467 -466 0 +467 228 466 0 +-468 6 0 +-468 -467 0 +468 -6 467 0 +-469 26 0 +-469 224 0 +469 -26 -224 0 +-470 -225 0 +-470 -469 0 +470 225 469 0 +-471 -6 0 +-471 -470 0 +471 6 470 0 +-472 -468 0 +-472 -471 0 +472 468 471 0 +-473 1 0 +-473 -472 0 +473 -1 472 0 +-474 -465 0 +-474 -473 0 +474 465 473 0 +-475 -3 0 +-475 -474 0 +475 3 474 0 +-476 26 0 +-476 -146 0 +476 -26 146 0 +-477 -249 0 +-477 -476 0 +477 249 476 0 +-478 3 0 +-478 -477 0 +478 -3 477 0 +-479 -475 0 +-479 -478 0 +479 475 478 0 +-480 -464 0 +-480 479 0 +480 464 -479 0 +-481 464 0 +-481 -479 0 +481 -464 479 0 +-482 -480 0 +-482 -481 0 +482 480 481 0 +-483 449 0 +-483 482 0 +483 -449 -482 0 +-484 -2 0 +-484 -25 0 +484 2 25 0 +-485 -25 0 +-485 -34 0 +485 25 34 0 +-486 -71 0 +-486 -485 0 +486 71 485 0 +-487 2 0 +-487 -486 0 +487 -2 486 0 +-488 -484 0 +-488 -487 0 +488 484 487 0 +-489 -1 0 +-489 -488 0 +489 1 488 0 +-490 1 0 +-490 5 0 +490 -1 -5 0 +-491 -489 0 +-491 -490 0 +491 489 490 0 +-492 -3 0 +-492 -491 0 +492 3 491 0 +-493 -3 0 +-493 -492 0 +493 3 492 0 +-494 -69 0 +-494 -493 0 +494 69 493 0 +-495 -25 0 +-495 69 0 +495 25 -69 0 +-496 -494 0 +-496 -495 0 +496 494 495 0 +-497 -2 0 +-497 -25 0 +497 2 25 0 +-498 -25 0 +-498 -34 0 +498 25 34 0 +-499 -93 0 +-499 -498 0 +499 93 498 0 +-500 2 0 +-500 -499 0 +500 -2 499 0 +-501 -497 0 +-501 -500 0 +501 497 500 0 +-502 -1 0 +-502 -501 0 +502 1 501 0 +-503 1 0 +-503 5 0 +503 -1 -5 0 +-504 -502 0 +-504 -503 0 +504 502 503 0 +-505 -3 0 +-505 -504 0 +505 3 504 0 +-506 -3 0 +-506 -505 0 +506 3 505 0 +-507 -91 0 +-507 -506 0 +507 91 506 0 +-508 -25 0 +-508 91 0 +508 25 -91 0 +-509 -507 0 +-509 -508 0 +509 507 508 0 +-510 -496 0 +-510 509 0 +510 496 -509 0 +-511 496 0 +-511 -509 0 +511 -496 509 0 +-512 -510 0 +-512 -511 0 +512 510 511 0 +-513 483 0 +-513 512 0 +513 -483 -512 0 +-514 26 0 +-514 -38 0 +514 -26 38 0 +-515 26 0 +-515 -40 0 +515 -26 40 0 +-516 -26 0 +-516 40 0 +516 26 -40 0 +-517 -515 0 +-517 -516 0 +517 515 516 0 +-518 38 0 +-518 -517 0 +518 -38 517 0 +-519 -514 0 +-519 -518 0 +519 514 518 0 +-520 26 0 +-520 -51 0 +520 -26 51 0 +-521 26 0 +-521 -53 0 +521 -26 53 0 +-522 -26 0 +-522 53 0 +522 26 -53 0 +-523 -521 0 +-523 -522 0 +523 521 522 0 +-524 51 0 +-524 -523 0 +524 -51 523 0 +-525 -520 0 +-525 -524 0 +525 520 524 0 +-526 519 0 +-526 -525 0 +526 -519 525 0 +-527 -519 0 +-527 525 0 +527 519 -525 0 +-528 -526 0 +-528 -527 0 +528 526 527 0 +-529 513 0 +-529 528 0 +529 -513 -528 0 +-530 -1 0 +-530 -27 0 +530 1 27 0 +-531 -28 0 +-531 280 0 +531 28 -280 0 +-532 -284 0 +-532 -531 0 +532 284 531 0 +-533 9 0 +-533 -532 0 +533 -9 532 0 +-534 28 0 +-534 280 0 +534 -28 -280 0 +-535 -281 0 +-535 -534 0 +535 281 534 0 +-536 -9 0 +-536 -535 0 +536 9 535 0 +-537 -533 0 +-537 -536 0 +537 533 536 0 +-538 1 0 +-538 -537 0 +538 -1 537 0 +-539 -530 0 +-539 -538 0 +539 530 538 0 +-540 -3 0 +-540 -539 0 +540 3 539 0 +-541 28 0 +-541 -216 0 +541 -28 216 0 +-542 -305 0 +-542 -541 0 +542 305 541 0 +-543 3 0 +-543 -542 0 +543 -3 542 0 +-544 -540 0 +-544 -543 0 +544 540 543 0 +-545 -1 0 +-545 -27 0 +545 1 27 0 +-546 -28 0 +-546 316 0 +546 28 -316 0 +-547 -320 0 +-547 -546 0 +547 320 546 0 +-548 9 0 +-548 -547 0 +548 -9 547 0 +-549 28 0 +-549 316 0 +549 -28 -316 0 +-550 -317 0 +-550 -549 0 +550 317 549 0 +-551 -9 0 +-551 -550 0 +551 9 550 0 +-552 -548 0 +-552 -551 0 +552 548 551 0 +-553 1 0 +-553 -552 0 +553 -1 552 0 +-554 -545 0 +-554 -553 0 +554 545 553 0 +-555 -3 0 +-555 -554 0 +555 3 554 0 +-556 28 0 +-556 -252 0 +556 -28 252 0 +-557 -341 0 +-557 -556 0 +557 341 556 0 +-558 3 0 +-558 -557 0 +558 -3 557 0 +-559 -555 0 +-559 -558 0 +559 555 558 0 +-560 -544 0 +-560 559 0 +560 544 -559 0 +-561 544 0 +-561 -559 0 +561 -544 559 0 +-562 -560 0 +-562 -561 0 +562 560 561 0 +-563 529 0 +-563 562 0 +563 -529 -562 0 +-564 28 0 +-564 -38 0 +564 -28 38 0 +-565 28 0 +-565 -43 0 +565 -28 43 0 +-566 -28 0 +-566 43 0 +566 28 -43 0 +-567 -565 0 +-567 -566 0 +567 565 566 0 +-568 38 0 +-568 -567 0 +568 -38 567 0 +-569 -564 0 +-569 -568 0 +569 564 568 0 +-570 28 0 +-570 -51 0 +570 -28 51 0 +-571 28 0 +-571 -56 0 +571 -28 56 0 +-572 -28 0 +-572 56 0 +572 28 -56 0 +-573 -571 0 +-573 -572 0 +573 571 572 0 +-574 51 0 +-574 -573 0 +574 -51 573 0 +-575 -570 0 +-575 -574 0 +575 570 574 0 +-576 569 0 +-576 -575 0 +576 -569 575 0 +-577 -569 0 +-577 575 0 +577 569 -575 0 +-578 -576 0 +-578 -577 0 +578 576 577 0 +-579 563 0 +-579 578 0 +579 -563 -578 0 +-580 -2 0 +-580 -29 0 +580 2 29 0 +-581 -29 0 +-581 -75 0 +581 29 75 0 +-582 -369 0 +-582 -581 0 +582 369 581 0 +-583 2 0 +-583 -582 0 +583 -2 582 0 +-584 -580 0 +-584 -583 0 +584 580 583 0 +-585 -1 0 +-585 -584 0 +585 1 584 0 +-586 1 0 +-586 10 0 +586 -1 -10 0 +-587 -585 0 +-587 -586 0 +587 585 586 0 +-588 -3 0 +-588 -587 0 +588 3 587 0 +-589 -3 0 +-589 -588 0 +589 3 588 0 +-590 -69 0 +-590 -589 0 +590 69 589 0 +-591 -29 0 +-591 69 0 +591 29 -69 0 +-592 -590 0 +-592 -591 0 +592 590 591 0 +-593 -2 0 +-593 -29 0 +593 2 29 0 +-594 -29 0 +-594 -97 0 +594 29 97 0 +-595 -384 0 +-595 -594 0 +595 384 594 0 +-596 2 0 +-596 -595 0 +596 -2 595 0 +-597 -593 0 +-597 -596 0 +597 593 596 0 +-598 -1 0 +-598 -597 0 +598 1 597 0 +-599 1 0 +-599 10 0 +599 -1 -10 0 +-600 -598 0 +-600 -599 0 +600 598 599 0 +-601 -3 0 +-601 -600 0 +601 3 600 0 +-602 -3 0 +-602 -601 0 +602 3 601 0 +-603 -91 0 +-603 -602 0 +603 91 602 0 +-604 -29 0 +-604 91 0 +604 29 -91 0 +-605 -603 0 +-605 -604 0 +605 603 604 0 +-606 -592 0 +-606 605 0 +606 592 -605 0 +-607 592 0 +-607 -605 0 +607 -592 605 0 +-608 -606 0 +-608 -607 0 +608 606 607 0 +-609 579 0 +-609 608 0 +609 -579 -608 0 +-610 -1 0 +-610 -30 0 +610 1 30 0 +-611 4 0 +-611 -32 0 +611 -4 32 0 +-612 -4 0 +-612 32 0 +612 4 -32 0 +-613 -611 0 +-613 -612 0 +613 611 612 0 +-614 1 0 +-614 -613 0 +614 -1 613 0 +-615 -610 0 +-615 -614 0 +615 610 614 0 +-616 -3 0 +-616 -615 0 +616 3 615 0 +-617 3 0 +-617 -32 0 +617 -3 32 0 +-618 -616 0 +-618 -617 0 +618 616 617 0 +-619 -1 0 +-619 -30 0 +619 1 30 0 +-620 4 0 +-620 -32 0 +620 -4 32 0 +-621 -4 0 +-621 32 0 +621 4 -32 0 +-622 -620 0 +-622 -621 0 +622 620 621 0 +-623 1 0 +-623 -622 0 +623 -1 622 0 +-624 -619 0 +-624 -623 0 +624 619 623 0 +-625 -3 0 +-625 -624 0 +625 3 624 0 +-626 3 0 +-626 -32 0 +626 -3 32 0 +-627 -625 0 +-627 -626 0 +627 625 626 0 +-628 -618 0 +-628 627 0 +628 618 -627 0 +-629 618 0 +-629 -627 0 +629 -618 627 0 +-630 -628 0 +-630 -629 0 +630 628 629 0 +-631 609 0 +-631 630 0 +631 -609 -630 0 +-632 -2 0 +-632 -31 0 +632 2 31 0 +-633 -31 0 +-633 -72 0 +633 31 72 0 +-634 -73 0 +-634 -633 0 +634 73 633 0 +-635 2 0 +-635 -634 0 +635 -2 634 0 +-636 -632 0 +-636 -635 0 +636 632 635 0 +-637 -1 0 +-637 -636 0 +637 1 636 0 +-638 1 0 +-638 7 0 +638 -1 -7 0 +-639 -637 0 +-639 -638 0 +639 637 638 0 +-640 -3 0 +-640 -639 0 +640 3 639 0 +-641 -3 0 +-641 -640 0 +641 3 640 0 +-642 -69 0 +-642 -641 0 +642 69 641 0 +-643 -31 0 +-643 69 0 +643 31 -69 0 +-644 -642 0 +-644 -643 0 +644 642 643 0 +-645 -2 0 +-645 -31 0 +645 2 31 0 +-646 -31 0 +-646 -94 0 +646 31 94 0 +-647 -95 0 +-647 -646 0 +647 95 646 0 +-648 2 0 +-648 -647 0 +648 -2 647 0 +-649 -645 0 +-649 -648 0 +649 645 648 0 +-650 -1 0 +-650 -649 0 +650 1 649 0 +-651 1 0 +-651 7 0 +651 -1 -7 0 +-652 -650 0 +-652 -651 0 +652 650 651 0 +-653 -3 0 +-653 -652 0 +653 3 652 0 +-654 -3 0 +-654 -653 0 +654 3 653 0 +-655 -91 0 +-655 -654 0 +655 91 654 0 +-656 -31 0 +-656 91 0 +656 31 -91 0 +-657 -655 0 +-657 -656 0 +657 655 656 0 +-658 -644 0 +-658 657 0 +658 644 -657 0 +-659 644 0 +-659 -657 0 +659 -644 657 0 +-660 -658 0 +-660 -659 0 +660 658 659 0 +-661 631 0 +-661 660 0 +661 -631 -660 0 +-662 32 0 +-662 -38 0 +662 -32 38 0 +-663 -32 0 +-663 38 0 +663 32 -38 0 +-664 -662 0 +-664 -663 0 +664 662 663 0 +-665 32 0 +-665 -51 0 +665 -32 51 0 +-666 -32 0 +-666 51 0 +666 32 -51 0 +-667 -665 0 +-667 -666 0 +667 665 666 0 +-668 664 0 +-668 -667 0 +668 -664 667 0 +-669 -664 0 +-669 667 0 +669 664 -667 0 +-670 -668 0 +-670 -669 0 +670 668 669 0 +-671 661 0 +-671 670 0 +671 -661 -670 0 +-672 -1 0 +-672 -33 0 +672 1 33 0 +-673 -36 0 +-673 194 0 +673 36 -194 0 +-674 -198 0 +-674 -673 0 +674 198 673 0 +-675 7 0 +-675 -674 0 +675 -7 674 0 +-676 36 0 +-676 194 0 +676 -36 -194 0 +-677 -195 0 +-677 -676 0 +677 195 676 0 +-678 -7 0 +-678 -677 0 +678 7 677 0 +-679 -675 0 +-679 -678 0 +679 675 678 0 +-680 1 0 +-680 -679 0 +680 -1 679 0 +-681 -672 0 +-681 -680 0 +681 672 680 0 +-682 -3 0 +-682 -681 0 +682 3 681 0 +-683 36 0 +-683 -213 0 +683 -36 213 0 +-684 -214 0 +-684 -683 0 +684 214 683 0 +-685 3 0 +-685 -684 0 +685 -3 684 0 +-686 -682 0 +-686 -685 0 +686 682 685 0 +-687 -1 0 +-687 -33 0 +687 1 33 0 +-688 -36 0 +-688 230 0 +688 36 -230 0 +-689 -234 0 +-689 -688 0 +689 234 688 0 +-690 7 0 +-690 -689 0 +690 -7 689 0 +-691 36 0 +-691 230 0 +691 -36 -230 0 +-692 -231 0 +-692 -691 0 +692 231 691 0 +-693 -7 0 +-693 -692 0 +693 7 692 0 +-694 -690 0 +-694 -693 0 +694 690 693 0 +-695 1 0 +-695 -694 0 +695 -1 694 0 +-696 -687 0 +-696 -695 0 +696 687 695 0 +-697 -3 0 +-697 -696 0 +697 3 696 0 +-698 36 0 +-698 -249 0 +698 -36 249 0 +-699 -250 0 +-699 -698 0 +699 250 698 0 +-700 3 0 +-700 -699 0 +700 -3 699 0 +-701 -697 0 +-701 -700 0 +701 697 700 0 +-702 -686 0 +-702 701 0 +702 686 -701 0 +-703 686 0 +-703 -701 0 +703 -686 701 0 +-704 -702 0 +-704 -703 0 +704 702 703 0 +-705 671 0 +-705 704 0 +705 -671 -704 0 +-706 -2 0 +-706 -34 0 +706 2 34 0 +-707 2 0 +-707 34 0 +707 -2 -34 0 +-708 -706 0 +-708 -707 0 +708 706 707 0 +-709 -1 0 +-709 -708 0 +709 1 708 0 +-710 1 0 +-710 4 0 +710 -1 -4 0 +-711 -709 0 +-711 -710 0 +711 709 710 0 +-712 -3 0 +-712 -711 0 +712 3 711 0 +-713 -3 0 +-713 -712 0 +713 3 712 0 +-714 -69 0 +-714 -713 0 +714 69 713 0 +-715 -34 0 +-715 69 0 +715 34 -69 0 +-716 -714 0 +-716 -715 0 +716 714 715 0 +-717 -2 0 +-717 -34 0 +717 2 34 0 +-718 2 0 +-718 34 0 +718 -2 -34 0 +-719 -717 0 +-719 -718 0 +719 717 718 0 +-720 -1 0 +-720 -719 0 +720 1 719 0 +-721 1 0 +-721 4 0 +721 -1 -4 0 +-722 -720 0 +-722 -721 0 +722 720 721 0 +-723 -3 0 +-723 -722 0 +723 3 722 0 +-724 -3 0 +-724 -723 0 +724 3 723 0 +-725 -91 0 +-725 -724 0 +725 91 724 0 +-726 -34 0 +-726 91 0 +726 34 -91 0 +-727 -725 0 +-727 -726 0 +727 725 726 0 +-728 -716 0 +-728 727 0 +728 716 -727 0 +-729 716 0 +-729 -727 0 +729 -716 727 0 +-730 -728 0 +-730 -729 0 +730 728 729 0 +-731 705 0 +-731 730 0 +731 -705 -730 0 +-732 -1 0 +-732 -35 0 +732 1 35 0 +-733 -13 0 +-733 286 0 +733 13 -286 0 +-734 -290 0 +-734 -733 0 +734 290 733 0 +-735 10 0 +-735 -734 0 +735 -10 734 0 +-736 13 0 +-736 286 0 +736 -13 -286 0 +-737 -287 0 +-737 -736 0 +737 287 736 0 +-738 -10 0 +-738 -737 0 +738 10 737 0 +-739 -735 0 +-739 -738 0 +739 735 738 0 +-740 1 0 +-740 -739 0 +740 -1 739 0 +-741 -732 0 +-741 -740 0 +741 732 740 0 +-742 -3 0 +-742 -741 0 +742 3 741 0 +-743 13 0 +-743 -305 0 +743 -13 305 0 +-744 -306 0 +-744 -743 0 +744 306 743 0 +-745 3 0 +-745 -744 0 +745 -3 744 0 +-746 -742 0 +-746 -745 0 +746 742 745 0 +-747 -1 0 +-747 -35 0 +747 1 35 0 +-748 -13 0 +-748 322 0 +748 13 -322 0 +-749 -326 0 +-749 -748 0 +749 326 748 0 +-750 10 0 +-750 -749 0 +750 -10 749 0 +-751 13 0 +-751 322 0 +751 -13 -322 0 +-752 -323 0 +-752 -751 0 +752 323 751 0 +-753 -10 0 +-753 -752 0 +753 10 752 0 +-754 -750 0 +-754 -753 0 +754 750 753 0 +-755 1 0 +-755 -754 0 +755 -1 754 0 +-756 -747 0 +-756 -755 0 +756 747 755 0 +-757 -3 0 +-757 -756 0 +757 3 756 0 +-758 13 0 +-758 -341 0 +758 -13 341 0 +-759 -342 0 +-759 -758 0 +759 342 758 0 +-760 3 0 +-760 -759 0 +760 -3 759 0 +-761 -757 0 +-761 -760 0 +761 757 760 0 +-762 -746 0 +-762 761 0 +762 746 -761 0 +-763 746 0 +-763 -761 0 +763 -746 761 0 +-764 -762 0 +-764 -763 0 +764 762 763 0 +-765 731 0 +-765 764 0 +765 -731 -764 0 +-766 36 0 +-766 -38 0 +766 -36 38 0 +-767 36 0 +-767 -41 0 +767 -36 41 0 +-768 -36 0 +-768 41 0 +768 36 -41 0 +-769 -767 0 +-769 -768 0 +769 767 768 0 +-770 38 0 +-770 -769 0 +770 -38 769 0 +-771 -766 0 +-771 -770 0 +771 766 770 0 +-772 36 0 +-772 -51 0 +772 -36 51 0 +-773 36 0 +-773 -54 0 +773 -36 54 0 +-774 -36 0 +-774 54 0 +774 36 -54 0 +-775 -773 0 +-775 -774 0 +775 773 774 0 +-776 51 0 +-776 -775 0 +776 -51 775 0 +-777 -772 0 +-777 -776 0 +777 772 776 0 +-778 771 0 +-778 -777 0 +778 -771 777 0 +-779 -771 0 +-779 777 0 +779 771 -777 0 +-780 -778 0 +-780 -779 0 +780 778 779 0 +-781 765 0 +-781 780 0 +781 -765 -780 0 +-782 -19 0 +-782 -22 0 +782 19 22 0 +-783 19 0 +-783 22 0 +783 -19 -22 0 +-784 -782 0 +-784 -783 0 +784 782 783 0 +-785 -13 0 +-785 -35 0 +785 13 35 0 +-786 13 0 +-786 35 0 +786 -13 -35 0 +-787 -785 0 +-787 -786 0 +787 785 786 0 +-788 -27 0 +-788 -28 0 +788 27 28 0 +-789 27 0 +-789 28 0 +789 -27 -28 0 +-790 -788 0 +-790 -789 0 +790 788 789 0 +-791 -17 0 +-791 -20 0 +791 17 20 0 +-792 17 0 +-792 20 0 +792 -17 -20 0 +-793 -791 0 +-793 -792 0 +793 791 792 0 +-794 -33 0 +-794 -36 0 +794 33 36 0 +-795 33 0 +-795 36 0 +795 -33 -36 0 +-796 -794 0 +-796 -795 0 +796 794 795 0 +-797 -24 0 +-797 -26 0 +797 24 26 0 +-798 24 0 +-798 26 0 +798 -24 -26 0 +-799 -797 0 +-799 -798 0 +799 797 798 0 +-800 -30 0 +-800 -32 0 +800 30 32 0 +-801 30 0 +-801 32 0 +801 -30 -32 0 +-802 -800 0 +-802 -801 0 +802 800 801 0 +-803 -15 0 +-803 -18 0 +803 15 18 0 +-804 15 0 +-804 18 0 +804 -15 -18 0 +-805 -803 0 +-805 -804 0 +805 803 804 0 +-806 802 0 +-806 805 0 +806 -802 -805 0 +-807 799 0 +-807 806 0 +807 -799 -806 0 +-808 796 0 +-808 807 0 +808 -796 -807 0 +-809 793 0 +-809 808 0 +809 -793 -808 0 +-810 790 0 +-810 809 0 +810 -790 -809 0 +-811 787 0 +-811 810 0 +811 -787 -810 0 +-812 784 0 +-812 811 0 +812 -784 -811 0 +-813 2 0 +-813 812 0 +813 -2 -812 0 +-814 -1 0 +-814 813 0 +814 1 -813 0 +-815 -3 0 +-815 814 0 +815 3 -814 0 +-816 2 0 +-816 370 0 +816 -2 -370 0 +-817 -1 0 +-817 816 0 +817 1 -816 0 +-818 -3 0 +-818 817 0 +818 3 -817 0 +-819 -815 0 +-819 818 0 +819 815 -818 0 +-820 815 0 +-820 -818 0 +820 -815 818 0 +-821 -819 0 +-821 -820 0 +821 819 820 0 +-822 -19 0 +-822 -22 0 +822 19 22 0 +-823 19 0 +-823 22 0 +823 -19 -22 0 +-824 -822 0 +-824 -823 0 +824 822 823 0 +-825 -13 0 +-825 -35 0 +825 13 35 0 +-826 13 0 +-826 35 0 +826 -13 -35 0 +-827 -825 0 +-827 -826 0 +827 825 826 0 +-828 -27 0 +-828 -28 0 +828 27 28 0 +-829 27 0 +-829 28 0 +829 -27 -28 0 +-830 -828 0 +-830 -829 0 +830 828 829 0 +-831 -17 0 +-831 -20 0 +831 17 20 0 +-832 17 0 +-832 20 0 +832 -17 -20 0 +-833 -831 0 +-833 -832 0 +833 831 832 0 +-834 -33 0 +-834 -36 0 +834 33 36 0 +-835 33 0 +-835 36 0 +835 -33 -36 0 +-836 -834 0 +-836 -835 0 +836 834 835 0 +-837 -24 0 +-837 -26 0 +837 24 26 0 +-838 24 0 +-838 26 0 +838 -24 -26 0 +-839 -837 0 +-839 -838 0 +839 837 838 0 +-840 -30 0 +-840 -32 0 +840 30 32 0 +-841 30 0 +-841 32 0 +841 -30 -32 0 +-842 -840 0 +-842 -841 0 +842 840 841 0 +-843 -15 0 +-843 -18 0 +843 15 18 0 +-844 15 0 +-844 18 0 +844 -15 -18 0 +-845 -843 0 +-845 -844 0 +845 843 844 0 +-846 842 0 +-846 845 0 +846 -842 -845 0 +-847 839 0 +-847 846 0 +847 -839 -846 0 +-848 836 0 +-848 847 0 +848 -836 -847 0 +-849 833 0 +-849 848 0 +849 -833 -848 0 +-850 830 0 +-850 849 0 +850 -830 -849 0 +-851 827 0 +-851 850 0 +851 -827 -850 0 +-852 824 0 +-852 851 0 +852 -824 -851 0 +-853 2 0 +-853 852 0 +853 -2 -852 0 +-854 -1 0 +-854 853 0 +854 1 -853 0 +-855 -3 0 +-855 854 0 +855 3 -854 0 +-856 2 0 +-856 385 0 +856 -2 -385 0 +-857 -1 0 +-857 856 0 +857 1 -856 0 +-858 -3 0 +-858 857 0 +858 3 -857 0 +-859 -855 0 +-859 858 0 +859 855 -858 0 +-860 855 0 +-860 -858 0 +860 -855 858 0 +-861 -859 0 +-861 -860 0 +861 859 860 0 +-862 821 0 +-862 -861 0 +862 -821 861 0 +-863 -821 0 +-863 861 0 +863 821 -861 0 +-864 -862 0 +-864 -863 0 +864 862 863 0 +-865 781 0 +-865 864 0 +865 -781 -864 0 +-865 0 diff --git a/test/cnf/strash1.cnf b/test/cnf/strash1.cnf new file mode 100644 index 00000000..c2784ecd --- /dev/null +++ b/test/cnf/strash1.cnf @@ -0,0 +1,15 @@ +p cnf 7 14 +-1 2 0 +-1 3 0 +1 -2 -3 0 +-5 1 4 0 +-1 5 0 +-4 5 0 +-6 2 0 +-6 3 0 +6 -2 -3 0 +-7 1 4 0 +-1 7 0 +-4 7 0 +5 7 0 +-5 -7 0 diff --git a/test/cnf/strash2.cnf b/test/cnf/strash2.cnf new file mode 100644 index 00000000..41080993 --- /dev/null +++ b/test/cnf/strash2.cnf @@ -0,0 +1,21 @@ +p cnf 10 20 +-5 1 0 +-5 2 0 +5 -1 -2 0 +-6 5 0 +-6 3 0 +6 -5 -3 0 +-7 6 0 +-7 4 0 +7 -6 -4 0 +-8 1 0 +-8 2 0 +8 -1 -2 0 +-9 8 0 +-9 3 0 +9 -8 -3 0 +-10 9 0 +-10 4 0 +10 -9 -4 0 +7 10 0 +-7 -10 0 diff --git a/test/cnf/strash3.cnf b/test/cnf/strash3.cnf new file mode 100644 index 00000000..cedd10c6 --- /dev/null +++ b/test/cnf/strash3.cnf @@ -0,0 +1,9 @@ +c --substitute=0 +c --tumble=0 +p cnf 4 6 +-1 2 0 +-1 3 0 +-2 4 0 +-3 -4 0 +1 -2 -3 0 +2 3 4 0 diff --git a/test/testbump.c b/test/testbump.c index ea8274c7..fe7fefa7 100644 --- a/test/testbump.c +++ b/test/testbump.c @@ -24,7 +24,7 @@ test_bump_rescale (void) assert (solver->scinc > 0); tissat_verbose ("initial score increment %g", solver->scinc); ACTIVE (0) = ACTIVE (1) = true; - heap *scores = &solver->scores; + heap *scores = &solver->scores[0]; unsigned count = 0; for (unsigned i = 1; i <= 5; i++) { @@ -39,7 +39,7 @@ test_bump_rescale (void) if (count++ & 1) PUSH_STACK (solver->analyzed, 1); } - kissat_bump (solver); + kissat_bump_analyzed (solver); CLEAR_STACK (solver->analyzed); if (prev >= solver->scinc || solver->scinc >= MAX_SCORE * 0.7 || diff --git a/test/testcnfs.h b/test/testcnfs.h index 8a2d6bb2..570198a8 100644 --- a/test/testcnfs.h +++ b/test/testcnfs.h @@ -70,5 +70,7 @@ CNF (20, add32, false) \ CNF (20, add64, false) \ CNF (20, add128, false) \ + CNF (20, strash1, false) \ + CNF (20, strash2, false) \ #endif diff --git a/test/testconfig.c b/test/testconfig.c index b7b0937f..ca66f9bf 100644 --- a/test/testconfig.c +++ b/test/testconfig.c @@ -2,6 +2,15 @@ #include "../src/config.h" +// Manually copied from '../src/config.c'. + +#define CONFIGURATIONS \ + CONFIGURATION (basic) \ + CONFIGURATION (default) \ + CONFIGURATION (plain) \ + CONFIGURATION (sat) \ + CONFIGURATION (unsat) + #include "test.h" static void