1 /**************************************************************************** 2 Copyright (c) 2006 - 2015, Armin Biere, Johannes Kepler University. 3 4 Permission is hereby granted, free of charge, to any person obtaining a copy 5 of this software and associated documentation files (the "Software"), to 6 deal in the Software without restriction, including without limitation the 7 rights to use, copy, modify, merge, publish, distribute, sublicense, and/or 8 sell copies of the Software, and to permit persons to whom the Software is 9 furnished to do so, subject to the following conditions: 10 11 The above copyright notice and this permission notice shall be included in 12 all copies or substantial portions of the Software. 13 14 THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR 15 IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, 16 FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE 17 AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER 18 LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING 19 FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS 20 IN THE SOFTWARE. 21 ****************************************************************************/ 22 23 #ifdef __cplusplus 24 extern "C" { 25 #endif 26 27 #ifndef picosat_h_INCLUDED 28 #define picosat_h_INCLUDED 29 /*------------------------------------------------------------------------*/ 30 31 #include <stdlib.h> 32 #include <stdio.h> 33 #include <stddef.h> 34 35 /*------------------------------------------------------------------------*/ 36 /* The following macros allows for users to distiguish between different 37 * versions of the API. The first 'PICOSAT_REENTRANT_API' is defined for 38 * the new reentrant API which allows to generate multiple instances of 39 * PicoSAT in one process. The second 'PICOSAT_API_VERSION' defines the 40 * (smallest) version of PicoSAT to which this API conforms. 41 */ 42 #define PICOSAT_REENTRANT_API 43 #define PICOSAT_API_VERSION 953 /* API version */ 44 45 /*------------------------------------------------------------------------*/ 46 /* These are the return values for 'picosat_sat' as for instance 47 * standardized by the output format of the SAT competition. 48 */ 49 #define PICOSAT_UNKNOWN 0 50 #define PICOSAT_SATISFIABLE 10 51 #define PICOSAT_UNSATISFIABLE 20 52 53 /*------------------------------------------------------------------------*/ 54 struct PicoSAT; //forward declaration 55 typedef struct PicoSAT PicoSAT; 56 57 /*------------------------------------------------------------------------*/ 58 59 const char *picosat_version (void); 60 const char *picosat_config (void); 61 const char *picosat_copyright (void); 62 63 /*------------------------------------------------------------------------*/ 64 /* You can make PicoSAT use an external memory manager instead of the one 65 * provided by LIBC. But then you need to call these three function before 66 * 'picosat_init'. The memory manager functions here all have an additional 67 * first argument which is a pointer to the memory manager, but otherwise 68 * are supposed to work as their LIBC counter parts 'malloc', 'realloc' and 69 * 'free'. As exception the 'resize' and 'delete' function have as third 70 * argument the number of bytes of the block given as second argument. 71 */ 72 73 typedef void * (*picosat_malloc)(void *, size_t); 74 typedef void * (*picosat_realloc)(void*, void *, size_t, size_t); 75 typedef void (*picosat_free)(void*, void*, size_t); 76 77 /*------------------------------------------------------------------------*/ 78 79 PicoSAT * picosat_init (void); /* constructor */ 80 81 PicoSAT * picosat_minit (void * state, 82 picosat_malloc, 83 picosat_realloc, 84 picosat_free); 85 86 void picosat_reset (PicoSAT *); /* destructor */ 87 88 /*------------------------------------------------------------------------*/ 89 /* The following five functions are essentially parameters to 'init', and 90 * thus should be called right after 'picosat_init' before doing anything 91 * else. You should not call any of them after adding a literal. 92 */ 93 94 /* Set output file, default is 'stdout'. 95 */ 96 void picosat_set_output (PicoSAT *, FILE *); 97 98 /* Measure all time spent in all calls in the solver. By default only the 99 * time spent in 'picosat_sat' is measured. Enabling this function might 100 * for instance triple the time needed to add large CNFs, since every call 101 * to 'picosat_add' will trigger a call to 'getrusage'. 102 */ 103 void picosat_measure_all_calls (PicoSAT *); 104 105 /* Set the prefix used for printing verbose messages and statistics. 106 * Default is "c ". 107 */ 108 void picosat_set_prefix (PicoSAT *, const char *); 109 110 /* Set verbosity level. A verbosity level of 1 and above prints more and 111 * more detailed progress reports on the output file, set by 112 * 'picosat_set_output'. Verbose messages are prefixed with the string set 113 * by 'picosat_set_prefix'. 114 */ 115 void picosat_set_verbosity (PicoSAT *, int new_verbosity_level); 116 117 /* Disable/Enable all pre-processing, currently only failed literal probing. 118 * 119 * new_plain_value != 0 only 'plain' solving, so no preprocessing 120 * new_plain_value == 0 allow preprocessing 121 */ 122 void picosat_set_plain (PicoSAT *, int new_plain_value); 123 124 /* Set default initial phase: 125 * 126 * 0 = false 127 * 1 = true 128 * 2 = Jeroslow-Wang (default) 129 * 3 = random initial phase 130 * 131 * After a variable has been assigned the first time, it will always 132 * be assigned the previous value if it is picked as decision variable. 133 * The initial assignment can be chosen with this function. 134 */ 135 void picosat_set_global_default_phase (PicoSAT *, int); 136 137 /* Set next/initial phase of a particular variable if picked as decision 138 * variable. Second argument 'phase' has the following meaning: 139 * 140 * negative = next value if picked as decision variable is false 141 * 142 * positive = next value if picked as decision variable is true 143 * 144 * 0 = use global default phase as next value and 145 * assume 'lit' was never assigned 146 * 147 * Again if 'lit' is assigned afterwards through a forced assignment, 148 * then this forced assignment is the next phase if this variable is 149 * used as decision variable. 150 */ 151 void picosat_set_default_phase_lit (PicoSAT *, int lit, int phase); 152 153 /* You can reset all phases by the following function. 154 */ 155 void picosat_reset_phases (PicoSAT *); 156 157 /* Scores can be erased as well. Note, however, that even after erasing 158 * scores and phases, learned clauses are kept. In addition head tail 159 * pointers for literals are not moved either. So expect a difference 160 * between calling the solver in incremental mode or with a fresh copy of 161 * the CNF. 162 */ 163 void picosat_reset_scores (PicoSAT *); 164 165 /* Reset assignment if in SAT state and then remove the given percentage of 166 * less active (large) learned clauses. If you specify 100% all large 167 * learned clauses are removed. 168 */ 169 void picosat_remove_learned (PicoSAT *, unsigned percentage); 170 171 /* Set some variables to be more important than others. These variables are 172 * always used as decisions before other variables are used. Dually there 173 * is a set of variables that is used last. The default is 174 * to mark all variables as being indifferent only. 175 */ 176 void picosat_set_more_important_lit (PicoSAT *, int lit); 177 void picosat_set_less_important_lit (PicoSAT *, int lit); 178 179 /* Allows to print to internal 'out' file from client. 180 */ 181 void picosat_message (PicoSAT *, int verbosity_level, const char * fmt, ...); 182 183 /* Set a seed for the random number generator. The random number generator 184 * is currently just used for generating random decisions. In our 185 * experiments having random decisions did not really help on industrial 186 * examples, but was rather helpful to randomize the solver in order to 187 * do proper benchmarking of different internal parameter sets. 188 */ 189 void picosat_set_seed (PicoSAT *, unsigned random_number_generator_seed); 190 191 /* If you ever want to extract cores or proof traces with the current 192 * instance of PicoSAT initialized with 'picosat_init', then make sure to 193 * call 'picosat_enable_trace_generation' right after 'picosat_init'. This 194 * is not necessary if you only use 'picosat_set_incremental_rup_file'. 195 * 196 * NOTE, trace generation code is not necessarily included, e.g. if you 197 * configure PicoSAT with full optimzation as './configure.sh -O' or with 198 199 * you do not get any results by trying to generate traces. 200 * 201 * The return value is non-zero if code for generating traces is included 202 * and it is zero if traces can not be generated. 203 */ 204 int picosat_enable_trace_generation (PicoSAT *); 205 206 /* You can dump proof traces in RUP format incrementally even without 207 * keeping the proof trace in memory. The advantage is a reduction of 208 * memory usage, but the dumped clauses do not necessarily belong to the 209 * clausal core. Beside the file the additional parameters denotes the 210 * maximal number of variables and the number of original clauses. 211 */ 212 void picosat_set_incremental_rup_file (PicoSAT *, FILE * file, int m, int n); 213 214 /* Save original clauses for 'picosat_deref_partial'. See comments to that 215 * function further down. 216 */ 217 void picosat_save_original_clauses (PicoSAT *); 218 219 /* Add a call back which is checked regularly to notify the SAT solver 220 * to terminate earlier. This is useful for setting external time limits 221 * or terminate early in say a portfolio style parallel SAT solver. 222 */ 223 void picosat_set_interrupt (PicoSAT *, 224 void * external_state, 225 int (*interrupted)(void * external_state)); 226 227 /*------------------------------------------------------------------------*/ 228 /* This function returns the next available unused variable index and 229 * allocates a variable for it even though this variable does not occur as 230 * assumption, nor in a clause or any other constraints. In future calls to 231 * 'picosat_sat', 'picosat_deref' and particularly for 'picosat_changed', 232 * this variable is treated as if it had been used. 233 */ 234 int picosat_inc_max_var (PicoSAT *); 235 236 /*------------------------------------------------------------------------*/ 237 /* Push and pop semantics for PicoSAT. 'picosat_push' opens up a new 238 * context. All clauses added in this context are attached to it and 239 * discarded when the context is closed with 'picosat_pop'. It is also 240 * possible to nest contexts. 241 * 242 * The current implementation uses a new internal variable for each context. 243 * However, the indices for these internal variables are shared with 244 * ordinary external variables. This means that after any call to 245 * 'picosat_push', new variable indices should be obtained with 246 * 'picosat_inc_max_var' and not just by incrementing the largest variable 247 * index used so far. 248 * 249 * The return value is the index of the literal that assumes this context. 250 * This literal can only be used for 'picosat_failed_context' otherwise 251 * it will lead to an API usage error. 252 */ 253 int picosat_push (PicoSAT *); 254 255 /* This is as 'picosat_failed_assumption', but only for internal variables 256 * generated by 'picosat_push'. 257 */ 258 int picosat_failed_context (PicoSAT *, int lit); 259 260 /* Returns the literal that assumes the current context or zero if the 261 * outer context has been reached. 262 */ 263 int picosat_context (PicoSAT *); 264 265 /* Closes the current context and recycles the literal generated for 266 * assuming this context. The return value is the literal for the new 267 * outer context or zero if the outer most context has been reached. 268 */ 269 int picosat_pop (PicoSAT *); 270 271 /* Force immmediate removal of all satisfied clauses and clauses that are 272 * added or generated in closed contexts. This function is called 273 * internally if enough units are learned or after a certain number of 274 * contexts have been closed. This number is fixed at compile time 275 * and defined as MAXCILS in 'picosat.c'. 276 * 277 * Note that learned clauses which only involve outer contexts are kept. 278 */ 279 void picosat_simplify (PicoSAT *); 280 281 /*------------------------------------------------------------------------*/ 282 /* If you know a good estimate on how many variables you are going to use 283 * then calling this function before adding literals will result in less 284 * resizing of the variable table. But this is just a minor optimization. 285 * Beside exactly allocating enough variables it has the same effect as 286 * calling 'picosat_inc_max_var'. 287 */ 288 void picosat_adjust (PicoSAT *, int max_idx); 289 290 /*------------------------------------------------------------------------*/ 291 /* Statistics. 292 */ 293 int picosat_variables (PicoSAT *); /* p cnf <m> n */ 294 int picosat_added_original_clauses (PicoSAT *); /* p cnf m <n> */ 295 size_t picosat_max_bytes_allocated (PicoSAT *); 296 double picosat_time_stamp (void); /* ... in process */ 297 void picosat_stats (PicoSAT *); /* > output file */ 298 unsigned long long picosat_propagations (PicoSAT *); /* #propagations */ 299 unsigned long long picosat_decisions (PicoSAT *); /* #decisions */ 300 unsigned long long picosat_visits (PicoSAT *); /* #visits */ 301 302 /* The time spent in calls to the library or in 'picosat_sat' respectively. 303 * The former is returned if, right after initialization 304 * 'picosat_measure_all_calls' is called. 305 */ 306 double picosat_seconds (PicoSAT *); 307 308 /*------------------------------------------------------------------------*/ 309 /* Add a literal of the next clause. A zero terminates the clause. The 310 * solver is incremental. Adding a new literal will reset the previous 311 * assignment. The return value is the original clause index to which 312 * this literal respectively the trailing zero belong starting at 0. 313 */ 314 int picosat_add (PicoSAT *, int lit); 315 316 /* As the previous function, but allows to add a full clause at once with an 317 * at compiled time known size. The list of argument literals has to be 318 * terminated with a zero literal. Literals beyond the first zero literal 319 * are discarded. 320 */ 321 int picosat_add_arg (PicoSAT *, ...); 322 323 /* As the previous function but with an at compile time unknown size. 324 */ 325 int picosat_add_lits (PicoSAT *, int * lits); 326 327 /* Print the CNF to the given file in DIMACS format. 328 */ 329 void picosat_print (PicoSAT *, FILE *); 330 331 /* You can add arbitrary many assumptions before the next 'picosat_sat' 332 * call. This is similar to the using assumptions in MiniSAT, except that 333 * for PicoSAT you do not have to collect all your assumptions in a vector 334 * yourself. In PicoSAT you can add one after the other, to be used in the 335 * next call to 'picosat_sat'. 336 * 337 * These assumptions can be interpreted as adding unit clauses with those 338 * assumptions as literals. However these assumption clauses are only valid 339 * for exactly the next call to 'picosat_sat', and will be removed 340 * afterwards, e.g. in following future calls to 'picosat_sat' after the 341 * next 'picosat_sat' call, unless they are assumed again trough 342 * 'picosat_assume'. 343 * 344 * More precisely, assumptions actually remain valid even after the next 345 * call to 'picosat_sat' has returned. Valid means they remain 'assumed' 346 * internally until a call to 'picosat_add', 'picosat_assume', or a second 347 * 'picosat_sat', following the first 'picosat_sat'. The reason for keeping 348 * them valid is to allow 'picosat_failed_assumption' to return correct 349 * values. 350 * 351 * Example: 352 * 353 * picosat_assume (1); // assume unit clause '1 0' 354 * picosat_assume (-2); // additionally assume clause '-2 0' 355 * res = picosat_sat (1000); // assumes 1 and -2 to hold 356 * // 1000 decisions max. 357 * 358 * if (res == PICOSAT_UNSATISFIABLE) 359 * { 360 * if (picosat_failed_assumption (1)) 361 * // unit clause '1 0' was necessary to derive UNSAT 362 * 363 * if (picosat_failed_assumption (-2)) 364 * // unit clause '-2 0' was necessary to derive UNSAT 365 * 366 * // at least one but also both could be necessary 367 * 368 * picosat_assume (17); // previous assumptions are removed 369 * // now assume unit clause '17 0' for 370 * // the next call to 'picosat_sat' 371 * 372 * // adding a new clause, actually the first literal of 373 * // a clause would also make the assumptions used in the previous 374 * // call to 'picosat_sat' invalid. 375 * 376 * // The first two assumptions above are not assumed anymore. Only 377 * // the assumptions, since the last call to 'picosat_sat' returned 378 * // are assumed, e.g. the unit clause '17 0'. 379 * 380 * res = picosat_sat (-1); 381 * } 382 * else if (res == PICOSAT_SATISFIABLE) 383 * { 384 * // now the assignment is valid and we can call 'picosat_deref' 385 * 386 * assert (picosat_deref (1) == 1)); 387 * assert (picosat_deref (-2) == 1)); 388 * 389 * val = picosat_deref (15); 390 * 391 * // previous two assumptions are still valid 392 * 393 * // would become invalid if 'picosat_add' or 'picosat_assume' is 394 * // called here, but we immediately call 'picosat_sat'. Now when 395 * // entering 'picosat_sat' the solver knows that the previous call 396 * // returned SAT and it can safely reset the previous assumptions 397 * 398 * res = picosat_sat (-1); 399 * } 400 * else 401 * { 402 * assert (res == PICOSAT_UNKNOWN); 403 * 404 * // assumptions valid, but assignment invalid 405 * // except for top level assigned literals which 406 * // necessarily need to have this value if the formula is SAT 407 * 408 * // as above the solver nows that the previous call returned UNKWOWN 409 * // and will before doing anything else reset assumptions 410 * 411 * picosat_sat (-1); 412 * } 413 */ 414 void picosat_assume (PicoSAT *, int lit); 415 416 /*------------------------------------------------------------------------*/ 417 /* This is an experimental feature for handling 'all different constraints' 418 * (ADC). Currently only one global ADC can be handled. The bit-width of 419 * all the bit-vectors entered in this ADC (stored in 'all different 420 * objects' or ADOs) has to be identical. 421 * 422 * TODO: also handle top level assigned literals here. 423 */ 424 void picosat_add_ado_lit (PicoSAT *, int); 425 426 /*------------------------------------------------------------------------*/ 427 /* Call the main SAT routine. A negative decision limit sets no limit on 428 * the number of decisions. The return values are as above, e.g. 429 * 'PICOSAT_UNSATISFIABLE', 'PICOSAT_SATISFIABLE', or 'PICOSAT_UNKNOWN'. 430 */ 431 int picosat_sat (PicoSAT *, int decision_limit); 432 433 /* As alternative to a decision limit you can use the number of propagations 434 * as limit. This is more linearly related to execution time. This has to 435 * be called after 'picosat_init' and before 'picosat_sat'. 436 */ 437 void picosat_set_propagation_limit (PicoSAT *, unsigned long long limit); 438 439 /* Return last result of calling 'picosat_sat' or '0' if not called. 440 */ 441 int picosat_res (PicoSAT *); 442 443 /* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE', then 444 * the satisfying assignment can be obtained by 'dereferencing' literals. 445 * The value of the literal is return as '1' for 'true', '-1' for 'false' 446 * and '0' for an unknown value. 447 */ 448 int picosat_deref (PicoSAT *, int lit); 449 450 /* Same as before but just returns true resp. false if the literals is 451 * forced to this assignment at the top level. This function does not 452 * require that 'picosat_sat' was called and also does not internally reset 453 * incremental usage. 454 */ 455 int picosat_deref_toplevel (PicoSAT *, int lit); 456 457 /* After 'picosat_sat' was called and returned 'PICOSAT_SATISFIABLE' a 458 * partial satisfying assignment can be obtained as well. It satisfies all 459 * original clauses. The value of the literal is return as '1' for 'true', 460 * '-1' for 'false' and '0' for an unknown value. In order to make this 461 * work all original clauses have to be saved internally, which has to be 462 * enabled by 'picosat_save_original_clauses' right after initialization. 463 */ 464 int picosat_deref_partial (PicoSAT *, int lit); 465 466 /* Returns non zero if the CNF is unsatisfiable because an empty clause was 467 * added or derived. 468 */ 469 int picosat_inconsistent (PicoSAT *); 470 471 /* Returns non zero if the literal is a failed assumption, which is defined 472 * as an assumption used to derive unsatisfiability. This is as accurate as 473 * generating core literals, but still of course is an overapproximation of 474 * the set of assumptions really necessary. The technique does not need 475 * clausal core generation nor tracing to be enabled and thus can be much 476 * more effective. The function can only be called as long the current 477 * assumptions are valid. See 'picosat_assume' for more details. 478 */ 479 int picosat_failed_assumption (PicoSAT *, int lit); 480 481 /* Returns a zero terminated list of failed assumption in the last call to 482 * 'picosat_sat'. The pointer is valid until the next call to 483 * 'picosat_sat' or 'picosat_failed_assumptions'. It only makes sense if the 484 * last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'. 485 */ 486 const int * picosat_failed_assumptions (PicoSAT *); 487 488 /* Returns a zero terminated minimized list of failed assumption for the last 489 * call to 'picosat_sat'. The pointer is valid until the next call to this 490 * function or 'picosat_sat' or 'picosat_mus_assumptions'. It only makes sense 491 * if the last call to 'picosat_sat' returned 'PICOSAT_UNSATISFIABLE'. 492 * 493 * The call back function is called for all successful simplification 494 * attempts. The first argument of the call back function is the state 495 * given as first argument to 'picosat_mus_assumptions'. The second 496 * argument to the call back function is the new reduced list of failed 497 * assumptions. 498 * 499 * This function will call 'picosat_assume' and 'picosat_sat' internally but 500 * before returning reestablish a proper UNSAT state, e.g. 501 * 'picosat_failed_assumption' will work afterwards as expected. 502 * 503 * The last argument if non zero fixes assumptions. In particular, if an 504 * assumption can not be removed it is permanently assigned true, otherwise 505 * if it turns out to be redundant it is permanently assumed to be false. 506 */ 507 const int * picosat_mus_assumptions (PicoSAT *, void *, 508 void(*)(void*,const int*),int); 509 510 /* Compute one maximal subset of satisfiable assumptions. You need to set 511 * the assumptions, call 'picosat_sat' and check for 'picosat_inconsistent', 512 * before calling this function. The result is a zero terminated array of 513 * assumptions that consistently can be asserted at the same time. Before 514 * returing the library 'reassumes' all assumptions. 515 * 516 * It could be beneficial to set the default phase of assumptions 517 * to true (positive). This can speed up the computation. 518 */ 519 const int * picosat_maximal_satisfiable_subset_of_assumptions (PicoSAT *); 520 521 /* This function assumes that you have set up all assumptions with 522 * 'picosat_assume'. Then it calls 'picosat_sat' internally unless the 523 * formula is already inconsistent without assumptions, i.e. it contains 524 * the empty clause. After that it extracts a maximal satisfiable subset of 525 * assumptions. 526 * 527 * The result is a zero terminated maximal subset of consistent assumptions 528 * or a zero pointer if the formula contains the empty clause and thus no 529 * more maximal consistent subsets of assumptions can be extracted. In the 530 * first case, before returning, a blocking clause is added, that rules out 531 * the result for the next call. 532 * 533 * NOTE: adding the blocking clause changes the CNF. 534 * 535 * So the following idiom 536 * 537 * const int * mss; 538 * picosat_assume (a1); 539 * picosat_assume (a2); 540 * picosat_assume (a3); 541 * picosat_assume (a4); 542 * while ((mss = picosat_next_maximal_satisfiable_subset_of_assumptions ())) 543 * process_mss (mss); 544 * 545 * can be used to iterate over all maximal consistent subsets of 546 * the set of assumptions {a1,a2,a3,a4}. 547 * 548 * It could be beneficial to set the default phase of assumptions 549 * to true (positive). This might speed up the computation. 550 */ 551 const int * 552 picosat_next_maximal_satisfiable_subset_of_assumptions (PicoSAT *); 553 554 /* Similarly we can iterate over all minimal correcting assumption sets. 555 * See the CAMUS literature [M. Liffiton, K. Sakallah JAR 2008]. 556 * 557 * The result contains each assumed literal only once, even if it 558 * was assumed multiple times (in contrast to the maximal consistent 559 * subset functions above). 560 * 561 * It could be beneficial to set the default phase of assumptions 562 * to true (positive). This might speed up the computation. 563 */ 564 const int * 565 picosat_next_minimal_correcting_subset_of_assumptions (PicoSAT *); 566 567 /* Compute the union of all minmal correcting sets, which is called 568 * the 'high level union of all minimal unsatisfiable subset sets' 569 * or 'HUMUS' in our papers. 570 * 571 * It uses 'picosat_next_minimal_correcting_subset_of_assumptions' and 572 * the same notes and advices apply. In particular, this implies that 573 * after calling the function once, the current CNF becomes inconsistent, 574 * and PicoSAT has to be reset. So even this function internally uses 575 * PicoSAT incrementally, it can not be used incrementally itself at this 576 * point. 577 * 578 * The 'callback' can be used for progress logging and is called after 579 * each extracted minimal correcting set if non zero. The 'nhumus' 580 * parameter of 'callback' denotes the number of assumptions found to be 581 * part of the HUMUS sofar. 582 */ 583 const int * 584 picosat_humus (PicoSAT *, 585 void (*callback)(void * state, int nmcs, int nhumus), 586 void * state); 587 588 /*------------------------------------------------------------------------*/ 589 /* Assume that a previous call to 'picosat_sat' in incremental usage, 590 * returned 'SATISFIABLE'. Then a couple of clauses and optionally new 591 * variables were added (a new variable is a variable that has an index 592 * larger then the maximum variable added so far). The next call to 593 * 'picosat_sat' also returns 'SATISFIABLE'. If this function 594 * 'picosat_changed' returns '0', then the assignment to the old variables 595 * is guaranteed to not have changed. Otherwise it might have changed. 596 * 597 * The return value to this function is only valid until new clauses are 598 * added through 'picosat_add', an assumption is made through 599 * 'picosat_assume', or again 'picosat_sat' is called. This is the same 600 * assumption as for 'picosat_deref'. 601 * 602 * TODO currently this function might also return a non zero value even if 603 * the old assignment did not change, because it only checks whether the 604 * assignment of at least one old variable was flipped at least once during 605 * the search. In principle it should be possible to be exact in the other 606 * direction as well by using a counter of variables that have an odd number 607 * of flips. But this is not implemented yet. 608 */ 609 int picosat_changed (PicoSAT *); 610 611 /*------------------------------------------------------------------------*/ 612 /* The following six functions internally extract the variable and clausal 613 * core and thus require trace generation to be enabled with 614 * 'picosat_enable_trace_generation' right after calling 'picosat_init'. 615 * 616 * TODO: using these functions in incremental mode with failed assumptions 617 * has only been tested for 'picosat_corelit' thoroughly. The others 618 * probably only work in non-incremental mode or without using 619 * 'picosat_assume'. 620 */ 621 622 /* This function determines whether the i'th added original clause is in the 623 * core. The 'i' is the return value of 'picosat_add', which starts at zero 624 * and is incremented by one after a original clause is added (that is after 625 * 'picosat_add (0)'). For the index 'i' the following has to hold: 626 * 627 * 0 <= i < picosat_added_original_clauses () 628 */ 629 int picosat_coreclause (PicoSAT *, int i); 630 631 /* This function gives access to the variable core, which is made up of the 632 * variables that were resolved in deriving the empty clause. 633 */ 634 int picosat_corelit (PicoSAT *, int lit); 635 636 /* Write the clauses that were used in deriving the empty clause to a file 637 * in DIMACS format. 638 */ 639 void picosat_write_clausal_core (PicoSAT *, FILE * core_file); 640 641 /* Write a proof trace in TraceCheck format to a file. 642 */ 643 void picosat_write_compact_trace (PicoSAT *, FILE * trace_file); 644 void picosat_write_extended_trace (PicoSAT *, FILE * trace_file); 645 646 /* Write a RUP trace to a file. This trace file contains only the learned 647 * core clauses while this is not necessarily the case for the RUP file 648 * obtained with 'picosat_set_incremental_rup_file'. 649 */ 650 void picosat_write_rup_trace (PicoSAT *, FILE * trace_file); 651 652 /*------------------------------------------------------------------------*/ 653 /* Keeping the proof trace around is not necessary if an over-approximation 654 * of the core is enough. A literal is 'used' if it was involved in a 655 * resolution to derive a learned clause. The core literals are necessarily 656 * a subset of the 'used' literals. 657 */ 658 659 int picosat_usedlit (PicoSAT *, int lit); 660 /*------------------------------------------------------------------------*/ 661 #endif 662 663 #ifdef __cplusplus 664 } 665 #endif 666