1 //===--- satoko.h -----------------------------------------------------------=== 2 // 3 // satoko: Satisfiability solver 4 // 5 // This file is distributed under the BSD 2-Clause License. 6 // See LICENSE for details. 7 // 8 //===------------------------------------------------------------------------=== 9 #ifndef satoko__satoko_h 10 #define satoko__satoko_h 11 12 #include "types.h" 13 #include "misc/util/abc_global.h" 14 ABC_NAMESPACE_HEADER_START 15 16 /** Return valeus */ 17 enum { 18 SATOKO_ERR = 0, 19 SATOKO_OK = 1 20 }; 21 22 enum { 23 SATOKO_UNDEC = 0, /* Undecided */ 24 SATOKO_SAT = 1, 25 SATOKO_UNSAT = -1 26 }; 27 28 enum { 29 SATOKO_LIT_FALSE = 1, 30 SATOKO_LIT_TRUE = 0, 31 SATOKO_VAR_UNASSING = 3 32 }; 33 34 struct solver_t_; 35 typedef struct solver_t_ satoko_t; 36 37 typedef struct satoko_opts satoko_opts_t; 38 struct satoko_opts { 39 /* Limits */ 40 long conf_limit; /* Limit on the n.of conflicts */ 41 long prop_limit; /* Limit on the n.of propagations */ 42 43 /* Constants used for restart heuristic */ 44 double f_rst; /* Used to force a restart */ 45 double b_rst; /* Used to block a restart */ 46 unsigned fst_block_rst; /* Lower bound n.of conflicts for start blocking restarts */ 47 unsigned sz_lbd_bqueue; /* Size of the moving avarege queue for LBD (force restart) */ 48 unsigned sz_trail_bqueue; /* Size of the moving avarege queue for Trail size (block restart) */ 49 50 /* Constants used for clause database reduction heuristic */ 51 unsigned n_conf_fst_reduce; /* N.of conflicts before first clause databese reduction */ 52 unsigned inc_reduce; /* Increment to reduce */ 53 unsigned inc_special_reduce; /* Special increment to reduce */ 54 unsigned lbd_freeze_clause; 55 float learnt_ratio; /* Percentage of learned clauses to remove */ 56 57 /* VSIDS heuristic */ 58 double var_decay; 59 float clause_decay; 60 unsigned var_act_rescale; 61 act_t var_act_limit; 62 63 64 /* Binary resolution */ 65 unsigned clause_max_sz_bin_resol; 66 unsigned clause_min_lbd_bin_resol; 67 float garbage_max_ratio; 68 char verbose; 69 char no_simplify; 70 }; 71 72 typedef struct satoko_stats satoko_stats_t; 73 struct satoko_stats { 74 unsigned n_starts; 75 unsigned n_reduce_db; 76 77 long n_decisions; 78 long n_propagations; 79 long n_propagations_all; 80 long n_inspects; 81 long n_conflicts; 82 long n_conflicts_all; 83 84 long n_original_lits; 85 long n_learnt_lits; 86 }; 87 88 89 //===------------------------------------------------------------------------=== 90 extern satoko_t *satoko_create(void); 91 extern void satoko_destroy(satoko_t *); 92 extern void satoko_reset(satoko_t *); 93 94 extern void satoko_default_opts(satoko_opts_t *); 95 extern void satoko_configure(satoko_t *, satoko_opts_t *); 96 extern int satoko_parse_dimacs(char *, satoko_t **); 97 extern void satoko_setnvars(satoko_t *, int); 98 extern int satoko_add_variable(satoko_t *, char); 99 extern int satoko_add_clause(satoko_t *, int *, int); 100 extern void satoko_assump_push(satoko_t *s, int); 101 extern void satoko_assump_pop(satoko_t *s); 102 extern int satoko_simplify(satoko_t *); 103 extern int satoko_solve(satoko_t *); 104 extern int satoko_solve_assumptions(satoko_t *s, int * plits, int nlits); 105 extern int satoko_solve_assumptions_limit(satoko_t *s, int * plits, int nlits, int nconflim); 106 extern int satoko_minimize_assumptions(satoko_t *s, int * plits, int nlits, int nconflim); 107 extern void satoko_mark_cone(satoko_t *, int *, int); 108 extern void satoko_unmark_cone(satoko_t *, int *, int); 109 110 extern void satoko_rollback(satoko_t *); 111 extern void satoko_bookmark(satoko_t *); 112 extern void satoko_unbookmark(satoko_t *); 113 /* If problem is unsatisfiable under assumptions, this function is used to 114 * obtain the final conflict clause expressed in the assumptions. 115 * - It receives as inputs the solver and a pointer to an array where clause 116 * is stored. The memory for the clause is managed by the solver. 117 * - The return value is either the size of the array or -1 in case the final 118 * conflict cluase was not generated. 119 */ 120 extern int satoko_final_conflict(satoko_t *, int **); 121 122 /* Procedure to dump a DIMACS file. 123 * - It receives as input the solver, a file name string and two integers. 124 * - If the file name string is NULL the solver will dump in stdout. 125 * - The first argument can be either 0 or 1 and is an option to dump learnt 126 * clauses. (value 1 will dump them). 127 * - The seccond argument can be either 0 or 1 and is an option to use 0 as a 128 * variable ID or not. Keep in mind that if 0 is used as an ID the generated 129 * file will not be a DIMACS. (value 1 will use 0 as ID). 130 */ 131 extern void satoko_write_dimacs(satoko_t *, char *, int, int); 132 extern satoko_stats_t * satoko_stats(satoko_t *); 133 extern satoko_opts_t * satoko_options(satoko_t *); 134 135 extern int satoko_varnum(satoko_t *); 136 extern int satoko_clausenum(satoko_t *); 137 extern int satoko_learntnum(satoko_t *); 138 extern int satoko_conflictnum(satoko_t *); 139 extern void satoko_set_stop(satoko_t *, int *); 140 extern void satoko_set_stop_func(satoko_t *s, int (*fnct)(int)); 141 extern void satoko_set_runid(satoko_t *, int); 142 extern int satoko_read_cex_varvalue(satoko_t *, int); 143 extern abctime satoko_set_runtime_limit(satoko_t *, abctime); 144 extern char satoko_var_polarity(satoko_t *, unsigned); 145 146 147 ABC_NAMESPACE_HEADER_END 148 #endif /* satoko__satoko_h */ 149