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