From 9a09689dfab27059332092bf329db0c4abc258b2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 22 Sep 2018 19:19:05 -0700 Subject: [PATCH] add documentation on the cuber Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 11 ++++++++++- src/sat/sat_lookahead.cpp | 2 ++ src/sat/sat_params.pyg | 28 +++++++++++++++++++++++++--- 3 files changed, 37 insertions(+), 4 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index b9e15d329..a6b05904c 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6605,7 +6605,12 @@ class Solver(Z3PPObject): _handle_parse_error(e, self.ctx) def cube(self, vars = None): - """Get set of cubes""" + """Get set of cubes + The method takes an optional set of variables that restrict which + variables may be used as a starting point for cubing. + If vars is not None, then the first case split is based on a variable in + this set. + """ self.cube_vs = AstVector(None, self.ctx) if vars is not None: for v in vars: @@ -6621,6 +6626,10 @@ class Solver(Z3PPObject): return def cube_vars(self): + """Access the set of variables that were touched by the most recently generated cube. + This set of variables can be used as a starting point for additional cubes. + The idea is that variables that appear in clauses that are reduced by the most recent + cube are likely more useful to cube on.""" return self.cube_vs def proof(self): diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 3833e2a52..4ca2c5f84 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -16,6 +16,8 @@ Author: Notes: + + --*/ #include diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg index 89776c479..113a8133e 100644 --- a/src/sat/sat_params.pyg +++ b/src/sat/sat_params.pyg @@ -50,17 +50,39 @@ def_module_params('sat', ('unit_walk', BOOL, False, 'use unit-walk search instead of CDCL'), ('unit_walk_threads', UINT, 0, 'number of unit-walk search threads to find satisfiable solution'), ('lookahead.cube.cutoff', SYMBOL, 'depth', 'cutoff type used to create lookahead cubes: depth, freevars, psat, adaptive_freevars, adaptive_psat'), + # - depth: the maximal cutoff is fixed to the value of lookahead.cube.depth. + # So if the value is 10, at most 1024 cubes will be generated of length 10. + # - freevars: cutoff based on a variable fraction of lookahead.cube.freevars. + # Cut if the number of current unassigned variables drops below a fraction of number of initial variables. + # - psat: Let psat_heur := (Sum_{clause C} (psat.clause_base ^ {-|C|+1})) / |freevars|^psat.var_exp + # Cut if the value of psat_heur exceeds psat.trigger + # - adaptive_freevars: Cut if the number of current unassigned variables drops below a fraction of free variables + # at the time of the last conflict. The fraction is increased every time the a cutoff is created. + # - adative_psat: Cut based on psat_heur in an adaptive way. ('lookahead.cube.fraction', DOUBLE, 0.4, 'adaptive fraction to create lookahead cubes. Used when lookahead.cube.cutoff is adaptive_freevars or adaptive_psat'), ('lookahead.cube.depth', UINT, 1, 'cut-off depth to create cubes. Used when lookahead.cube.cutoff is depth.'), - ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free fariable fraction. Used when lookahead.cube.cutoff is freevars'), + ('lookahead.cube.freevars', DOUBLE, 0.8, 'cube free variable fraction. Used when lookahead.cube.cutoff is freevars'), ('lookahead.cube.psat.var_exp', DOUBLE, 1, 'free variable exponent for PSAT cutoff'), ('lookahead.cube.psat.clause_base', DOUBLE, 2, 'clause base for PSAT cutoff'), ('lookahead.cube.psat.trigger', DOUBLE, 5, 'trigger value to create lookahead cubes for PSAT cutoff. Used when lookahead.cube.cutoff is psat'), - ('lookahead_search', BOOL, False, 'use lookahead solver'), ('lookahead.preselect', BOOL, False, 'use pre-selection of subset of variables for branching'), ('lookahead_simplify', BOOL, False, 'use lookahead solver during simplification'), ('lookahead.use_learned', BOOL, False, 'use learned clauses when selecting lookahead literal'), ('lookahead_simplify.bca', BOOL, True, 'add learned binary clauses as part of lookahead simplification'), ('lookahead.global_autarky', BOOL, False, 'prefer to branch on variables that occur in clauses that are reduced'), - ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu'))) + ('lookahead.reward', SYMBOL, 'march_cu', 'select lookahead heuristic: ternary, heule_schur (Heule Schur), heuleu (Heule Unit), unit, or march_cu')) + # reward function used to determine which literal to cube on. + # - ternary: reward function useful for random 3-SAT instances. Used by Heule and Knuth in March. + # - heule_schur: reward function based on "Schur Number 5", Heule, AAAI 2018 + # The score of a literal lit is: + # Sum_{C in Clauses | lit in C} 2 ^ (- |C|+1) + # * Sum_{lit' in C | lit' != lit} lit_occs(~lit') + # / | C | + # where lit_occs(lit) is the number of clauses containing lit. + # - heuleu: The score of a literal lit is: Sum_{C in Clauses | lit in C} 2 ^ (-|C| + 1) + # - unit: heule_schur + also counts number of unit clauses. + # - march_cu: default reward function used in a version of March + # Each reward function also comes with its own variant of "mix_diff", which + # is the function for combining reward metrics for the positive and negative variant of a literal. + )