1module ibalpqsat; % Quantified SAT solving 2 3revision('ibalpqsat, "$Id: ibalpqsat.red 3961 2017-03-19 08:24:03Z thomas-sturm $"); 4 5copyright('ibalpqsat, "(c) 2007-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm"); 6 7% Redistribution and use in source and binary forms, with or without 8% modification, are permitted provided that the following conditions 9% are met: 10% 11% * Redistributions of source code must retain the relevant 12% copyright notice, this list of conditions and the following 13% disclaimer. 14% * Redistributions in binary form must reproduce the above 15% copyright notice, this list of conditions and the following 16% disclaimer in the documentation and/or other materials provided 17% with the distribution. 18% 19% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS 20% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT 21% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR 22% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT 23% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, 24% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT 25% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, 26% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY 27% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT 28% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE 29% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. 30% 31 32fluid '(ibalp_qsatoptions!* !*rlverbose); 33 34fluid '(donel!*, numcdcl!*, numlocs!*); 35 36procedure my_mkvect(n); 37 << 38 ioto_tprin2t {"entering mkvect n=",n}; 39 for i := 0:n collect (i . nil) 40 >>; 41 42procedure my_putv(v,n,a); 43 begin scalar w; 44 ioto_tprin2t {"entering putv n=",n," size=",length v}; 45 w := assoc(n,v); 46 cdr w := a; 47 return v 48 end; 49 50procedure my_getv(v,n); 51 << 52 ioto_tprin2t {"entering getv n=",n," size=",length v}; 53 cdr assoc(n,v) 54 >>; 55 56procedure my_mkvect(n); 57 << 58 ioto_tprin2t {"entering mkvect n=",n}; 59 mkvect n 60 >>; 61 62procedure my_putv(v,n,a); 63 begin scalar w; 64 ioto_tprin2t {"entering putv n=",n," size=",upbv v}; 65 putv(v,n,a); 66 ioto_tprin2t {"leaving putv n=",n," size=",upbv v}; 67 end; 68 69procedure my_getv(v,n); 70 << 71 ioto_tprin2t {"entering getv n=",n," size=",upbv v}; 72 getv(v,n) 73 >>; 74 75procedure ibalp_qsat!-initoptions(); 76 % Initialise the options. Sets default values for all options. 77 ibalp_qsat!-setoptionl({'zmom,5,1,1.2,200}); 78 79procedure ibalp_qsat!-getoptionl(); 80 % Get the option list. Returns the list with the options of the SAT 81 % solver. 82 begin scalar tlist; 83 tlist := lto_catsoc('clause_del,ibalp_qsatoptions!*) . nil; 84 tlist := lto_catsoc('res_inc,ibalp_qsatoptions!*) . tlist; 85 tlist := lto_catsoc('first_val,ibalp_qsatoptions!*) . tlist; 86 tlist := lto_catsoc('res_start,ibalp_qsatoptions!*) . tlist; 87 tlist := lto_catsoc('heuristic,ibalp_qsatoptions!*) . tlist; 88 return tlist 89 end; 90 91procedure ibalp_qsat!-setoptionl(optionl); 92 % Set options. [optionl] is a list of options. It must be [nil] or 93 % have five elements, indicating the branching heuristc, the 94 % restart value, the first value to be set, the increase factor for 95 % restarts, the bound for clause deletion. Returns the new list of 96 % options. 97 begin scalar temp; 98 if null optionl then 99 return ibalp_qsat!-getoptionl(); 100 temp := car optionl; 101 ibalp_qsatoptions!* := ('heuristic . temp) . nil; 102 temp := cadr optionl; 103 ibalp_qsatoptions!* := ('res_start . temp) . ibalp_qsatoptions!*; 104 temp := caddr optionl; 105 ibalp_qsatoptions!* := ('first_val . temp) . ibalp_qsatoptions!*; 106 temp := cadddr optionl; 107 ibalp_qsatoptions!* := ('res_inc . temp) . ibalp_qsatoptions!*; 108 temp := car cddddr optionl; 109 ibalp_qsatoptions!* := ('clause_del . temp) . ibalp_qsatoptions!*; 110 return ibalp_qsat!-getoptionl(); 111 end; 112 113procedure ibalp_qsat!-getoption(opt); 114 % Get option. [opt] is one of the options heuristic, res_start, 115 % first_val, res_inc or clause_del. Returns the corresponding 116 % option. 117 lto_catsoc(opt,ibalp_qsatoptions!*); 118 119#if t 120 121inline procedure ibalp_var!-new(id); 122 % Create a new variable. [id] is the identifier of the 123 % variable. Returns a list with the following components: l[0] is 124 % the identifier; l[1] is the value of the variable; l[2] is the 125 % list of positive occurences of the variable; l[3] is the list of 126 % negative occurences; l[4] is the number of currently false 127 % clauses where the variable has a positive occurence; l[5] is the 128 % number of currently false clauses where the variable has a 129 % negative occurence; l[6] is the level at which the variable was 130 % set; l[7] is the reason for the variable; l[8] is the number of 131 % positive occurences in new added conflict-clauses; l[9] is the 132 % number of positive occurences in new added conflict-clauses; 133 % l[10] is the list of watched clauses; l[11] is the f-Calc; 134 % l[12] is the quantifier of this variable; l[13] is the 135 % quantification level of the variable; l[14] is the flipped-flag. 136 {id,nil,nil,nil,0,0,-1,nil,0,0,nil,0,nil,0,nil}; 137 138inline procedure ibalp_var!-setval(var,val); 139 % Set the value of a variable. [var] is a variable; [val] is the 140 % value [0], [1] or [nil]; 141 cadr var := val; 142 143inline procedure ibalp_var!-setposocc(var,posocc); 144 % Add a clause to the list of clauses where the variable has a 145 % positive occurence. [var] is a variable; [negocc] the clause. 146 caddr var := posocc . caddr var; 147 148inline procedure ibalp_var!-setnegocc(var,negocc); 149 % Add a clause to the list of clauses where the variable has a 150 % negative occurence. [var] is a variable; [negocc] the clause. 151 cadddr var := negocc . cadddr var; 152 153inline procedure ibalp_var!-setposoccabs(var,posocc); 154 % Add a clause to the list of clauses where the variable has a 155 % positive occurence. [var] is a variable; [negocc] the clause. 156 caddr var := posocc; 157 158inline procedure ibalp_var!-setnegoccabs(var,negocc); 159 % Add a clause to the list of clauses where the variable has a 160 % negative occurence. [var] is a variable; [negocc] the clause. 161 cadddr var := negocc; 162 163inline procedure ibalp_var!-setnumpos(var,numpos); 164 % Get the number of currently false clauses where the variable has 165 % a positive occurence and is not set. [var] is a variable; 166 % [numpos] the number of occurences. 167 car cddddr var := numpos; 168 169inline procedure ibalp_var!-setnumneg(var,numneg); 170 % Set the number of currently false clauses where the variable has 171 % a negative occurence and is not set. [var] is a variable; 172 % [numneg] the number of occurences. 173 cadr cddddr var := numneg; 174 175inline procedure ibalp_var!-setlev(var,lev); 176 % Set the level at which the variable was set. [var] is a variable; 177 % [lev] is the number of the level; 178 caddr cddddr var := lev; 179 180inline procedure ibalp_var!-setreas(var,reas); 181 % Set the reason why the variable was set. [var] is a variable; 182 % [reas] is the clause which became unit and forced the set or nil 183 % if it was a decision. 184 cadddr cddddr var := reas; 185 186inline procedure ibalp_var!-setposcc(var,num); 187 % Set the number of positive occurences in added 188 % conflict-clauses. [var] is a variable; [num] is the number of 189 % occurences. 190 car cddddr cddddr var := num; 191 192inline procedure ibalp_var!-setnegcc(var,num); 193 % Set the number of negative occurences in added 194 % conflict-clauses. [var] is a variable; [num] is the number of 195 % occurences. 196 cadr cddddr cddddr var := num; 197 198inline procedure ibalp_var!-setwc(var,wc); 199 % Set the watched-clauses of a variable . [var] is a variable; [wc] 200 % is a watched clause. 201 caddr cddddr cddddr var := wc . caddr cddddr cddddr var; 202 203inline procedure ibalp_var!-setmom(var,mom); 204 % Set the MOM-value for this variable. [var] is a variable; [mom] 205 % is the MOM-value. 206 cadddr cddddr cddddr var := mom; 207 208inline procedure ibalp_var!-setquant(var,quant); 209 % Set the quantifier for this variable. [var] is a variable; 210 % [quant] is [nil] if it is an unquantified variable, [ex] for an 211 % existential quantified variable and [all] for an universal 212 % quantified variable. 213 car cddddr cddddr cddddr var := quant; 214 215inline procedure ibalp_var!-setqlevel(var,qlevel); 216 % Set the quantifier-level for this variable. [var] is a variable; 217 % [qlevel] the quantifier level. 218 cadr cddddr cddddr cddddr var := qlevel; 219 220inline procedure ibalp_var!-setflip(var,flip); 221 % Set the flip-level for this variable. [var] is a variable; 222 % [flip] is the flipstatus. 223 caddr cddddr cddddr cddddr var := flip; 224 225inline procedure ibalp_var!-getid(var); 226 % Get the identifier of a variable. [var] is variable. Returns the 227 % identifier. 228 car var; 229 230inline procedure ibalp_var!-getval(var); 231 % Get the current value of a variable. [var] is a variable. Returns 232 % [1] if the variable is set to true, [0] if set to false and [nil] 233 % if the variable is not set. 234 cadr var; 235 236inline procedure ibalp_var!-getposocc(var); 237 % Get the list of all clauses where the variable has a positive 238 % occurence. [var] is a variable. Returns the list of clauses. 239 caddr var; 240 241inline procedure ibalp_var!-getnegocc(var); 242 % Get the list of all clauses where the variable has a negative 243 % occurence. [var] is a variable. Returns the list of clauses. 244 cadddr var; 245 246inline procedure ibalp_var!-getnumpos(var); 247 % Get the number of currently false clauses where the variable has 248 % a positive occurence and is not set. [var] is a variable. Returns 249 % the number of clauses. 250 car cddddr var; 251 252inline procedure ibalp_var!-getnumneg(var); 253 % Get the number of currently false clauses where the variable has 254 % a negative occurence and is not set. [var] is a variable. Returns 255 % the number of clauses. 256 cadr cddddr var; 257 258inline procedure ibalp_var!-getlev(var); 259 % Get the level at which the variable was set. [var] is a 260 % variable. Returns the level. 261 caddr cddddr var; 262 263inline procedure ibalp_var!-getreas(var); 264 % Get the reason why the variable was set. [var] is a variable. 265 % Returns the clause which became unit and forced the set or [nil] 266 % if a decision was the reason. 267 cadddr cddddr var; 268 269inline procedure ibalp_var!-getposcc(var); 270 % Get the number of positive occurences in added 271 % conflict-clauses. [var] is a variable. Returns the number of 272 % positive occurences in conflict-clauses. 273 car cddddr cddddr var; 274 275inline procedure ibalp_var!-getnegcc(var); 276 % Get the number of negative occurences in added 277 % conflict-clauses. [var] is a variable. Returns the number of 278 % negative occurences in conflict-clauses. 279 cadr cddddr cddddr var; 280 281inline procedure ibalp_var!-getwc(var); 282 % Get the watched-clauses of a variable . [var] is a variable. 283 caddr cddddr cddddr var; 284 285inline procedure ibalp_var!-delwc(var,wc); 286 % Delete a single watched-clauses of this variable . [var] is a 287 % variable; [wc] is a clause. 288 caddr cddddr cddddr var := lto_delq(wc,caddr cddddr cddddr var); 289 290inline procedure ibalp_var!-delallwc(var); 291 % Delete all watched-clauses of this variable . [var] is a 292 % variable. 293 caddr cddddr cddddr var := nil; 294 295inline procedure ibalp_var!-getmom(var); 296 % Get the MOM-value for this variable. [var] is a variable. 297 cadddr cddddr cddddr var; 298 299inline procedure ibalp_var!-getquant(var); 300 % Get the quantifier for this variable. [var] is a variable; 301 % Return [nil] if it is an unquantified variable, [ex] for an 302 % existential quantified variable and [all] for an universal 303 % quantified variable. 304 car cddddr cddddr cddddr var; 305 306inline procedure ibalp_var!-isex(var); 307 % Returns if a variable is existential quantified. [var] is a 308 % variable. Returns [t] iff the var is existential quantified. 309 car cddddr cddddr cddddr var eq 'ex; 310 311inline procedure ibalp_var!-isuni(var); 312 % Returns if a variable is universal quantified. [var] is a 313 % variable. Returns [t] iff the var is universal quantified. 314 car cddddr cddddr cddddr var eq 'all; 315 316inline procedure ibalp_var!-getqlevel(var); 317 % Get the quantifier-level for this variable. [var] is a variable; 318 % Returns the quantifier level. 319 cadr cddddr cddddr cddddr var; 320 321inline procedure ibalp_var!-getflip(var); 322 % Get the flipstatus for this variable. [var] is a variable; 323 % Returns [nil] if the variable is no decision variable, 0 if the 324 % variable i unflipped and 1 if flipped. 325 caddr cddddr cddddr cddddr var; 326 327inline procedure ibalp_clause!-new(); 328 % Create a new clause. Returns a list with the following 329 % components: l[0] is a list of the positive literals of the 330 % clause; l[1] is a list of the negative literals of the clause; 331 % l[2] is the number of currently unset positive variables in the 332 % clause; l[3] is the number of currently unset negative variables 333 % in the clause; l[4] is the variable turning this clause to true 334 % or [nil] if the clause is false; l[5] is a counter for new-added 335 % clauses. 336 {nil,nil,0,0,nil,nil,nil}; 337 338inline procedure ibalp_clause!-setsat(clause,sat); 339 % Set the variable turning a clause to true. [clause] is a clause; 340 % [sat] is the variable turning to true 341 car cddddr clause := sat . car cddddr clause; 342 343inline procedure ibalp_clause!-delallsat(clause); 344 % Set the variable turning a clause to true. [clause] is a clause; 345 % [sat] is the variable turning to true 346 car cddddr clause := nil; 347 348inline procedure ibalp_clause!-setposlit(clause,var); 349 % Add a variable to the list of positive literals of a 350 % clause. [clause] is a clause; [var] is a variable. 351 car clause := var . car clause; 352 353inline procedure ibalp_clause!-setneglit(clause,var); 354 % Add a variable to the list of negative literals of a 355 % clause. [clause] is a clause; [var] is a variable. 356 cadr clause := var . cadr clause; 357 358inline procedure ibalp_clause!-setposlitabs(clause,var); 359 % Add a variable to the list of positive literals of a 360 % clause. [clause] is a clause; [var] is a variable. 361 car clause := var; 362 363inline procedure ibalp_clause!-setneglitabs(clause,var); 364 % Add a variable to the list of negative literals of a 365 % clause. [clause] is a clause; [var] is a variable. 366 cadr clause := var; 367 368inline procedure ibalp_clause!-setactpos(clause,actpos); 369 % Set the number of positive literals that are currently 370 % unset. [clause] is a clause; [actpos] is the number of currently 371 % unset literals. 372 caddr clause := actpos; 373 374inline procedure ibalp_clause!-setactneg(clause,actneg); 375 % Set the number of negative literals that are currently 376 % unset. [clause] is a clause; [actneg] is the number of currently 377 % unset literals. 378 cadddr clause := actneg; 379 380inline procedure ibalp_clause!-setcount(clause,count); 381 % Set the current count for new-added clauses. [clause] is a 382 % clause; [count] is the count. 383 cadr cddddr clause := count; 384 385inline procedure ibalp_clause!-setwl(clause,wl); 386 % Add a watched literal for this clause. [clause] is a 387 % clause; [wl] is a variable. 388 caddr cddddr clause := wl . caddr cddddr clause; 389 390inline procedure ibalp_clause!-delallwl(clause); 391 % Delete the watched literals for this clause. [clause] is a 392 % clause. 393 caddr cddddr clause := nil; 394 395inline procedure ibalp_clause!-delwl(clause,wl); 396 % Delete a single watched literal from this clause. [clause] is a 397 % clause; [wl] is a variable. 398 caddr cddddr clause := lto_delq(wl,caddr cddddr clause); 399 400inline procedure ibalp_clause!-getposlit(clause); 401 % Get a list of all positive literals of a clause. [clause] is a 402 % clause. Returns the list of variables. [nil] if the clause has no 403 % positive literals. 404 car clause; 405 406inline procedure ibalp_clause!-getneglit(clause); 407 % Get a list of all negative literals of a clause. [clause] is a 408 % clause. Returns the list of variables. [nil] if the clause has no 409 % negative literals. 410 cadr clause; 411 412inline procedure ibalp_clause!-getactpos(clause); 413 % Get the number of positive literals that are currently unset in a 414 % clause. [clause] is a clause. Returns the number of literals 415 caddr clause; 416 417inline procedure ibalp_clause!-getactneg(clause); 418 % Get the number of negative literals that are currently unset in a 419 % clause. [clause] is a clause. Returns the number of literals. 420 cadddr clause; 421 422inline procedure ibalp_clause!-getsat(clause); 423 % Get the variable turning a clause to true. [clause] is a 424 % clause. Returns the variable or [nil] if the clause is false. 425 car cddddr clause; 426 427inline procedure ibalp_clause!-delsat(clause,sat); 428 % Delete a variable turning a clause to true. [clause] is a clause; 429 % [sat] is a variable. 430 car cddddr clause := lto_delq(sat,car cddddr clause); 431 432inline procedure ibalp_clause!-getcount(clause); 433 % Get the current count for new-added clauses. [clause] is a 434 % clause. Return the count. 435 cadr cddddr clause; 436 437inline procedure ibalp_clause!-getwl(clause); 438 % Get the watched literals for this clause. [clause] is a 439 % clause. Return the watched literal. 440 caddr cddddr clause; 441 442#else 443 444inline procedure ibalp_var!-new(id); 445 % Create a new variable. [id] is the identifier of the 446 % variable. Returns a list with the following components: l[0] is 447 % the identifier; l[1] is the value of the variable; l[2] is the 448 % list of positive occurences of the variable; l[3] is the list of 449 % negative occurences; l[4] is the number of currently false 450 % clauses where the variable has a positive occurence; l[5] is the 451 % number of currently false clauses where the variable has a 452 % negative occurence; l[6] is the level at which the variable was 453 % set; l[7] is the reason for the variable; l[8] is the number of 454 % positive occurences in new added conflict-clauses; l[9] is the 455 % number of positive occurences in new added conflict-clauses; 456 % l[10] is the list of watched clauses; l[11] is the MOM-Calc; 457 % l[12] is the quantifier of this variable; l[13] is the 458 % quantification level of the variable; l[14] is the flipped-flag. 459 begin scalar v; 460 v := mkvect(14); 461 putv(v,0,id); 462 putv(v,4,0); 463 putv(v,5,0); 464 putv(v,6,-1); 465 putv(v,8,0); 466 putv(v,9,0); 467 putv(v,11,0); 468 putv(v,13,0); 469 return v 470 end; 471 472inline procedure ibalp_var!-setval(var,val); 473 % Set the value of a variable. [var] is a variable; [val] is the 474 % value [0], [1] or [nil]; 475 putv(var,1,val); 476 477inline procedure ibalp_var!-setposocc(var,posocc); 478 % Add a clause to the list of clauses where the variable has a 479 % positive occurence. [var] is a variable; [negocc] the clause. 480 putv(var,2,posocc . getv(var,2)); 481 482inline procedure ibalp_var!-setnegocc(var,negocc); 483 % Add a clause to the list of clauses where the variable has a 484 % negative occurence. [var] is a variable; [negocc] the clause. 485 putv(var,3,negocc . getv(var,3)); 486 487inline procedure ibalp_var!-setposoccabs(var,posocc); 488 % Add a clause to the list of clauses where the variable has a 489 % positive occurence. [var] is a variable; [negocc] the clause. 490 putv(var,2,posocc); 491 492inline procedure ibalp_var!-setnegoccabs(var,negocc); 493 % Add a clause to the list of clauses where the variable has a 494 % negative occurence. [var] is a variable; [negocc] the clause. 495 putv(var,3,negocc); 496 497inline procedure ibalp_var!-setnumpos(var,numpos); 498 % Get the number of currently false clauses where the variable has 499 % a positive occurence and is not set. [var] is a variable; 500 % [numpos] the number of occurences. 501 putv(var,4,numpos); 502 503inline procedure ibalp_var!-setnumneg(var,numneg); 504 % Set the number of currently false clauses where the variable has 505 % a negative occurence and is not set. [var] is a variable; 506 % [numneg] the number of occurences. 507 putv(var,5,numneg); 508 509inline procedure ibalp_var!-setlev(var,lev); 510 % Set the level at which the variable was set. [var] is a variable; 511 % [lev] is the number of the level; 512 putv(var,6,lev); 513 514inline procedure ibalp_var!-setreas(var,reas); 515 % Set the reason why the variable was set. [var] is a variable; 516 % [reas] is the clause which became unit and forced the set or nil 517 % if it was a decision. 518 putv(var,7,reas); 519 520inline procedure ibalp_var!-setposcc(var,num); 521 % Set the number of positive occurences in added 522 % conflict-clauses. [var] is a variable; [num] is the number of 523 % occurences. 524 putv(var,8,num); 525 526inline procedure ibalp_var!-setnegcc(var,num); 527 % Set the number of negative occurences in added 528 % conflict-clauses. [var] is a variable; [num] is the number of 529 % occurences. 530 putv(var,9,num); 531 532inline procedure ibalp_var!-setwc(var,wc); 533 % Set the watched-clauses of a variable . [var] is a variable; [wc] 534 % is a watched clause. 535 putv(var,10,wc . getv(var,10)); 536 537inline procedure ibalp_var!-setmom(var,mom); 538 % Set the MOM-value for this variable. [var] is a variable; [mom] 539 % is the MOM-value. 540 putv(var,11,mom); 541 542inline procedure ibalp_var!-setquant(var,quant); 543 % Set the quantifier for this variable. [var] is a variable; 544 % [quant] is [nil] if it is an unquantified variable, [ex] for an 545 % existential quantified variable and [all] for an universal 546 % quantified variable. 547 putv(var,12,quant); 548 549inline procedure ibalp_var!-setqlevel(var,qlevel); 550 % Set the quantifier-level for this variable. [var] is a variable; 551 % [qlevel] the quantifier level. 552 putv(var,13,qlevel); 553 554inline procedure ibalp_var!-setflip(var,flip); 555 % Set the flip-level for this variable. [var] is a variable; 556 % [flip] is the flipstatus. 557 putv(var,14,flip); 558 559inline procedure ibalp_var!-getid(var); 560 % Get the identifier of a variable. [var] is variable. Returns the 561 % identifier. 562 getv(var,0); 563 564inline procedure ibalp_var!-getval(var); 565 % Get the current value of a variable. [var] is a variable. Returns 566 % [1] if the variable is set to true, [0] if set to false and [nil] 567 % if the variable is not set. 568 getv(var,1); 569 570inline procedure ibalp_var!-getposocc(var); 571 % Get the list of all clauses where the variable has a positive 572 % occurence. [var] is a variable. Returns the list of clauses. 573 getv(var,2); 574 575inline procedure ibalp_var!-getnegocc(var); 576 % Get the list of all clauses where the variable has a negative 577 % occurence. [var] is a variable. Returns the list of clauses. 578 getv(var,3); 579 580inline procedure ibalp_var!-getnumpos(var); 581 % Get the number of currently false clauses where the variable has 582 % a positive occurence and is not set. [var] is a variable. Returns 583 % the number of clauses. 584 getv(var,4); 585 586inline procedure ibalp_var!-getnumneg(var); 587 % Get the number of currently false clauses where the variable has 588 % a negative occurence and is not set. [var] is a variable. Returns 589 % the number of clauses. 590 getv(var,5); 591 592inline procedure ibalp_var!-getlev(var); 593 % Get the level at which the variable was set. [var] is a 594 % variable. Returns the level. 595 getv(var,6); 596 597inline procedure ibalp_var!-getreas(var); 598 % Get the reason why the variable was set. [var] is a variable. 599 % Returns the clause which became unit and forced the set or [nil] 600 % if a decision was the reason. 601 getv(var,7); 602 603inline procedure ibalp_var!-getposcc(var); 604 % Get the number of positive occurences in added 605 % conflict-clauses. [var] is a variable. Returns the number of 606 % positive occurences in conflict-clauses. 607 getv(var,8); 608 609inline procedure ibalp_var!-getnegcc(var); 610 % Get the number of negative occurences in added 611 % conflict-clauses. [var] is a variable. Returns the number of 612 % negative occurences in conflict-clauses. 613 getv(var,9); 614 615inline procedure ibalp_var!-getwc(var); 616 % Get the watched-clauses of a variable . [var] is a variable. 617 getv(var,10); 618 619inline procedure ibalp_var!-delwc(var,wc); 620 % Delete a single watched-clauses of this variable . [var] is a 621 % variable; [wc] is a clause. 622 putv(var,10,lto_delq(wc,getv(var,10))); 623 624inline procedure ibalp_var!-delallwc(var); 625 % Delete all watched-clauses of this variable . [var] is a 626 % variable. 627 putv(var,10,nil); 628 629inline procedure ibalp_var!-getmom(var); 630 % Get the MOM-value for this variable. [var] is a variable. 631 getv(var,11); 632 633inline procedure ibalp_var!-getquant(var); 634 % Get the quantifier for this variable. [var] is a variable; 635 % Return [nil] if it is an unquantified variable, [ex] for an 636 % existential quantified variable and [all] for an universal 637 % quantified variable. 638 getv(var,12); 639 640inline procedure ibalp_var!-isex(var); 641 % Returns if a variable is existential quantified. [var] is a 642 % variable. Returns [t] iff the var is existential quantified. 643 getv(var,12) eq 'ex; 644 645inline procedure ibalp_var!-isuni(var); 646 % Returns if a variable is universal quantified. [var] is a 647 % variable. Returns [t] iff the var is universal quantified. 648 getv(var,12) eq 'all; 649 650inline procedure ibalp_var!-getqlevel(var); 651 % Get the quantifier-level for this variable. [var] is a variable; 652 % Returns the quantifier level. 653 getv(var,13); 654 655inline procedure ibalp_var!-getflip(var); 656 % Get the flipstatus for this variable. [var] is a variable; 657 % Returns [nil] if the variable is no decision variable, 0 if the 658 % variable i unflipped and 1 if flipped. 659 getv(var,14); 660 661inline procedure ibalp_clause!-new(); 662 % Create a new clause. Returns a list with the following 663 % components: l[0] is a list of the positive literals of the 664 % clause; l[1] is a list of the negative literals of the clause; 665 % l[2] is the number of currently unset positive variables in the 666 % clause; l[3] is the number of currently unset negative variables 667 % in the clause; l[4] is the variable turning this clause to true 668 % or [nil] if the clause is false; l[5] is a counter for new-added 669 % clauses. 670 begin scalar v; 671 v := mkvect(6); 672 putv(v,2,0); 673 putv(v,3,0); 674 return v 675 end; 676 677inline procedure ibalp_clause!-setsat(clause,sat); 678 % Set the variable turning a clause to true. [clause] is a clause; 679 % [sat] is the variable turning to true 680 putv(clause,4,sat . getv(clause,4)); 681 682inline procedure ibalp_clause!-delallsat(clause); 683 % Set the variable turning a clause to true. [clause] is a clause; 684 % [sat] is the variable turning to true 685 putv(clause,4,nil); 686 687inline procedure ibalp_clause!-setposlit(clause,var); 688 % Add a variable to the list of positive literals of a 689 % clause. [clause] is a clause; [var] is a variable. 690 putv(clause,0,var . getv(clause,0)); 691 692inline procedure ibalp_clause!-setneglit(clause,var); 693 % Add a variable to the list of negative literals of a 694 % clause. [clause] is a clause; [var] is a variable. 695 putv(clause,1,var . getv(clause,1)); 696 697inline procedure ibalp_clause!-setposlitabs(clause,var); 698 % Add a variable to the list of positive literals of a 699 % clause. [clause] is a clause; [var] is a variable. 700 putv(clause,0,var); 701 702inline procedure ibalp_clause!-setneglitabs(clause,var); 703 % Add a variable to the list of negative literals of a 704 % clause. [clause] is a clause; [var] is a variable. 705 putv(clause,1,var); 706 707inline procedure ibalp_clause!-setactpos(clause,actpos); 708 % Set the number of positive literals that are currently 709 % unset. [clause] is a clause; [actpos] is the number of currently 710 % unset literals. 711 putv(clause,2,actpos); 712 713inline procedure ibalp_clause!-setactneg(clause,actneg); 714 % Set the number of negative literals that are currently 715 % unset. [clause] is a clause; [actneg] is the number of currently 716 % unset literals. 717 putv(clause,3,actneg); 718 719inline procedure ibalp_clause!-setcount(clause,count); 720 % Set the current count for new-added clauses. [clause] is a 721 % clause; [count] is the count. 722 putv(clause,5,count); 723 724inline procedure ibalp_clause!-setwl(clause,wl); 725 % Add a watched literal for this clause. [clause] is a 726 % clause; [wl] is a variable. 727 putv(clause,6,wl . getv(clause,6)); 728 729inline procedure ibalp_clause!-delallwl(clause); 730 % Delete the watched literals for this clause. [clause] is a 731 % clause. 732 putv(clause,6,nil); 733 734inline procedure ibalp_clause!-delwl(clause,wl); 735 % Delete a single watched literal from this clause. [clause] is a 736 % clause; [wl] is a variable. 737 putv(clause,6,lto_delq(wl,getv(clause,6))); 738 739inline procedure ibalp_clause!-getposlit(clause); 740 % Get a list of all positive literals of a clause. [clause] is a 741 % clause. Returns the list of variables. [nil] if the clause has no 742 % positive literals. 743 getv(clause,0); 744 745inline procedure ibalp_clause!-getneglit(clause); 746 % Get a list of all negative literals of a clause. [clause] is a 747 % clause. Returns the list of variables. [nil] if the clause has no 748 % negative literals. 749 getv(clause,1); 750 751inline procedure ibalp_clause!-getactpos(clause); 752 % Get the number of positive literals that are currently unset in a 753 % clause. [clause] is a clause. Returns the number of literals 754 getv(clause,2); 755 756inline procedure ibalp_clause!-getactneg(clause); 757 % Get the number of negative literals that are currently unset in a 758 % clause. [clause] is a clause. Returns the number of literals. 759 getv(clause,3); 760 761inline procedure ibalp_clause!-getsat(clause); 762 % Get the variable turning a clause to true. [clause] is a 763 % clause. Returns the variable or [nil] if the clause is false. 764 getv(clause,4); 765 766inline procedure ibalp_clause!-delsat(clause,sat); 767 % Delete a variable turning a clause to true. [clause] is a clause; 768 % [sat] is a variable. 769 putv(clause,4,lto_delq(sat,getv(clause,4))); 770 771inline procedure ibalp_clause!-getcount(clause); 772 % Get the current count for new-added clauses. [clause] is a 773 % clause. Return the count. 774 getv(clause,5); 775 776inline procedure ibalp_clause!-getwl(clause); 777 % Get the watched literals for this clause. [clause] is a 778 % clause. Return the watched literal. 779 getv(clause,6); 780 781#endif 782 783procedure ibalp_printclause(clause); 784 % Helper function to print a clause. 785 begin scalar poslit,neglit,sat; 786 for each v in ibalp_clause!-getposlit clause do 787 poslit := ibalp_var!-getid v . poslit; 788 for each v in ibalp_clause!-getneglit clause do 789 neglit := ibalp_var!-getid v . neglit; 790 for each v in ibalp_clause!-getsat clause do 791 sat := v . sat; 792 ioto_tprin2t {"Clause ",poslit," ",neglit," ","SAT: ",sat} 793 end; 794 795procedure ibalp_printclauses(clausel); 796 % Helper function to print all clauses. 797 for each c in clausel do 798 ibalp_printclause c; 799 800procedure ibalp_printvaral(varal); 801 % Helper function to print the list of variables. 802 for each v in varal do 803 ioto_tprin2t {ibalp_var!-getid cdr v, " ", ibalp_var!-getval cdr v, " ", ibalp_var!-getquant cdr v}; 804 805procedure ibalp_qsat!-dimacs(input); 806 % The main entry point for solving a given .cnf or .qdimacs 807 % file. [input] is the filename. Returns [true] or [false]. 808 begin scalar pair,clausel,varal; 809 if null ibalp_qsatoptions!* then ibalp_qsat!-initoptions(); 810 pair := ibalp_qsat!-readdimacs2(input); 811 clausel := cadr pair; 812 varal := cddr pair; 813 return if car pair then 814 car ibalp_qsat!-cdcl(clausel,varal,nil,t) 815 else 816 ibalp_start!-sat(clausel,varal) 817 end; 818 819procedure ibalp_qsat!-readdimacs(input); 820 % Read a .cnf or .qdimacs file and conert it to Lisp 821 % Prefix. [input] is the filename. Returns the corresponding 822 % formula in Lisp Prefix. 823 begin scalar pair,clausel,varal; 824 pair := ibalp_qsat!-readdimacs2(input); 825 clausel := cadr pair; 826 varal := cddr pair; 827 return ibalp_convcnf(clausel,varal,car pair) 828 end; 829 830procedure ibalp_qsat(f); 831 % The main entry point for the QSAT function. [f] is a formula in 832 % lisp prefix. Returns true or false in SAT and Q-SAT or a formula 833 % in DNF in PQ-SAT. 834 begin scalar pair,clausel,varal,readform,qsat,pqsat; 835 if null ibalp_qsatoptions!* then ibalp_qsat!-initoptions(); 836 qsat := cl_bvarl f; 837 pqsat := cl_fvarl f; 838 readform := if qsat then cl_matrix (cl_pnf f) else f; 839 if not (ibalp_iscnf readform) then << 840 %readform := ibalp_get3cnf(readform); 841 if !*rlverbose then 842 ioto_tprin2t "Formula was not in CNF. Using QE"; 843 return cl_qe(f,nil) 844 >>; 845 pair := ibalp_readform readform; 846 clausel := car pair; 847 varal := cdr pair; 848 if null clausel then 849 return 'true; 850 if ibalp_emptyclausep car clausel then 851 return 'false; 852 if qsat and null pqsat then 853 return ibalp_start!-qsat(clausel,varal,f) 854 else if qsat and pqsat then 855 return ibalp_start!-pqsat(clausel,varal,f,pqsat) 856 else 857 return ibalp_start!-sat(clausel,varal) 858 end; 859 860procedure ibalp_start!-sat(clausel,varal); 861 % Start SAT solving. [clausel] is the list of clauses; [varal] is 862 % the A-List of variables. Returns [true] if there is a satisfying 863 % assignment, [nil] else. 864 begin scalar resstart,firstval,inc,heur; 865 if !*rlverbose then 866 ioto_tprin2t {"Starting SAT Algorithm"}; 867 for each v in varal do 868 ibalp_var!-setmom(cdr v,ibalp_calcmom cdr v); 869 resstart := ibalp_qsat!-getoption('res_start); 870 firstval := ibalp_qsat!-getoption('first_val); 871 inc := ibalp_qsat!-getoption('res_inc); 872 heur := ibalp_qsat!-getoption('heuristic); 873 return ibalp_cdcl(clausel,varal,resstart,firstval,1,inc,heur) 874 end; 875 876procedure ibalp_start!-qsat(clausel,varal,f); 877 % Start Q-SAT solving. [clausel] is the list of clauses, [varal] 878 % is the A-List of variables; [f] is the original 879 % formula. Returns [true] if the formula is true, [nil] else. 880 begin scalar varal,pair; 881 if !*rlverbose then 882 ioto_tprin2t {"Starting QSAT Algorithm"}; 883 pair := ibalp_readquantal(cl_pnf f,varal); 884 varal := cdr pair; 885 if eqn(car pair,1) and ibalp_var!-isex cdar varal then 886 return ibalp_start!-sat(clausel,varal) 887 else 888 return car ibalp_qsat!-cdcl(clausel,varal,nil,t) 889 end; 890 891procedure ibalp_start!-pqsat(clausel,varal,f,pqsat); 892 % Start parametric Q-SAT solving. [clausel] is the list of 893 % clauses; [varal] is the A-List of variables; [f] is the 894 % original formula; [pqsat] is the list of free 895 % variables. Returns a condition to the free variables in DNF or 896 % true or false. 897 begin scalar pair,psat; 898 if !*rlverbose then 899 ioto_tprin2t {"Starting PQSAT Algorithm with ", length pqsat, " free variables..."}; 900 pair := ibalp_readquantal(cl_pnf f,varal); 901 varal := cdr pair; 902 pair := ibalp_splitvars(pqsat,varal); 903 varal := car pair; 904 pqsat := cdr pair; 905 psat := ibalp_psatp varal; 906 if !*rlverbose and psat then 907 ioto_tprin2t {"**PSAT Problem"}; 908 donel!* := nil; 909 numcdcl!* := 0; 910 numlocs!* := 0; 911 %if length pqsat / length varal > 2/3 then 912 if nil then 913 return cl_qe(f,nil) 914 else << 915 varal := cdr ibalp_readquantal(cl_pnf f,varal); 916 pair := ibalp_qsat!-par(pqsat,clausel,varal,nil,psat); 917 if !*rlverbose then << 918 ioto_tprin2t {"Runs of CDCL: ", numcdcl!*}; 919 ioto_tprin2t {"Local Search Successes: ", numlocs!*}; 920 >>; 921 return ibalp_exres2(car pair,pqsat) 922 >> 923 end; 924 925procedure ibalp_cdcl(clausel,varal,c,setval,rescount,inc,heur); 926 % Conflict Driven Clause Learning Procedure. [clausel] is the list 927 % of clauses; [varal] is the A-List of variables; [c] is the number 928 % of conflict clauses for a restart; [setval] is the value a chosen 929 % variable should be set to; [rescount] is a counter for restarts; 930 % [inc] is the increase factor for restarts; [heur] is the used 931 % heuristic. Returns [true] if there is a satisfying assignment, 932 % [false] else. 933 begin scalar res,fin,pair,ec,lv,upl; integer level,count; 934 pair := ibalp_preprocess(clausel,varal); 935 clausel := car pair; 936 varal := cdr pair; 937 if null clausel then return {'true}; 938 upl := ibalp_initwl clausel; 939 while null fin do << 940 ec := ibalp_cec clausel; 941 if null ec then << 942 upl := ibalp_getupl clausel; 943 pair := ibalp_unitprop(upl,clausel,level); 944 ec := car pair; 945 lv := cdr pair; 946 >>; 947 if ec then << 948 if eqn(level,0) then << 949 fin := t; 950 res := {'false} 951 >> else << 952 ibalp_recalcv varal; 953 count := count + 1; 954 ibalp_dimcount clausel; 955 pair := ibalp_analconf(ec,level,lv,clausel,varal); 956 level := car pair; 957 clausel := cdr pair; 958 pair := ibalp_dosimpl(clausel,varal); 959 clausel := car pair; 960 varal := cdr pair 961 >> 962 >> else << 963 if ibalp_istotal varal or ibalp_csat clausel then << 964 fin := t; 965 res := {'true} 966 >> else << 967 pair := ibalp_getvar(varal,clausel,heur); 968 level := level + 1; 969 if heur = 'activity then setval := cdr pair; 970 ibalp_var!-set(car pair,setval,level,nil); 971 if count > c then << 972 res := ibalp_restart(clausel,varal,c, 973 rescount,setval,inc,heur); 974 fin := t 975 >> 976 >> 977 >> 978 >>; 979 return res 980 end; 981 982procedure ibalp_preprocess(clausel,varal); 983 % Pre-processing of the formula. [clausel] is the list of clauses; 984 % [varal] is the A-List of variables. Retruns a pair of the new 985 % clauses and the new variables. 986 begin scalar pair; integer count; 987 for each v in varal do << 988 if eqn(ibalp_var!-getnumpos cdr v,0) then << 989 count := count + 1; 990 pair := ibalp_simplify(cdr v,0,nil,clausel,varal); 991 clausel := car pair; 992 varal := cdr pair 993 >> else if eqn(ibalp_var!-getnumneg cdr v,0) then << 994 count := count + 1; 995 pair := ibalp_simplify(cdr v,1,nil,clausel,varal); 996 clausel := car pair; 997 varal := cdr pair 998 >> 999 >>; 1000 if !*rlverbose then 1001 ioto_tprin2t {"deleted variables in pre-processing ",count}; 1002 return (clausel . varal) 1003 end; 1004 1005procedure ibalp_getvar(varal,clausel,heur); 1006 % Get a variable corresponding to a branching heuristic. [clausel] 1007 % is the list of clauses; [varal] is the A-List of variables; 1008 % [heur] is the branching heuristic. Returns a pair of variable and 1009 % value it should be assigned to. 1010 if heur = 'zmom then 1011 ibalp_getvar!-zmom(varal,clausel) 1012 else if heur = 'activity then 1013 ibalp_getmacvext varal 1014 else ibalp_getvar!-dlcs varal; 1015 1016procedure ibalp_restart(clausel,varal,c,rescount,setval,inc,heur); 1017 % Restart the CDCL algorithm. [clausel] is the list of clauses; 1018 % [varal] is the A-List of variables; [c] is the number of conflict 1019 % clauses for a restart; [setval] is the value a chosen variable 1020 % should be set to; [rescount] is a counter for restarts; [inc] is 1021 % the increase factor for restarts; [heur] is the used 1022 % heuristic. Returns [true] if there is a satisfying assignment for 1023 % the formula, [nil] else. 1024 << 1025 if !*rlverbose then 1026 ioto_tprin2t {"restart ",rescount}; 1027 ibalp_dav(varal,clausel); 1028 if c > ibalp_qsat!-getoption('clause_del) then 1029 clausel := ibalp_killcount clausel; 1030 ibalp_cdcl(clausel,varal,c*inc,1-setval,rescount+1,inc,heur) 1031 >>; 1032 1033procedure ibalp_analconf(ec,level,lv,clausel,varal); 1034 % Analyse conflict. [ec] is the empty clause; [level] is the 1035 % current level; [lv] is the last assigned variable; [clausel] is 1036 % the list of clauses; [varal] is the A-List of variables. Returns 1037 % a pair of the new level and the new list of clauses. 1038 begin scalar pair,newlev,cc,p,val; 1039 cc := ibalp_calccc!-fuip(ec,level,lv); 1040 pair := ibalp_calccvar(cc,level); 1041 p := car pair; 1042 newlev := cdr pair; 1043 val := ibalp_var!-getval p; 1044 clausel := cc . clausel; 1045 ibalp_tvb(varal,newlev); 1046 ibalp_renewwl clausel; 1047 ibalp_var!-set(p,1-val,newlev,nil); 1048 return (newlev . clausel) 1049 end; 1050 1051procedure ibalp_dosimpl(clausel,varal); 1052 % Perform Simplifications. [clausel] is the list of clauses; 1053 % [varal] is the A-List of variables. Return a pair of the new 1054 % clauses and the new variables. 1055 begin scalar h,pair; 1056 while h := ibalp_hassimple clausel do << 1057 pair := ibalp_simplify(nil,nil,h,clausel,varal); 1058 clausel := car pair; 1059 varal := cdr pair 1060 >>; 1061 return (clausel . varal) 1062 end; 1063 1064procedure ibalp_simplify(dvar,dval,clause,clausel,varal); 1065 % Simplification. Delete needles literals. [dvar] is a variable; 1066 % [dval] its value; [clause] is a clause; [clausel] is the list of 1067 % clauses; [varal] is the A-List of variables. Returns a pair of 1068 % the new clauses and the new variables. 1069 begin scalar var,val; 1070 if null dvar then << 1071 if ibalp_lenisone ibalp_clause!-getposlit clause then << 1072 var := car ibalp_clause!-getposlit clause; 1073 val := 1 1074 >> 1075 else << 1076 var := car ibalp_clause!-getneglit clause; 1077 val := 0 1078 >>; 1079 if ibalp_var!-getval var then 1080 ibalp_var!-unset(var,ibalp_var!-getval var); 1081 ibalp_var!-set(var,val,0,nil); 1082 >> else << 1083 var := dvar; 1084 val := dval 1085 >>; 1086 if eqn(val,1) then << 1087 for each clause in ibalp_var!-getposocc var do 1088 clausel := ibalp_delclause(clause,clausel); 1089 for each clause in ibalp_var!-getnegocc var do 1090 ibalp_dellit(var,clause,nil); 1091 >> else << 1092 for each clause in ibalp_var!-getnegocc var do 1093 clausel := ibalp_delclause(clause,clausel); 1094 for each clause in ibalp_var!-getposocc var do 1095 ibalp_dellit(var,clause,t); 1096 >>; 1097 varal := lto_delq(atsoc(ibalp_var!-getid var,varal),varal); 1098 return (clausel . varal) 1099 end; 1100 1101procedure ibalp_lenisone(l); 1102 l and null cdr l; 1103 1104procedure ibalp_commonlenisone(l1,l2); 1105 % l1 and l2 are lists, which are not both empty. 1106 null l1 and ibalp_lenisone l2 or null l2 and ibalp_lenisone l1; 1107 1108procedure ibalp_hassimple(clausel); 1109 % Check if a clause list has some literals to simplify. [clausel] 1110 % is the list of clauses. Returns a clause to simplfy or [nil]. 1111 begin scalar ret,tl; 1112 tl := clausel; 1113 while tl and null ret do << 1114 if ibalp_commonlenisone( 1115 ibalp_clause!-getposlit car tl,ibalp_clause!-getneglit car tl) 1116 then 1117 ret := car tl; 1118 tl := cdr tl 1119 >>; 1120 return ret 1121 end; 1122 1123procedure ibalp_getupl(clausel); 1124 % Get initial set for Unit Propagation. [clausel] is the list of 1125 % clauses. Returns a list of unit clauses. 1126 begin scalar upl; 1127 for each c in clausel do 1128 if null ibalp_clause!-getsat c and 1129 eqn(ibalp_clause!-getactpos c + ibalp_clause!-getactneg c,1) then 1130 upl := c . upl; 1131 return upl 1132 end; 1133 1134procedure ibalp_unitprop(clist,clausel,level); 1135 % Unitpropagation. [clist] is a list of clauses with unit 1136 % variables; [clausel] ist the list of clauses; [level] is the 1137 % level the reduction is made; [setvar] is the last variable 1138 % set. Returns a Pair. The first entry is an empty clause if one is 1139 % derived the second the variable set at last. 1140 begin scalar tl,clause,actpos,actneg,var,ec,upl,w; 1141 w := tl := clist; 1142 while tl and null ec do << 1143 clause := car tl; 1144 if null ibalp_clause!-getsat clause then << 1145 actpos := ibalp_clause!-getactpos clause; 1146 actneg := ibalp_clause!-getactneg clause; 1147 % Since clause is unit, we know that actpos is 1 and 1148 % actneg is 0 or vice versa. 1149 if actpos #= 1 then << 1150 var := car ibalp_clause!-getwl clause; 1151 if null ibalp_var!-getval var then << 1152 upl := ibalp_var!-set(var,1,level,clause); 1153 nconc(w,upl); 1154 w := upl or w 1155 >> 1156 >> else << 1157 var := car ibalp_clause!-getwl clause; 1158 if null ibalp_var!-getval var then << 1159 upl := ibalp_var!-set(var,0,level,clause); 1160 nconc(w,upl); 1161 w := upl or w 1162 >> 1163 >> 1164 >>; 1165 tl := cdr tl; 1166 ec := ibalp_cec clausel 1167 >>; 1168 return (ec . var) 1169 end; 1170 1171procedure ibalp_initwl(clausel); 1172 % Initialize the watched literals. [clausel] is the list of 1173 % clauses. Returns a list of unit clauses. 1174 begin scalar count,upl,tl; 1175 for each c in clausel do << 1176 count := 0; 1177 tl := ibalp_clause!-getposlit c; 1178 while not eqn(count,2) and tl do << 1179 ibalp_clause!-setwl(c,car tl); 1180 ibalp_var!-setwc(car tl,c); 1181 count := count + 1; 1182 tl := cdr tl 1183 >>; 1184 tl := ibalp_clause!-getneglit c; 1185 while not eqn(count,2) and tl do << 1186 ibalp_clause!-setwl(c,car tl); 1187 ibalp_var!-setwc(car tl,c); 1188 count := count + 1; 1189 tl := cdr tl 1190 >>; 1191 if count < 2 then upl := c . upl 1192 >>; 1193 return upl 1194 end; 1195 1196procedure ibalp_renewwl(clausel); 1197 % Renew watched literals. [clausel] is the list of clauses; 1198 begin scalar wl; 1199 for each c in clausel do << 1200 if null ibalp_clause!-getsat c then << 1201 if eqn(length ibalp_clause!-getwl c,1) and 1202 length ibalp_clause!-getposlit c + 1203 length ibalp_clause!-getneglit c > 1 then << 1204 wl := ibalp_getnewwl c; 1205 if wl then << 1206 ibalp_clause!-setwl(c,wl); 1207 ibalp_var!-setwc(wl,c) 1208 >>; 1209 >> else 1210 if null ibalp_clause!-getwl c and 1211 length ibalp_clause!-getposlit c + 1212 length ibalp_clause!-getneglit c > 1 then << 1213 wl := ibalp_getnewwl c; 1214 if wl then << 1215 ibalp_clause!-setwl(c,wl); 1216 ibalp_var!-setwc(wl,c) 1217 >>; 1218 wl := ibalp_getnewwl c; 1219 if wl then << 1220 ibalp_clause!-setwl(c,wl); 1221 ibalp_var!-setwc(wl,c) 1222 >> 1223 >> 1224 >> 1225 >> 1226 end; 1227 1228procedure ibalp_resolve(newclause,clause1,clause2,cv); 1229 % Resolve two clauses to one. [newclause] is the new clause; 1230 % [clause1] is the first clause to resolve; [clause2] is the second 1231 % clause to resolve; [cv] is the conflict variable within the two 1232 % clauses. 1233 << 1234 for each v in ibalp_clause!-getposlit clause1 do 1235 if null (v eq cv) and 1236 null memq(v,ibalp_clause!-getposlit newclause) then << 1237 ibalp_clause!-setposlit(newclause,v); 1238 ibalp_var!-setposocc(v,newclause); 1239 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v + 1) 1240 >>; 1241 for each v in ibalp_clause!-getposlit clause2 do 1242 if null (v eq cv) and 1243 null memq(v,ibalp_clause!-getposlit newclause) then << 1244 ibalp_clause!-setposlit(newclause,v); 1245 ibalp_var!-setposocc(v,newclause); 1246 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v + 1) 1247 >>; 1248 for each v in ibalp_clause!-getneglit clause1 do 1249 if null (v eq cv) and 1250 null memq(v,ibalp_clause!-getneglit newclause) then << 1251 ibalp_clause!-setneglit(newclause,v); 1252 ibalp_var!-setnegocc(v,newclause); 1253 ibalp_var!-setnumneg(v,ibalp_var!-getnumneg v + 1) 1254 >>; 1255 for each v in ibalp_clause!-getneglit clause2 do 1256 if null (v eq cv) and 1257 null memq(v,ibalp_clause!-getneglit newclause) then << 1258 ibalp_clause!-setneglit(newclause,v); 1259 ibalp_var!-setnegocc(v,newclause); 1260 ibalp_var!-setnumneg(v,ibalp_var!-getnumneg v + 1) 1261 >>; 1262 >>; 1263 1264procedure ibalp_dav(varal,clausel); 1265 % Delete all assignments to variables. [varal] is the A-List of 1266 % variables; [clausel] is the list of clauses. 1267 << 1268 for each v in varal do << 1269 if ibalp_var!-getval cdr v then << 1270 ibalp_var!-unset(cdr v,ibalp_var!-getval cdr v); 1271 ibalp_var!-setflip(cdr v,nil) 1272 >> 1273 >>; 1274 for each v in varal do << 1275 ibalp_var!-delallwc cdr v 1276 >>; 1277 for each c in clausel do 1278 ibalp_clause!-delallwl c 1279 >>; 1280 1281procedure ibalp_calccc!-fuip(ec,level,lv); 1282 % Calculate conflict clause after Strategy: First UIP. [ec] is the 1283 % empty clause to start the calculation with; [level] is the 1284 % conflict level; [lv] is the last variable set. Returns the new 1285 % learnt clause. 1286 begin scalar newclause,tv,reas; 1287 newclause := ibalp_clause!-new(); 1288 ibalp_resolve(newclause,ec,ibalp_var!-getreas lv,lv); 1289 while tv := ibalp_countgetlev(newclause,level) do << 1290 if eqn(ibalp_var!-getval tv,0) then 1291 ibalp_dellit(tv,newclause,t) 1292 else 1293 ibalp_dellit(tv,newclause,nil); 1294 reas := ibalp_var!-getreas tv; 1295 if ibalp_clause!-getcount reas then 1296 ibalp_clause!-setcount(reas,ibalp_clause!-getcount reas + 1); 1297 ibalp_resolve(newclause,newclause,reas,tv); 1298 >>; 1299 for each v in ibalp_clause!-getposlit newclause do 1300 ibalp_var!-setposcc(v,ibalp_var!-getposcc v + 1); 1301 for each v in ibalp_clause!-getneglit newclause do 1302 ibalp_var!-setnegcc(v,ibalp_var!-getnegcc v + 1); 1303 ibalp_clause!-setcount(newclause,1); 1304 return newclause 1305 end; 1306 1307procedure ibalp_countgetlev(clause,level); 1308 % Count variables at a certain level and return a variable at this 1309 % level if there are more than one. [clause] is a clause; [level] 1310 % is the level. Returns a 1311 % variable or [nil] 1312 begin scalar temp,tv,ret; 1313 tv := ibalp_clause!-getposlit clause; 1314 while tv and null ret do << 1315 temp := car tv; 1316 if ibalp_var!-getlev temp = level and 1317 ibalp_var!-getreas temp then 1318 ret := temp; 1319 tv := cdr tv; 1320 >>; 1321 tv := ibalp_clause!-getneglit clause; 1322 while tv and null ret do << 1323 temp := car tv; 1324 if ibalp_var!-getlev temp = level and 1325 ibalp_var!-getreas temp then 1326 ret := temp; 1327 tv := cdr tv; 1328 >>; 1329 return ret 1330 end; 1331 1332procedure ibalp_dellit(lit,clause,posneg); 1333 % Delete a literal from a clause. [lit] is the literal to delete; 1334 % [clause] is the clause; [posneg] is [t] if it is a true literal, 1335 % [nil] else; 1336 if posneg then << 1337 ibalp_var!-setposoccabs(lit,lto_delq(clause,ibalp_var!-getposocc lit)); 1338 ibalp_clause!-setposlitabs( 1339 clause,lto_delq(lit,ibalp_clause!-getposlit clause)) 1340 >> else << 1341 ibalp_var!-setnegoccabs(lit,lto_delq(clause,ibalp_var!-getnegocc lit)); 1342 ibalp_clause!-setneglitabs( 1343 clause,lto_delq(lit,ibalp_clause!-getneglit clause)) 1344 >>; 1345 1346procedure ibalp_dimcount(clausel); 1347 % Decrease the counter of newly added clauses. [clausel] is the 1348 % list of clauses. 1349 begin scalar doit,tc,c; 1350 doit := t; 1351 tc := clausel; 1352 while doit do << 1353 c := car tc; 1354 if null ibalp_clause!-getcount c then 1355 doit := nil 1356 else 1357 ibalp_clause!-setcount(c,ibalp_clause!-getcount c - 0.05); 1358 tc := cdr tc 1359 >> 1360 end; 1361 1362procedure ibalp_killcount(clausel); 1363 % Delete clauses with a count < 1. [clausel] is the list of 1364 % clauses. Return the new list of clauses. 1365 begin scalar doit,tc,c; 1366 doit := t; 1367 tc := clausel; 1368 while doit do << 1369 c := car tc; 1370 if null ibalp_clause!-getcount c then doit := nil else << 1371 tc := cdr tc; 1372 if ibalp_clause!-getcount c < 1 then 1373 clausel := ibalp_delclause(c,clausel); 1374 >> 1375 >>; 1376 return clausel 1377 end; 1378 1379procedure ibalp_delclause(c,clausel); 1380 % Delete a clause. [c] is the clause to delete; [clausel] is the 1381 % list of clauses. 1382 << 1383 for each v in ibalp_clause!-getposlit c do << 1384 ibalp_var!-setposoccabs(v,lto_delq(c,ibalp_var!-getposocc v)); 1385 if ibalp_clause!-getcount c then 1386 ibalp_var!-setposcc(v,ibalp_var!-getposcc v - 1); 1387 if null ibalp_clause!-getsat c then 1388 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v - 1); 1389 ibalp_var!-setmom(v,ibalp_calcmom v) 1390 >>; 1391 for each v in ibalp_clause!-getneglit c do << 1392 ibalp_var!-setnegoccabs(v,lto_delq(c,ibalp_var!-getnegocc v)); 1393 if ibalp_clause!-getcount c then 1394 ibalp_var!-setnegcc(v,ibalp_var!-getnegcc v - 1); 1395 if null ibalp_clause!-getsat c then 1396 ibalp_var!-setnumneg(v,ibalp_var!-getnumneg v - 1); 1397 ibalp_var!-setmom(v,ibalp_calcmom v) 1398 >>; 1399 for each v in ibalp_clause!-getwl c do << 1400 ibalp_var!-delwc(v,c); 1401 >>; 1402 clausel := lto_delq(c,clausel); 1403 clausel 1404 >>; 1405 1406procedure ibalp_getmacvext(varal); 1407 % Get most active variable. [varal] is the list of 1408 % variables. Returns a pair of the most active variable and its 1409 % value. 1410 begin scalar tv,tm,val; 1411 tv := ibalp_cv varal; 1412 if ibalp_var!-getposcc tv > ibalp_var!-getnegcc tv then << 1413 tm := ibalp_var!-getposcc tv; 1414 val := 1 1415 >> else << 1416 tm := ibalp_var!-getnegcc tv; 1417 val := 0 1418 >>; 1419 for each v in varal do 1420 if null ibalp_var!-getval cdr v then << 1421 if ibalp_var!-getposcc cdr v > tm then << 1422 tv := cdr v; 1423 val := 1; 1424 tm := ibalp_var!-getposcc tv 1425 >>; 1426 if ibalp_var!-getnegcc cdr v > tm then << 1427 tv := cdr v; 1428 val := 0; 1429 tm := ibalp_var!-getnegcc tv 1430 >> 1431 >>; 1432 return (tv . val) 1433 end; 1434 1435procedure ibalp_recalcv(varal); 1436 % Recalc variables activity value. [varal] is the A-List of 1437 % variables. 1438 for each v in varal do << 1439 ibalp_var!-setposcc(cdr v,ibalp_var!-getposcc cdr v - 0.05); 1440 ibalp_var!-setnegcc(cdr v,ibalp_var!-getnegcc cdr v - 0.05) 1441 >>; 1442 1443procedure ibalp_calccvar(cc,level); 1444 % Calclate the only conflict variable set at the conflict 1445 % level. [cc] is the conflict clause; [varal] is the A-List of 1446 % variables; [level] is the conflict level. Returns a Pair. The 1447 % first entry is the conflict variable and the second is the 1448 % highest level of all other variables. 1449 begin scalar v,rv; integer lev; 1450 for each v in ibalp_clause!-getposlit cc do << 1451 if eqn(ibalp_var!-getlev v,level) then 1452 rv := v 1453 else 1454 if ibalp_var!-getlev v > lev then lev := ibalp_var!-getLev v 1455 >>; 1456 for each v in ibalp_clause!-getneglit cc do << 1457 if eqn(ibalp_var!-getlev v,level) then 1458 rv := v 1459 else 1460 if ibalp_var!-getlev v > lev then lev := ibalp_var!-getLev v 1461 >>; 1462 return (rv . lev) 1463 end; 1464 1465procedure ibalp_tvb(varal,level); 1466 % Take back all variable assignments down to a certain 1467 % level. [varal] is the A-List of variables; [level] is the level. 1468 for each v in varal do 1469 if ibalp_var!-getlev cdr v >= level then 1470 ibalp_var!-unset(cdr v,ibalp_var!-getval cdr v); 1471 1472procedure ibalp_istotal(varal); 1473 % Checks if an assignment is total. [varal] is a A-List of 1474 % variables. Returns [t] if the assigenment is total [nil] else. 1475 null varal or (ibalp_var!-getval cdar varal and 1476 ibalp_istotal cdr varal); 1477 1478procedure ibalp_getvar!-zmom(varal,clausel); 1479 % Get a variable following the ZMOM (maximum occurrences in minimal 1480 % clauses ) strategy. [varal] is a A-List of variables. Returns a 1481 % Pair. The first entry is the chosen variable, the second entry 1482 % is the value the variable should be set to. 1483 begin scalar minc,tv,tmax,h,val; 1484 minc := ibalp_minclnr clausel; 1485 tmax := -1; 1486 for each v in varal do << 1487 if null ibalp_var!-getval cdr v and 1488 (h := ibalp_var!-getmom cdr v) > tmax then 1489 if ibalp_isinminclause(cdr v,minc) then << 1490 tv := cdr v; 1491 tmax := h 1492 >> 1493 >>; 1494 val := if ibalp_var!-getposcc tv > ibalp_var!-getnegcc tv then 1 else 0; 1495 return (tv . val) 1496 end; 1497 1498procedure ibalp_isinminclause(var,minc); 1499 % Check if a variable is in a clause of minmal size. [var] is a 1500 % variable; [minc] is the size of a minimal clause. Returns [t] if 1501 % the variable is in a clause of minimal size, [nil] else. 1502 begin scalar tv,ret; 1503 tv := ibalp_var!-getposocc var; 1504 while tv and null ret do << 1505 if null ibalp_clause!-getsat car tv and 1506 eqn(ibalp_clause!-getactneg car tv + 1507 ibalp_clause!-getactpos car tv,minc) then 1508 ret := t; 1509 tv := cdr tv; 1510 >>; 1511 tv := ibalp_var!-getnegocc var; 1512 while tv and null ret do << 1513 if null ibalp_clause!-getsat car tv and 1514 eqn(ibalp_clause!-getactneg car tv + 1515 ibalp_clause!-getactpos car tv,minc) then 1516 ret := t; 1517 tv := cdr tv; 1518 >>; 1519 return ret 1520 end; 1521 1522procedure ibalp_getvar!-dlcs(varal); 1523 % Get a variable following the DLCS (dynamic largest combined sum) 1524 % strategy. [varal] is a A-List of variables. Returns a Pair. The 1525 % first entry is the chosen variable, the second entry is the value 1526 % the variable should be set to. 1527 begin scalar tv,max,val; 1528 tv := ibalp_cv varal; 1529 max := ibalp_var!-getnumneg tv + ibalp_var!-getnumpos tv; 1530 for each var in varal do 1531 if null ibalp_var!-getval cdr var then 1532 if ibalp_var!-getnumneg cdr var + 1533 ibalp_var!-getnumpos cdr var > max then << 1534 tv := cdr var; 1535 max := ibalp_var!-getnumneg cdr var + 1536 ibalp_var!-getnumpos cdr var 1537 >>; 1538 val := if ibalp_var!-getnumpos tv > ibalp_var!-getnumneg tv then 1539 1 1540 else 1541 0; 1542 return (tv . val) 1543 end; 1544 1545procedure ibalp_minclnr(clausel); 1546 % Get the size of a minimal clause. [clausel] is the list of 1547 % clauses. Returns the size of a minimum clause. 1548 begin scalar min; 1549 %hack 1550 min := 100000; 1551 for each c in clausel do 1552 if null ibalp_clause!-getsat c then 1553 if ibalp_clause!-getactpos c + 1554 ibalp_clause!-getactneg c < min then 1555 min := ibalp_clause!-getactpos c + 1556 ibalp_clause!-getactneg c; 1557 return min 1558 end; 1559 1560procedure ibalp_calcmom(var); 1561 % Calculate the zmom value of a variable. [var] is a 1562 % variable. Returns the mom value. 1563 (ibalp_var!-getnumpos var + ibalp_var!-getnumneg var)*32 + 1564 (ibalp_var!-getnumpos var * ibalp_var!-getnumneg var); 1565 1566procedure ibalp_cec(clausel); 1567 % Check empty clauses. [clausel] is the list of clauses. Returns 1568 % the first empty clause if there is one (a clause which is false 1569 % but has also no unset variables), else [nil]. 1570 if null clausel then 1571 nil 1572 else if ibalp_emptyclausep car clausel then 1573 car clausel 1574 else 1575 ibalp_cec cdr clausel; 1576 1577procedure ibalp_emptyclausep(clause); 1578 null ibalp_clause!-getsat clause and 1579 eqn(ibalp_clause!-getactpos clause,0) and 1580 eqn(ibalp_clause!-getactneg clause,0); 1581 1582procedure ibalp_csat(clausel); 1583 % Check SAT. [clausel] is the list of clauses. Returns [t] if all 1584 % the clauses are true, else [nil]. 1585 null clausel or (ibalp_clause!-getsat car clausel 1586 and ibalp_csat cdr clausel); 1587 1588procedure ibalp_cv(varal); 1589 % Choose a variable. [varal] is the A-List of variables. Returns a 1590 % unset variable. 1591 if null ibalp_var!-getval cdar varal then 1592 cdar varal 1593 else 1594 ibalp_cv cdr varal; 1595 1596procedure ibalp_var!-set(var,val,level,reas); 1597 % Set a variable. [var] is the variable; [val] is value to be set; 1598 % [level] is the level the variable is set; [reas] is the reason 1599 % why the variable is set. Sets the given variable from [nil] to 1600 % [val] and updates all needed data structures. Returns a pair of 1601 % new unit clauses. 1602 begin scalar id,sc,upl; 1603 ibalp_var!-setval(var,val); 1604 ibalp_var!-setlev(var,level); 1605 ibalp_var!-setreas(var,reas); 1606 id := ibalp_var!-getid var; 1607 sc := if eqn(val,0) then 1608 ibalp_var!-getnegocc var 1609 else 1610 ibalp_var!-getposocc var; 1611 ibalp_var!-satlist(sc,id); 1612 sc := if eqn(val,1) then 1613 ibalp_var!-getnegocc var 1614 else 1615 ibalp_var!-getposocc var; 1616 ibalp_var!-unsatlist(sc,val); 1617 upl := ibalp_var!-wclist var; 1618 ibalp_var!-setmom(var,ibalp_calcmom var); 1619 return upl 1620 end; 1621 1622procedure ibalp_var!-satlist(sc,id); 1623 % Perform changes on the list of satisfied clauses. [sc] is the 1624 % list of satisfied clauses; [id] is the identifier of the 1625 % variable. 1626 for each clause in sc do << 1627 if null ibalp_clause!-getsat clause then << 1628 for each v in ibalp_clause!-getposlit clause do << 1629 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v - 1); 1630 ibalp_var!-setmom(v,ibalp_calcmom v) 1631 >>; 1632 for each v in ibalp_clause!-getneglit clause do << 1633 ibalp_var!-setnumneg(v, ibalp_var!-getnumneg v - 1); 1634 ibalp_var!-setmom(v,ibalp_calcmom v) 1635 >>; 1636 for each v in ibalp_clause!-getwl clause do << 1637 ibalp_var!-delwc(v,clause) 1638 >>; 1639 ibalp_clause!-delallwl clause; 1640 >>; 1641 ibalp_clause!-setsat(clause,id) 1642 >>; 1643 1644procedure ibalp_var!-unsatlist(sc,val); 1645 % Perform changes on the list of unsatisfied clauses. [sc] is the 1646 % list of unsatisfied clauses; [val] is the value of the 1647 % variable. 1648 for each clause in sc do 1649 if eqn(val,1) then 1650 ibalp_clause!-setactneg(clause, 1651 ibalp_clause!-getactneg clause - 1) 1652 else 1653 ibalp_clause!-setactpos(clause, 1654 ibalp_clause!-getactpos clause - 1); 1655 1656procedure ibalp_var!-wclist(var); 1657 % Perform changes on the list of watched clauses. [var] is the 1658 % variable. Returns the list of unit clauses. 1659 begin scalar newwl,upl; 1660 for each c in ibalp_var!-getwc var do 1661 if null ibalp_clause!-getsat c then << 1662 ibalp_clause!-delwl(c,var); 1663 ibalp_var!-delwc(var,c); 1664 newwl := ibalp_getnewwl c; 1665 if null newwl then 1666 upl := c . upl 1667 else << 1668 ibalp_clause!-setwl(c,newwl); 1669 ibalp_var!-setwc(newwl,c) 1670 >> 1671 >>; 1672 return upl 1673 end; 1674 1675procedure ibalp_var!-setq(var,val,level,reas); 1676 % Set a variable (QSAT). [var] is the variable; [val] is value to 1677 % be set; [varal] is the list of variables; [level] is the level 1678 % the variable is set; [reas] is the reason why the variable is 1679 % set. Sets the given variable from [nil] to [val] and updates all 1680 % needed data structures. Returns a pair of new unit clauses and 1681 % new conflict clauses. 1682 begin scalar clause,id,sc,upl,h,ec; 1683 ibalp_var!-setval(var,val); 1684 ibalp_var!-setlev(var,level); 1685 ibalp_var!-setreas(var,reas); 1686 id := ibalp_var!-getid var; 1687 sc := if eqn(val,0) then 1688 ibalp_var!-getnegocc var 1689 else 1690 ibalp_var!-getposocc var; 1691 ibalp_var!-satlistq(sc,id); 1692 sc := if eqn(val,1) then 1693 ibalp_var!-getnegocc var 1694 else 1695 ibalp_var!-getposocc var; 1696 for each clause in sc do << 1697 if eqn(val,1) then 1698 ibalp_clause!-setactneg(clause, 1699 ibalp_clause!-getactneg clause - 1) 1700 else 1701 ibalp_clause!-setactpos(clause, 1702 ibalp_clause!-getactpos clause - 1); 1703 if h := ibalp_qsat!-isunit clause then upl := (h . clause) . upl; 1704 if ibalp_qsat!-isec clause then ec := clause 1705 >>; 1706 ibalp_var!-setmom(var,ibalp_calcmom var); 1707 return (upl . ec) 1708 end; 1709 1710procedure ibalp_var!-satlistq(sc,id); 1711 % Perform changes on the list of satisfied clauses. [sc] is the 1712 % list of satisfied clauses; [id] is the identifier of the 1713 % variable. 1714 for each clause in sc do << 1715 if null ibalp_clause!-getsat clause then << 1716 for each v in ibalp_clause!-getposlit clause do << 1717 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v - 1); 1718 ibalp_var!-setmom(v,ibalp_calcmom v) 1719 >>; 1720 for each v in ibalp_clause!-getneglit clause do << 1721 ibalp_var!-setnumneg(v, ibalp_var!-getnumneg v - 1); 1722 ibalp_var!-setmom(v,ibalp_calcmom v) 1723 >>; 1724 >>; 1725 ibalp_clause!-setsat(clause,id) 1726 >>; 1727 1728procedure ibalp_var!-unset(var,val); 1729 % Unset a variable. [var] is the variable; [val] is value to be 1730 % unset. Sets the given variable from [val] to [nil] and updates 1731 % all needed data structures. 1732 begin scalar clause,id,sc; 1733 ibalp_var!-setval(var,nil); 1734 ibalp_var!-setlev(var,-1); 1735 ibalp_var!-setreas(var,nil); 1736 id := ibalp_var!-getid var; 1737 sc := if eqn(val,1) then 1738 ibalp_var!-getnegocc var 1739 else 1740 ibalp_var!-getposocc var; 1741 for each clause in sc do << 1742 if eqn(val,1) then 1743 ibalp_clause!-setactneg(clause, 1744 ibalp_clause!-getactneg clause +1) 1745 else 1746 ibalp_clause!-setactpos(clause, 1747 ibalp_clause!-getactpos clause +1) 1748 >>; 1749 sc := if eqn(val,0) then 1750 ibalp_var!-getnegocc var 1751 else 1752 ibalp_var!-getposocc var; 1753 ibalp_unvar!-unsatlist(sc,id); 1754 ibalp_var!-setmom(var,ibalp_calcmom var) 1755 end; 1756 1757procedure ibalp_unvar!-unsatlist(sc,id); 1758 % Perform changes on the list of unsatisfied clauses. [sc] is the 1759 % list of unsatisfied clauses; [id] is the identifier of the 1760 % variable. 1761 begin scalar newwl; 1762 for each clause in sc do << 1763 ibalp_clause!-delsat(clause,id); 1764 if null ibalp_clause!-getsat clause then << 1765 for each v in ibalp_clause!-getposlit clause do << 1766 ibalp_var!-setnumpos(v, ibalp_var!-getnumpos v + 1); 1767 ibalp_var!-setmom(v,ibalp_calcmom v) 1768 >>; 1769 for each v in ibalp_clause!-getneglit clause do << 1770 ibalp_var!-setnumneg(v, ibalp_var!-getnumneg v + 1); 1771 ibalp_var!-setmom(v,ibalp_calcmom v) 1772 >>; 1773 for each v in ibalp_clause!-getwl clause do << 1774 ibalp_var!-delwc(v,clause) 1775 >>; 1776 ibalp_clause!-delallwl clause; 1777 newwl := ibalp_getnewwl clause; 1778 ibalp_clause!-setwl(clause,newwl); 1779 ibalp_var!-setwc(newwl,clause); 1780 newwl := ibalp_getnewwl clause; 1781 if newwl then << 1782 ibalp_clause!-setwl(clause,newwl); 1783 ibalp_var!-setwc(newwl,clause) 1784 >> 1785 >> 1786 >>; 1787 end; 1788 1789procedure ibalp_var!-unsetq(var,val); 1790 % Unset a variable (QSAT). [var] is the variable; [val] is value to 1791 % be unset; Sets the given variable from [val] to [nil] and updates 1792 % all needed data structures. 1793 begin scalar clause,v,id,sc; 1794 ibalp_var!-setval(var,nil); 1795 ibalp_var!-setlev(var,-1); 1796 ibalp_var!-setreas(var,nil); 1797 id := ibalp_var!-getid var; 1798 sc := if eqn(val,1) then 1799 ibalp_var!-getnegocc var 1800 else 1801 ibalp_var!-getposocc var; 1802 ibalp_unvar!-unsatlistq(sc,val); 1803 sc := if eqn(val,0) then 1804 ibalp_var!-getnegocc var 1805 else 1806 ibalp_var!-getposocc var; 1807 for each clause in sc do << 1808 ibalp_clause!-delsat(clause,id); 1809 if null ibalp_clause!-getsat clause then << 1810 for each v in ibalp_clause!-getposlit clause do << 1811 ibalp_var!-setnumpos(v, ibalp_var!-getnumpos v + 1); 1812 ibalp_var!-setmom(v,ibalp_calcmom v) 1813 >>; 1814 for each v in ibalp_clause!-getneglit(clause) do << 1815 ibalp_var!-setnumneg(v, ibalp_var!-getnumneg v + 1); 1816 ibalp_var!-setmom(v,ibalp_calcmom v) 1817 >>; 1818 >> 1819 >>; 1820 ibalp_var!-setmom(var,ibalp_calcmom var) 1821 end; 1822 1823procedure ibalp_unvar!-unsatlistq(sc,val); 1824 % Perform changes on the list of unsatisfied clauses. [sc] is the 1825 % list of unsatisfied clauses; [val] is the value of the 1826 % variable. 1827 for each clause in sc do << 1828 if eqn(val,1) then 1829 ibalp_clause!-setactneg(clause, 1830 ibalp_clause!-getactneg clause +1) 1831 else 1832 ibalp_clause!-setactpos(clause, 1833 ibalp_clause!-getactpos clause +1) 1834 >>; 1835 1836procedure ibalp_getnewwl(clause); 1837 % Get a new watched literal for a clause. [clause] is a clause; 1838 % Returns a new watched literal or [nil]. 1839 begin scalar tl,wl; 1840 tl := ibalp_clause!-getposlit clause; 1841 while tl and null wl do << 1842 if null ibalp_var!-getval car tl and 1843 null memq(car tl,ibalp_clause!-getwl clause) 1844 then 1845 wl := car tl; 1846 tl := cdr tl 1847 >>; 1848 tl := ibalp_clause!-getneglit clause; 1849 while tl and null wl do << 1850 if null ibalp_var!-getval car tl and 1851 null memq(car tl,ibalp_clause!-getwl clause) 1852 then 1853 wl := car tl; 1854 tl := cdr tl 1855 >>; 1856 return wl 1857 end; 1858 1859procedure ibalp_iscnf(f); 1860 ibalp_clausep f or (rl_op f eq 'and and ibalp_clauselp rl_argn f); 1861 1862procedure ibalp_clauselp(l); 1863 null l or (ibalp_clausep car l and ibalp_clauselp cdr l); 1864 1865procedure ibalp_clausep(s); 1866 ibalp_litp s or (rl_op s eq 'or and ibalp_litlp rl_argn s); 1867 1868procedure ibalp_litlp(l); 1869 null l or (ibalp_litp car l and ibalp_litlp cdr l); 1870 1871procedure ibalp_litp(s); 1872 ibalp_atomp s or (rl_op s eq 'not and ibalp_atomp rl_arg1 s); 1873 1874procedure ibalp_atomp(s); 1875 % We consider true and false to be atomic formulas at this point. 1876 rl_tvalp s or (rl_op s eq 'equal and idp ibalp_arg2l s and numberp ibalp_arg2r s); 1877 1878procedure ibalp_readform(f); 1879 % Read a formula in cnf. [f] is a formula in cnf in lisp 1880 % prefix. Returns a pair: [clausel] is the list of clauses; [varal] 1881 % is the A-List of variables. 1882 begin scalar pair,clausel,varal,clause,argn,x,c; integer count; 1883 f := cl_mkstrict(f,'and); 1884 argn := rl_argn f; 1885 c := t; while c and argn do << 1886 x := car argn; 1887 argn := cdr argn; 1888 pair := ibalp_readclause(x,varal); 1889 clause := car pair; 1890 varal := cdr pair; 1891 if clause neq 'true then << 1892 if ibalp_emptyclausep clause then 1893 c := nil 1894 else 1895 (if ibalp_clmember(clause,clausel) or ibalp_redclause clause then << 1896 ibalp_undoclause clause; 1897 count := count + 1 1898 >> else 1899 clausel := car pair . clausel) 1900 >> 1901 >>; 1902 if null c then << 1903 if !*rlverbose then 1904 ioto_tprin2t {"Detected empty clause"}; 1905 return {clause} . nil 1906 >>; 1907 if null clausel then << 1908 if !*rlverbose then 1909 ioto_tprin2t {"Tautology detected"}; 1910 return nil . nil 1911 >>; 1912 if !*rlverbose then 1913 ioto_tprin2t {"Deleted redundant clauses: ",count}; 1914 return (clausel . varal) 1915 end; 1916 1917procedure ibalp_clmember(x,l); 1918 l and (ibalp_cequal(x,car l) or ibalp_clmember(x,cdr l)); 1919 1920procedure ibalp_cequal(c1,c2); 1921 begin scalar poslitl1,neglitl1,poslitl2,neglitl2; 1922 poslitl1 := for each v in ibalp_clause!-getposlit c1 collect 1923 ibalp_var!-getid v; 1924 poslitl2 := for each v in ibalp_clause!-getposlit c2 collect 1925 ibalp_var!-getid v; 1926 if not lto_setequalq(poslitl1,poslitl2) then 1927 return nil; 1928 neglitl1 := for each v in ibalp_clause!-getneglit c1 collect 1929 ibalp_var!-getid v; 1930 neglitl2 := for each v in ibalp_clause!-getneglit c2 collect 1931 ibalp_var!-getid v; 1932 return lto_setequalq(neglitl1,neglitl2) 1933 end; 1934 1935procedure ibalp_undoclause(clause); 1936 % Undo a clause if it redundant. [clause] is a clause. 1937 << 1938 for each v in ibalp_clause!-getposlit clause do << 1939 ibalp_var!-setposoccabs(v,lto_delq(clause,ibalp_var!-getposocc v)); 1940 ibalp_var!-setnumpos(v,ibalp_var!-getnumpos v - 1); 1941 ibalp_var!-setposcc(v,ibalp_var!-getposcc v - 1) 1942 >>; 1943 for each v in ibalp_clause!-getneglit clause do << 1944 ibalp_var!-setnegoccabs(v,lto_delq(clause,ibalp_var!-getnegocc v)); 1945 ibalp_var!-setnumneg(v,ibalp_var!-getnumneg v - 1); 1946 ibalp_var!-setnegcc(v,ibalp_var!-getnegcc v - 1) 1947 >> 1948 >>; 1949 1950procedure ibalp_redclause(clause); 1951 % Checks if a new clause is redundant. [clause] is a 1952 % clause. Returns [t] if the clause is redundant, [nil] else. 1953 begin scalar tv,ret; 1954 tv := ibalp_clause!-getposlit clause; 1955 while tv and null ret do << 1956 if ibalp_vmember(car tv,ibalp_clause!-getneglit clause) then 1957 ret := t; 1958 tv := cdr tv 1959 >>; 1960 return ret 1961 end; 1962 1963procedure ibalp_vmember(v,vl); 1964 vl and (ibalp_vequal(v,car vl) or ibalp_vmember(v,cdr vl)); 1965 1966procedure ibalp_vequal(v1,v2); 1967 ibalp_var!-getid v1 eq ibalp_var!-getid v2; 1968 1969procedure ibalp_readclause(c,varal); 1970 % Read a clause. [c] is a clause in lisp prefix; [varal] is the 1971 % A-List of variables. Returns a pair: [clause] is the created 1972 % datastructure for this clause; [varal] is the updated list of 1973 % variables. 1974 begin scalar x,id,val,clause,nc,posids,negids,cnt; 1975 nc := rl_argn c; 1976 clause := ibalp_clause!-new(); 1977 cnt := t; while cnt and nc do << 1978 x := car nc; 1979 if x eq 'true then 1980 cnt := nil 1981 else << 1982 nc := cdr nc; 1983 if x neq 'false then << 1984 if rl_op x eq 'not then << 1985 id := ibalp_arg2l rl_arg1 x; 1986 val := 1 #- ibalp_arg2r rl_arg1 x 1987 >> else << 1988 id := ibalp_arg2l x; 1989 val := ibalp_arg2r x 1990 >>; 1991 if val #= 1 then << 1992 if not memq(id,posids) then << 1993 ibalp_clause!-setactpos(clause, 1994 ibalp_clause!-getactpos clause + 1); 1995 posids := id . posids; 1996 varal := ibalp_process!-var(clause,varal,id,1) 1997 >> 1998 >> else << 1999 if not memq(id,negids) then << 2000 ibalp_clause!-setactneg(clause, 2001 ibalp_clause!-getactneg clause + 1); 2002 negids := id . negids; 2003 varal := ibalp_process!-var(clause,varal,id,0) 2004 >> 2005 >> 2006 >> 2007 >> 2008 >>; 2009 if not cnt then 2010 return 'true . varal; 2011 return (clause . varal) 2012 end; 2013 2014procedure ibalp_qsat!-readdimacs2(file); 2015 % Read a .cnf or .qdimacs file. [file] is the filename. Returns a 2016 % pair of the clauses and variables of this file. 2017 begin scalar ch,tok,doit,numvars,numclauses,varal,clausel,pair,qsat; 2018 ch := open(file, 'input); 2019 rds ch; 2020 tok := read(); 2021 if not (tok eq 'p or tok eq 'c) then << 2022 rederr "Invalid input format"; 2023 rds nil; 2024 close(ch); 2025 return {'false} 2026 >>; 2027 if tok eq 'c then doit := t; 2028 while doit do << 2029 tok := read(); 2030 if tok eq 'p then doit := nil 2031 >>; 2032 tok := read(); 2033 if not (tok eq 'cnf) then rederr "Invalid input format"; 2034 numvars := read(); 2035 numclauses := read(); 2036 if !*rlverbose then 2037 ioto_tprin2t {"Reading ",numvars," variables and ", 2038 numclauses," clauses"}; 2039 tok := read(); 2040 if tok eq 'e or tok eq 'a then << 2041 qsat := t; 2042 if !*rlverbose then 2043 ioto_tprin2t "Q-SAT: Reading quantifiers"; 2044 pair := ibalp_readquant!-cnf(tok); 2045 tok := car pair; 2046 varal := cdr pair 2047 >>; 2048 pair := ibalp_readclause!-cnf(numclauses,varal,tok); 2049 clausel := car pair; 2050 varal := cdr pair; 2051 rds nil; 2052 close(ch); 2053 return (qsat . (clausel . varal)) 2054 end; 2055 2056procedure ibalp_readquant!-cnf(tok); 2057 % Read quantifier list from a .qdimacs file. [tok] is the last read 2058 % token. Returns a pair of the last read token and the new 2059 % variables. 2060 begin scalar varal,quant,level,doit,qswitch,var; 2061 if tok eq 'e then quant := 'ex else quant := 'all; 2062 level := 1; 2063 doit := t; 2064 while doit or qswitch do << 2065 tok := read(); 2066 if eqn(tok,0) then << 2067 doit := nil; 2068 tok := read(); 2069 if tok eq 'a or tok eq 'e then << 2070 qswitch := t; 2071 quant := if tok eq 'a then 'all else 'ex; 2072 level := level + 1 2073 >> else 2074 qswitch := nil; 2075 >> else << 2076 var := ibalp_var!-new(tok); 2077 ibalp_var!-setqlevel(var,level); 2078 ibalp_var!-setquant(var,quant); 2079 varal := (tok . var) . varal; 2080 >> 2081 >>; 2082 varal := reverse varal; 2083 return (tok . varal) 2084 end; 2085 2086procedure ibalp_readclause!-cnf(numclauses,varal,lt); 2087 % Reads the clauses of a .cnf or .qdimacs file. [numclauses] is the 2088 % number of clauses; [varal] is the A-List of variables; [lt] is 2089 % the last read token. Returns a pair of clauses / variables. 2090 begin scalar doit,poslit,neglit,clause,tok,clausel,first; integer count; 2091 first := t; 2092 for i := 1 : numclauses do << 2093 doit := t; 2094 poslit := nil; 2095 neglit := nil; 2096 clause := ibalp_clause!-new(); 2097 while doit do << 2098 if first then << 2099 tok := lt; 2100 first := nil 2101 >> 2102 else 2103 tok := read(); 2104 if tok = 0 then 2105 doit := nil 2106 else 2107 if tok < 0 and null memq(-tok,neglit) then << 2108 ibalp_clause!-setactneg(clause, 2109 ibalp_clause!-getactneg clause + 1); 2110 varal := ibalp_process!-var(clause,varal,-tok,0) 2111 >> else if tok > 0 and null memq(tok,poslit) then << 2112 ibalp_clause!-setactpos(clause, 2113 ibalp_clause!-getactpos clause + 1); 2114 varal := ibalp_process!-var(clause,varal,tok,1) 2115 >> 2116 >>; 2117 if ibalp_clmember(clause,clausel) or ibalp_redclause clause then << 2118 ibalp_undoclause clause; 2119 count := count + 1 2120 >> else 2121 clausel := clause . clausel; 2122 >>; 2123 if !*rlverbose then 2124 ioto_tprin2t {"Deleted Redundant Clauses: ",count}; 2125 return (clausel . varal) 2126 end; 2127 2128procedure ibalp_process!-var(clause,varal,id,val); 2129 % Process a variable of the input. [clause] is a clause; [varal] is 2130 % the A-List of variables; [id] is a number; [val] is the value of 2131 % the variable. Returns the new A-List of variables. 2132 begin scalar h,var; 2133 id := intern compress('!! . explode id); 2134 if h := atsoc(id,varal) then 2135 var := cdr h 2136 else << 2137 var := ibalp_var!-new(id); 2138 varal := (id . var) . varal 2139 >>; 2140 if eqn(val,1) then << 2141 ibalp_var!-setposocc(var,clause); 2142 ibalp_var!-setnumpos(var,ibalp_var!-getnumpos var + 1); 2143 ibalp_var!-setposcc(var,ibalp_var!-getposcc var + 1); 2144 ibalp_clause!-setposlit(clause,var) 2145 >> 2146 else << 2147 ibalp_var!-setnegocc(var,clause); 2148 ibalp_var!-setnumneg(var,ibalp_var!-getnumneg var + 1); 2149 ibalp_var!-setnegcc(var,ibalp_var!-getnegcc var + 1); 2150 ibalp_clause!-setneglit(clause,var) 2151 >>; 2152 return varal 2153 end; 2154 2155procedure ibalp_get3cnf(f); 2156 % Generate set of polynomials 3CNF. [f] is a formula. [trthval] is 2157 % 0 or 1. Returns a list of polynomials by transforming [f] into a 2158 % into a conjunctive clausal form, containing max 3 variables per 2159 % clause. 2160 begin scalar newf,newform; 2161 newf := f; 2162 newf := ibalp_pset3knfnf newf; 2163 newf := ibalp_pset3knf2(newf,nil); 2164 newf := if rl_op newf eq 'and then 2165 rl_mkn('and,for each j in rl_argn newf join 2166 ibalp_pset3knf3(j,nil)) 2167 else 2168 rl_smkn('and,ibalp_pset3knf3(newf,nil)); 2169 newform := for each c in rl_argn newf join 2170 if rl_op c = 'equal or rl_op c = 'not then 2171 {c} 2172 else 2173 rl_argn ibalp_cnf c; 2174 newform := 'and . newform; 2175 return newform 2176 end; 2177 2178procedure ibalp_convcnf(clausel,varal,qsat); 2179 % Converts a list of clauses and variables into Lisp 2180 % Prefix. [clausel] is the list of variables; [varal] is the A-List 2181 % of variables; [qsat] indicates if it is a Q-SAT problem or 2182 % not. Returns the corresponding formula in lisp-prefix. 2183 begin scalar formula,tempcl,id,newvaral,rvaral; 2184 for each v in varal do << 2185 id := ibalp_var!-mkid ibalp_var!-getid cdr v; 2186 newvaral := (ibalp_var!-getid cdr v . id) . newvaral 2187 >>; 2188 for each clause in clausel do << 2189 tempcl := nil; 2190 for each v in ibalp_clause!-getposlit clause do << 2191 id := cdr atsoc(ibalp_var!-getid v,newvaral); 2192 tempcl := {'equal,id,1} . tempcl; 2193 >>; 2194 for each v in ibalp_clause!-getneglit clause do << 2195 id := cdr atsoc(ibalp_var!-getid v,newvaral); 2196 tempcl := {'equal,id,0} . tempcl 2197 >>; 2198 if length tempcl > 1 then 2199 tempcl := 'or . tempcl 2200 else 2201 tempcl := {'equal, cadar tempcl,caddar tempcl}; 2202 formula := tempcl . formula; 2203 >>; 2204 if length formula > 1 then 2205 formula := 'and . formula; 2206 if qsat then << 2207 rvaral := reverse varal; 2208 for each v in rvaral do << 2209 id := cdr atsoc(ibalp_var!-getid v,newvaral); 2210 if ibalp_var!-isex cdr v then 2211 formula := {'ex, id, formula} 2212 else 2213 formula := {'all, id, formula} 2214 >> 2215 >>; 2216 return formula 2217 end; 2218 2219procedure ibalp_var!-mkid(tok); 2220 % Turn a number into a identifier. [tok] is a number. Returns an 2221 % identifier. 2222 intern compress ('v . 'a . 'r . explode tok); 2223 2224%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% QSAT %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 2225 2226procedure ibalp_qsat!-cdcl(clausel,varal,origupl,qsat); 2227 % Main procedure for the conflictdriven clausel-learning QSAT 2228 % algorithm. [clausel] is the list of clauses; [varal] is the 2229 % A-List of variables; [origupl] is a set of initial unit clauses; 2230 % [qsat] indicates if it is a Q-SAT problem or a parametric 2231 % one. Return [true] if the formula is true, [false] else. 2232 begin scalar fin,break,res,level,pair,ec,lv,upl; 2233 pair := ibalp_qsat!-preprocess(clausel,varal,origupl,qsat); 2234 if car pair then return car pair; 2235 clausel := cadr pair; 2236 varal := cddr pair; 2237 level := 1; 2238 while null fin do << 2239 break := nil; 2240 pair := ibalp_qsat!-cv(clausel,varal,level); 2241 if cdr pair and eqn(level,1) then << 2242 res := {'false}; 2243 break := t; 2244 fin := t 2245 >> else 2246 upl := car pair; 2247 while null break do << 2248 pair := ibalp_qsat!-cdclup(upl,level); 2249 ec := car pair; 2250 lv := cdr pair; 2251 if ec then << 2252 pair := ibalp_qsat!-analconf(ec,lv,level,clausel,varal); 2253 if cddr pair < 0 then << 2254 res := {'false}; 2255 break := t; 2256 fin := t 2257 >> else << 2258 clausel := car pair; 2259 level := cddr pair; 2260 upl := car ibalp_qsat!-btcase(level, 2261 cadr pair,varal,car clausel,t); 2262 ec := nil 2263 >> 2264 >> else if ibalp_qsat!-csat clausel then << 2265 pair := ibalp_qsat!-analsatNAIV varal; 2266 if cdr pair <= 0 then << 2267 res := {'true}; 2268 break := t; 2269 fin := t 2270 >> else << 2271 level := cdr pair; 2272 upl := car ibalp_qsat!-btcase(level,car pair,varal,nil,nil); 2273 >> 2274 >> else << 2275 break := t; 2276 level := level + 1 2277 >> 2278 >> 2279 >>; 2280 return (res . (clausel . varal)) 2281 end; 2282 2283procedure ibalp_qsat!-preprocess(clausel,varal,origupl,qsat); 2284 % Perform pre-processing on the formula. [clausel] is the list of 2285 % clauses; [varal] is the A-List of variables; [origupl] is the set 2286 % of initial unit clauses; [qsat] indicates if it is a Q-SAT or a 2287 % parametric problem. Return a pair of clauses/variables and a 2288 % possible return value (Sudden death). 2289 begin scalar pair,res; 2290 pair := ibalp_qsat!-cdclup(origupl,-1); 2291 if car pair then res := ({'false} . (clausel . varal)); 2292 if qsat then << 2293 pair := ibalp_qsat!-doSimpl(clausel,varal); 2294 clausel := car pair; 2295 varal := cdr pair 2296 >>; 2297 if ibalp_qsat!-csat clausel then res := ({'true} . (clausel . varal)); 2298 if null clausel then res := ({'true} . (clausel . varal)); 2299 if ibalp_qsat!-abort clausel then res := ({'false} . (clausel . varal)); 2300 return (res . (clausel . varal)) 2301 end; 2302 2303procedure ibalp_qsat!-doSimpl(clausel,varal); 2304 % Do simplifications on the formula. [clausel] is the list of 2305 % clauses; [varal] is the A-List of variables. Return a pair of 2306 % clauses and variables. 2307 begin scalar h,pair; integer count; 2308 while h := ibalp_hassimple clausel do << 2309 pair := ibalp_simplify(nil,nil,h,clausel,varal); 2310 clausel := car pair; 2311 varal := cdr pair 2312 >>; 2313 for each v in varal do << 2314 if ibalp_var!-isex cdr v and 2315 eqn(ibalp_var!-getnumpos cdr v,0) then << 2316 count := count + 1; 2317 ibalp_var!-setq(cdr v,0,0,nil); 2318 pair := ibalp_simplify(cdr v,0,nil,clausel,varal); 2319 clausel := car pair; 2320 varal := cdr pair; 2321 >> else if ibalp_var!-isex cdr v and 2322 eqn(ibalp_var!-getnumneg cdr v,0) then << 2323 count := count + 1; 2324 ibalp_var!-setq(cdr v,1,0,nil); 2325 pair := ibalp_simplify(cdr v,1,nil,clausel,varal); 2326 clausel := car pair; 2327 varal := cdr pair; 2328 >> 2329 >>; 2330 if !*rlverbose then 2331 ioto_tprin2t {"Deleted variables in pre-processing: ",count}; 2332 return (clausel . varal) 2333 end; 2334 2335procedure ibalp_qsat!-cv(clausel,varal,level); 2336 % Choose and set a variable. [clausel] is the list of clauses; 2337 % [varal] is the A-List of variables; [level] is the current 2338 % level. Returns the new list of unit clauses. 2339 begin scalar cv,temp; 2340 cv := ibalp_qsat!-mom(varal,clausel); 2341 temp := ibalp_var!-setq(cv,1,level,nil); 2342 if cdr temp then << 2343 ibalp_var!-unsetq(cv,1); 2344 temp := ibalp_var!-setq(cv,0,level,nil) 2345 >>; 2346 ibalp_var!-setflip(cv,0); 2347 return temp 2348 end; 2349 2350procedure ibalp_qsat!-btcase(blevel,bvar,varal,cc,val); 2351 % Subprocedure for the backtrack case. [blevel] is the backtracking 2352 % level; [bvar] is the backtrack variable; [varal] is the A-List of 2353 % variables; [cc] is the new learnt clause; [val] indicates if it 2354 % is a conflict-driven or a SAT-driven backtracking. Returns the 2355 % list of new unit clauses. 2356 begin scalar tval,temp; 2357 tval := ibalp_var!-getval bvar; 2358 ibalp_qsat!-backtrack(blevel,varal,val); 2359 temp := ibalp_var!-setq(bvar,1-tval,blevel,cc); 2360 ibalp_var!-setflip(bvar,1); 2361 return temp 2362 end; 2363 2364 2365procedure ibalp_qsat!-analconf(ec,lv,level,clausel,varal); 2366 % Clausel Learning backtracking. [ec] is the conflict clause; [lv] 2367 % is the variable last set; [level] is the current level; [clausel] 2368 % is the list of clauses; [varal] is the A-List of 2369 % variables. Returns a pair. The first entry is the new list of 2370 % clauses. The second entry is a pair of conflict variable and the 2371 % conflict-level. 2372 begin scalar cl,cc,cv; 2373 if eqn(level,0) then return (clausel . (nil . -1)); 2374 cc := ibalp_qsat!-calccc(varal,ec,lv); 2375 if null cc then 2376 return (clausel . (nil . -1)) 2377 else << 2378 cv := ibalp_qsat!-calccvar cc; 2379 cl := ibalp_qsat!-getbtlevel(cc,level); 2380 clausel := cc . clausel; 2381 return (clausel . (cv . cl)) 2382 >> 2383 end; 2384 2385procedure ibalp_qsat!-mom(varal,clausel); 2386 % Get a variable following the original MOM-strategy. [varal] is 2387 % the A-List of variables; [clausel] is the list of 2388 % clauses. Returns a variable. 2389 begin scalar min,tv,h,qlevel,tmom; 2390 min := ibalp_minclnr clausel; 2391 qlevel := ibalp_qsat!-qlevel varal; 2392 tmom := -1; 2393 for each v in varal do 2394 if eqn(ibalp_var!-getqlevel cdr v,qlevel) 2395 and null ibalp_var!-getval cdr v 2396 and ibalp_var!-getquant cdr v then 2397 if (h := ibalp_qsat!-calcmom(cdr v,min)) > tmom then << 2398 tmom := h; 2399 tv := cdr v 2400 >>; 2401 return tv 2402 end; 2403 2404procedure ibalp_qsat!-calcmom(var,min); 2405 % Calculate the mom value of a variable. [var] is a variable; [min] 2406 % is the size of minimal clause. Returns the mom value. 2407 begin integer minpos,minneg; 2408 for each clause in ibalp_var!-getposocc var do 2409 if null clause and eqn(ibalp_clause!-getactpos clause + 2410 ibalp_clause!-getactneg clause,min) then 2411 minpos := minpos + 1; 2412 for each clause in ibalp_var!-getnegocc var do 2413 if null clause and eqn(ibalp_clause!-getactpos clause + 2414 ibalp_clause!-getactneg clause,min) then 2415 minneg := minneg + 1; 2416 return (minpos + minneg)*64 + (minpos * minneg) 2417 end; 2418 2419procedure ibalp_qsat!-qlevel(varal); 2420 % Return the current quantification level. [varal] is the A-List of 2421 % variables. Returns the current quantification level. 2422 if null ibalp_var!-getval cdar varal then 2423 ibalp_var!-getqlevel cdar varal 2424 else 2425 ibalp_qsat!-qlevel cdr varal; 2426 2427procedure ibalp_qsat!-hassimple(clausel); 2428 % Check if a clause list has some literals to simplify. [clausel] 2429 % is the list of clauses. Returns a clause to simplfy or [nil]. 2430 begin scalar ret,tl,tv; 2431 tl := clausel; 2432 while tl and null ret do << 2433 if eqn(length ibalp_clause!-getposlit car tl + 2434 length ibalp_clause!-getneglit car tl,1) then << 2435 tv := if null ibalp_clause!-getposlit car tl then 2436 car ibalp_clause!-getneglit car tl 2437 else 2438 car ibalp_clause!-getposlit car tl; 2439 if ibalp_var!-isex tv and ibalp_var!-getreas tv then 2440 ret := car tl 2441 if ibalp_var!-isex tv and ibalp_var!-getreas tv then 2442 ret := car tl; 2443 >>; 2444 tl := cdr tl; 2445 >>; 2446 return ret 2447 end; 2448 2449procedure ibalp_qsat!-abort(clausel); 2450 % Checks for contradictions after simplification. [clausel] is the 2451 % list of clauses. Return [t] if there is a contradiction, [nil] 2452 % else. 2453 if null clausel then nil else 2454 if null ibalp_clause!-getposlit car clausel 2455 and null ibalp_clause!-getneglit car clausel then t 2456 else 2457 ibalp_qsat!-abort cdr clausel; 2458 2459procedure ibalp_qsat!-calccvar(clause); 2460 % Calculate the conflict variable of a new learnt clause. [clause] 2461 % is the new learnt clause. Returns the conflict variable. 2462 begin scalar tl,tv,cv,level; 2463 level := -1; 2464 tl := ibalp_clause!-getposlit clause; 2465 while tl do << 2466 tv := car tl; 2467 if ibalp_var!-isex tv and ibalp_var!-getlev tv > level then << 2468 level := ibalp_var!-getlev tv; 2469 cv := tv 2470 >>; 2471 tl := cdr tl 2472 >>; 2473 tl := ibalp_clause!-getneglit clause; 2474 while tl do << 2475 tv := car tl; 2476 if ibalp_var!-isex tv and ibalp_var!-getlev tv > level then << 2477 level := ibalp_var!-getlev tv; 2478 cv := tv 2479 >>; 2480 tl := cdr tl 2481 >>; 2482 return cv 2483 end; 2484 2485procedure ibalp_qsat!-getbtlevel(clause,oldlev); 2486 % Calculate the backtrack level after a conflict case. [clause] is 2487 % the new learnt clause; [oldlev] is the old level; Returns the 2488 % backtrack level. 2489 begin scalar tl,tv,level,tlevel; 2490 level := -1; 2491 tl := ibalp_clause!-getposlit clause; 2492 tlevel := ibalp_var!-getlev ibalp_qsat!-calccvar clause; 2493 while tl do << 2494 tv := car tl; 2495 if ibalp_var!-isex tv and 2496 ibalp_var!-getlev tv > level and ibalp_var!-getlev tv < tlevel then 2497 level := ibalp_var!-getlev tv; 2498 tl := cdr tl 2499 >>; 2500 tl := ibalp_clause!-getneglit clause; 2501 while tl do << 2502 tv := car tl; 2503 if ibalp_var!-isex tv and 2504 ibalp_var!-getlev tv > level and ibalp_var!-getlev tv < tlevel then 2505 level := ibalp_var!-getlev tv; 2506 tl := cdr tl 2507 >>; 2508 return if eqn(level,-1) then oldlev - 1 else level 2509 end; 2510 2511procedure ibalp_qsat!-calccc(varal,ec,lv); 2512 % Calculate conflict clause after Strategy: First UIP. [varal] is a 2513 % A-List of variables; [ec] is the empty clause to start the 2514 % calculation with [lv] is the last variable set. Returns the new 2515 % generated clause or nil if there is a sudden death. 2516 begin scalar newclause,tv,reas,doit,res; 2517 newclause := ibalp_clause!-new(); 2518 res := t; 2519 ibalp_resolve(newclause,ec,ibalp_var!-getreas lv,lv); 2520 doit := ibalp_qsat!-doresolve(newclause,varal); 2521 if cdr doit then return nil; 2522 while car doit and res do << 2523 tv := ibalp_qsat!-getresvar newclause; 2524 if eqn(ibalp_var!-getval tv,0) then 2525 ibalp_dellit(tv,newclause,t) 2526 else 2527 ibalp_dellit(tv,newclause,nil); 2528 reas := ibalp_var!-getreas tv; 2529 if ibalp_clausetest(reas,newclause) then res := nil; 2530 if not (null ibalp_clause!-getcount reas) then 2531 ibalp_clause!-setcount(reas,ibalp_clause!-getcount reas + 1); 2532 ibalp_resolve(newclause,newclause,reas,tv); 2533 doit := ibalp_qsat!-doresolve(newclause,varal); 2534 if cdr doit then res := nil 2535 >>; 2536 ibalp_clause!-setcount(newclause,1); 2537 return if res then newclause else nil; 2538 end; 2539 2540procedure ibalp_clausetest(clause1,clause2); 2541 % Tests if two clauses have the same literal. [clause1] is a 2542 % clause; [clause2] is a clause. Returns [t] or [nil]. 2543 ibalp_clause!-getposlit clause1 equal ibalp_clause!-getposlit clause2 2544 and ibalp_clause!-getneglit clause1 equal 2545 ibalp_clause!-getneglit clause2; 2546 2547procedure ibalp_qsat!-doresolve(newclause,varal); 2548 % Test the stopping criterion for resolving. [newclause] is a 2549 % clause; [varal] is the A-List of variables. Returns a pair. The 2550 % first entry is the result of the test, the second is a flag for a 2551 % sudden death. 2552 begin scalar hl,cl,hv,decv,ac1,ac2; 2553 hl := -2; 2554 for each v in ibalp_clause!-getposlit newclause do << 2555 if ibalp_var!-isex v then << 2556 ac1 := t; 2557 if ibalp_var!-getlev v > hl then << 2558 hl := ibalp_var!-getlev v; 2559 hv := v; 2560 cl := 1 2561 >> else if eqn(ibalp_var!-getlev v,hl) then 2562 cl := cl + 1; 2563 if ibalp_var!-getlev v > 0 then ac2 := t 2564 >> 2565 >>; 2566 for each v in ibalp_clause!-getneglit newclause do << 2567 if ibalp_var!-isex v then << 2568 ac1 := t; 2569 if ibalp_var!-getlev v > hl then << 2570 hl := ibalp_var!-getlev v; 2571 hv := v; 2572 cl := 1 2573 >> else if eqn(ibalp_var!-getlev v,hl) then 2574 cl := cl + 1; 2575 if ibalp_var!-getlev v > 0 then ac2 := t 2576 >> 2577 >>; 2578 if null ac1 or null ac2 then return (nil . t); 2579 if cl > 1 then return (t . nil); 2580 decv := ibalp_qsat!-searchdec(hl,varal); 2581 if not (ibalp_var!-isex decv) then return (t . nil); 2582 return ibalp_qsat!-unicheck(newclause,hv) 2583 end; 2584 2585procedure ibalp_qsat!-searchdec(level,varal); 2586 % Search a decision variable at a certain level. [level] is the 2587 % level; [varal] is the A-List of variables. 2588 if null varal then nil else 2589 if eqn(ibalp_var!-getlev cdar varal,level) and 2590 null ibalp_var!-getreas cdar varal then 2591 cdar varal 2592 else 2593 ibalp_qsat!-searchdec(level,cdr varal); 2594 2595procedure ibalp_qsat!-unicheck(clause,var); 2596 % Checks the third condition of the stopping criterion. [clause] is 2597 % a clause; [var] is a single variable. Returns a pair. The first 2598 % entry indicates the result of the check. 2599 begin scalar tl,res,tv,ql,dl; 2600 ql := ibalp_var!-getqlevel var; 2601 dl := ibalp_var!-getlev var; 2602 tl := ibalp_clause!-getposlit clause; 2603 while tl and null res do << 2604 tv := car tl; 2605 if ibalp_var!-isuni tv and 2606 ibalp_var!-getqlevel tv < ql then 2607 if not (eqn(ibalp_var!-getval tv,0) and 2608 ibalp_var!-getlev tv < dl) then 2609 res := t; 2610 tl := cdr tl; 2611 >>; 2612 tl := ibalp_clause!-getneglit clause; 2613 while tl and null res do << 2614 tv := car tl; 2615 if ibalp_var!-isuni tv and 2616 ibalp_var!-getqlevel tv < ql then 2617 if not (eqn(ibalp_var!-getval tv,0) and 2618 ibalp_var!-getlev tv < dl) then 2619 res := t; 2620 tl := cdr tl; 2621 >>; 2622 return (res . nil); 2623 end; 2624 2625procedure ibalp_qsat!-getresvar(clause); 2626 % Get the variable for the next resolve. [clause] is a 2627 % clause. Returns a variable. 2628 begin scalar tl,tv,res,lev; 2629 tl := ibalp_clause!-getposlit clause; 2630 lev := -2; 2631 while tl do << 2632 tv := car tl; 2633 if ibalp_var!-getreas tv and ibalp_var!-getlev tv > lev then << 2634 res := tv; 2635 lev := ibalp_var!-getlev tv 2636 >>; 2637 tl := cdr tl; 2638 >>; 2639 tl := ibalp_clause!-getneglit clause; 2640 while tl do << 2641 tv := car tl; 2642 if ibalp_var!-getreas tv and ibalp_var!-getlev tv > lev then << 2643 res := tv; 2644 lev := ibalp_var!-getlev tv 2645 >>; 2646 tl := cdr tl; 2647 >>; 2648 return res 2649 end; 2650 2651procedure ibalp_qsat!-analsatNAIV(varal); 2652 % Naive SAT-driven backtracking. [varal] is the A-List of 2653 % variables. Returns a pair of branching variable and the 2654 % branch-level. 2655 begin scalar cv,cl; 2656 cl := -1; 2657 for each v in varal do << 2658 if ibalp_var!-isuni cdr v and eqn(ibalp_var!-getflip cdr v,0) then 2659 if ibalp_var!-getlev cdr v > cl then << 2660 cl := ibalp_var!-getlev cdr v; 2661 cv := cdr v 2662 >> 2663 >>; 2664 return (cv . cl) 2665 end; 2666 2667procedure ibalp_qsat!-backtrack(level,varal,val); 2668 % Backtrack to a certain level. [level] is the backtrack level; 2669 % [varal] is the A-List of variables; [val] indicates if it is a 2670 % Conflict-driven or a SAT-driven backtracking. 2671 if val then << 2672 for each v in varal do 2673 if ibalp_var!-getlev cdr v > level then << 2674 ibalp_var!-unsetq(cdr v,ibalp_var!-getval cdr v); 2675 ibalp_var!-setflip(cdr v,nil) 2676 >> 2677 >> else << 2678 for each v in varal do 2679 if ibalp_var!-getlev cdr v >= level then << 2680 ibalp_var!-unsetq(cdr v,ibalp_var!-getval cdr v); 2681 ibalp_var!-setflip(cdr v,nil) 2682 >> 2683 >>; 2684 2685procedure ibalp_qsat!-cdclup(clist,level); 2686 % Unitpropagation. [clist] is a list of clauses with unit 2687 % variables; [level] is the level the reduction is made; Returns a 2688 % Pair. The first entry is an empty clause if one is derived the 2689 % second the variable set at last. 2690 begin scalar tl,tv,lv,ec,upl,temp; 2691 tl := clist; 2692 while tl and null ec do << 2693 tv := car tl; 2694 if null ibalp_clause!-getsat cdr tv then << 2695 temp := ibalp_var!-setq(caar tv,cdar tv,level,cdr tv); 2696 upl := car temp; 2697 nconc(tl,upl) 2698 >>; 2699 tl := cdr tl; 2700 lv := caar tv; 2701 ec := cdr temp; 2702 >>; 2703 return (ec. lv) 2704 end; 2705 2706procedure ibalp_qsat!-isunit(clause); 2707 % Check if a clause is a unit clause. [clause] is a clause. Returns 2708 % the unit variable and its assignment of a unit clause or [nil] if 2709 % the clause is not unit. 2710 begin scalar tl,tv,min,te; integer ce; 2711 if ibalp_clause!-getsat clause then return nil; 2712 %dirty hack 2713 min := 10000; 2714 tl := ibalp_clause!-getposlit clause; 2715 while tl and ce < 2 do << 2716 tv := car tl; 2717 if ibalp_var!-isex tv and null ibalp_var!-getval tv then << 2718 ce := ce + 1; 2719 te := (tv . 1) 2720 >>; 2721 if ibalp_var!-isuni tv and null ibalp_var!-getval tv and 2722 ibalp_var!-getqlevel tv < min then min := ibalp_var!-getqlevel tv; 2723 tl := cdr tl 2724 >>; 2725 tl := ibalp_clause!-getneglit clause; 2726 while tl and ce < 2 do << 2727 tv := car tl; 2728 if ibalp_var!-isex tv and null ibalp_var!-getval tv then << 2729 ce := ce + 1; 2730 te := (tv . 0) 2731 >>; 2732 if ibalp_var!-isuni tv and null ibalp_var!-getval tv and 2733 ibalp_var!-getqlevel tv < min then min := ibalp_var!-getqlevel tv; 2734 tl := cdr tl 2735 >>; 2736 return if eqn(ce,1) and ibalp_var!-getqlevel car te < min then 2737 te 2738 else 2739 nil 2740 end; 2741 2742procedure ibalp_qsat!-isec(clause); 2743 % Check if a clause is an empty clause. [clausel] is the list of 2744 % clauses. Returns [t] if the clause is a empty clause, [nil] else. 2745 begin scalar ec,tl,tv; 2746 if ibalp_clause!-getsat clause then return nil; 2747 ec := t; 2748 tl := ibalp_clause!-getposlit clause; 2749 while ec and tl do << 2750 tv := car tl; 2751 if ibalp_var!-isex tv and 2752 not eqn(ibalp_var!-getval tv,0) then ec := nil; 2753 if ibalp_var!-isuni tv and 2754 eqn(ibalp_var!-getval tv,1) then ec := nil; 2755 if null ibalp_var!-getquant tv and null ibalp_var!-getval tv then 2756 ec := nil; 2757 tl := cdr tl 2758 >>; 2759 tl := ibalp_clause!-getneglit clause; 2760 while ec and tl do << 2761 tv := car tl; 2762 if ibalp_var!-isex tv and 2763 not eqn(ibalp_var!-getval tv,1) then ec := nil; 2764 if ibalp_var!-isuni tv and 2765 eqn(ibalp_var!-getval tv,0) then ec := nil; 2766 if null ibalp_var!-getquant tv and null ibalp_var!-getval tv then 2767 ec := nil; 2768 tl := cdr tl 2769 >>; 2770 return ec 2771 end; 2772 2773procedure ibalp_qsat!-csat(clausel); 2774 % Check if the formula is satisfied. [clausel] is the List of 2775 % clauses. Returns [t] if all clauses are satisfied, [nil] else. 2776 ibalp_csat clausel; 2777 2778procedure ibalp_readquantal(formula,varal); 2779 % Read prenex quantifiers of a formula. [formula] is a formula in 2780 % LISP-Prefix, [varal] is the A-List of variables. Reads the 2781 % quantifiers and annotates each quantified variable with its 2782 % quantifier and its quantification level. Returns a pair of the 2783 % highest quantification level and the A-List of the new sorted 2784 % variables. 2785 begin scalar hl,tl; 2786 tl := ibalp_readquantal2(formula,varal,rl_op formula,1,nil); 2787 hl := ibalp_var!-getqlevel cdar tl; 2788 for each v in varal do 2789 if null ibalp_var!-getquant cdr v then 2790 tl := v . tl; 2791 tl := reverse tl; 2792 return (hl . tl) 2793 end; 2794 2795procedure ibalp_readquantal2(formula,varal,quant,level,newvaral); 2796 % Helper function for reading prenex quantifiers of a 2797 % formula. [formula] is a formula in LISP-Prefix, [varal] is the 2798 % A-List of variables, [quant] is the current quantifier, [level] 2799 % is the current quantification level, [varal] is the new A-list of 2800 % variables. Returns a A-List of the new sorted variables. 2801 if rl_quap rl_op formula then << 2802 if not (rl_op formula eq quant) then level := level + 1; 2803 if atsoc(rl_var formula,varal) then << 2804 ibalp_var!-setquant(cdr atsoc(rl_var formula,varal),rl_op formula); 2805 ibalp_var!-setqlevel(cdr atsoc(rl_var formula,varal),level); 2806 newvaral := (ibalp_var!-getid cdr atsoc(rl_var formula,varal) . 2807 cdr atsoc(rl_var formula,varal)) . newvaral 2808 >>; 2809 ibalp_readquantal2(rl_mat formula,varal,rl_op formula,level,newvaral) 2810 >> else 2811 newvaral; 2812 2813%%%%%%%%%%%%%%%%%%%%%%%%%% Parametric QSAT %%%%%%%%%%%%%%%%%%%%%%%%%% 2814 2815procedure ibalp_qsat!-par(fvl,clausel,varal,result,psat); 2816 % The main procedure for parametric Q-SAT. [fvl] is the list of 2817 % currently free variables; [clausel] is the list of clauses; [varal] is the 2818 % A-List of variables; [result] is the current list of 2819 % results; [pqsat] ist the list of free variables. Returns a pair of the 2820 % result and the clauses/variables. 2821 begin scalar tv,res,pair,ec,upl,pair2,ec2; 2822 tv := ibalp_getfree!-dlcs fvl; 2823 if null tv then << 2824 if (not member(ibalp_qsat!-calcbin fvl,donel!*)) then << 2825 upl := ibalp_qsat!-getupl clausel; 2826 res := ibalp_qsat!-cdcl(clausel,varal,upl,nil); 2827 numcdcl!* := numcdcl!* + 1; 2828 donel!* := ibalp_qsat!-calcbin fvl . donel!*; 2829 if car res = {'true} then << 2830 result := (ibalp_exres fvl) . result; 2831 if psat then 2832 result := ibalp_qsat!-localsearch(clausel,varal,length fvl, 2833 fvl,result); 2834 >>; 2835 return (result . (cadr res . cddr res)); 2836 >> else 2837 return (result . (clausel . varal)); 2838 >> else << 2839 ec := ibalp_var!-setq(tv,1,-42,nil); 2840 if null cdr ec then << 2841 pair := ibalp_qsat!-par(fvl,clausel,varal,result,psat); 2842 result := car pair; 2843 clausel := cadr pair; 2844 varal := cddr pair; 2845 ibalp_qsat!-dav varal; 2846 >>; 2847 ibalp_var!-unsetq(tv,1); 2848 ec := ibalp_var!-setq(tv,0,-42,nil); 2849 if null cdr ec then << 2850 pair := ibalp_qsat!-par(fvl,clausel,varal,result,psat); 2851 result := car pair; 2852 clausel := cadr pair; 2853 varal := cddr pair; 2854 ibalp_qsat!-dav varal; 2855 >>; 2856 ibalp_var!-unsetq(tv,0); 2857 return (result . (clausel . varal)) 2858 >> 2859 end; 2860 2861procedure ibalp_qsat!-localsearch(clausel,varal,radius,fvl,result); 2862 % Performs a local search with a given radius. [clausel] is the list of 2863 % clauses; [varal] is the A-List of variables; [radius] is the radius for 2864 % the local search; [fvl] is the list of free variables; [result] ist the 2865 % current result. Returns the new result. 2866 begin scalar v,oldl,varl; 2867 varl := ibalp_qsat!-getlocvars!-last(fvl,radius); 2868 for each v in varl do << 2869 oldl := ibalp_var!-getval v . oldl; 2870 ibalp_var!-unsetq(v,ibalp_var!-getval v); 2871 >>; 2872 result := ibalp_qsat!-localsearchrec(clausel,varal,varl,fvl,result); 2873 for i := 1:length varl do << 2874 v := nth(varl,i); 2875 if eqn(nth(oldl,(length oldl) - i + 1),0) then 2876 ibalp_var!-setq(v,0,-42,nil) 2877 else 2878 ibalp_var!-setq(v,1,-42,nil) 2879 >>; 2880 return result 2881 end; 2882 2883procedure ibalp_qsat!-getlocvars!-last(fvl,number); 2884 % Get the [number] last free variables for local search. 2885 begin scalar l,varl; 2886 l := length fvl; 2887 for i := l-number+1:l do 2888 varl := nth(fvl,i) . varl; 2889 return varl 2890 end; 2891 2892procedure ibalp_qsat!-getlocvars!-rand(fvl,number); 2893 % Get [number] random free variables for local search. 2894 begin scalar v,r,varl; 2895 while not eqn(length varl,number) do << 2896 r := random length fvl; 2897 v := nth(fvl,r+1); 2898 if (not memq(v,varl)) then 2899 varl := v . varl 2900 >>; 2901 return varl 2902 end; 2903 2904procedure ibalp_qsat!-localsearchrec(clausel,varal,selvars,fvl,result); 2905 % Recursive helper function of the local search. 2906 begin scalar tv,res,pair,ec,upl,pair2; 2907 tv := ibalp_getfree selvars; 2908 if null tv then << 2909 if ibalp_csat clausel and 2910 not member(ibalp_qsat!-calcbin fvl,donel!*) then << 2911 donel!* := ibalp_qsat!-calcbin fvl . donel!*; 2912 numlocs!* := numlocs!* + 1; 2913 result := (ibalp_exres fvl) . result; 2914 >> 2915 >> else << 2916 ec := ibalp_var!-setq(tv,1,-42,nil); 2917 if null cdr ec then 2918 result := ibalp_qsat!-localsearchrec(clausel,varal,selvars, 2919 fvl,result); 2920 ibalp_var!-unsetq(tv,1); 2921 ec := ibalp_var!-setq(tv,0,-42,nil); 2922 if null cdr ec then 2923 result := ibalp_qsat!-localsearchrec(clausel,varal,selvars, 2924 fvl,result); 2925 ibalp_var!-unsetq(tv,0) 2926 >>; 2927 return result 2928 end; 2929 2930procedure ibalp_qsat!-calcbin(fvl); 2931 % Calculate a binary representation of the current assignment to the free 2932 % variables in [fvl]. 2933 if null fvl then 0 else 2934 ibalp_var!-getval car fvl * 2^(length fvl -1) + 2935 ibalp_qsat!-calcbin(cdr fvl); 2936 2937procedure ibalp_printvars(fvl); 2938 % Helper function to print the list of variables. 2939 for each v in fvl do 2940 ioto_tprin2t {ibalp_var!-getid v, " ", ibalp_var!-getval v}; 2941 2942procedure ibalp_qsat!-getupl(clausel); 2943 % Get a initial set of unit clauses. [clausel] is the list of 2944 % clauses. Return a list of unit clauses. 2945 begin scalar upl,h; 2946 for each clause in clausel do 2947 if (h := ibalp_qsat!-isunit clause) then 2948 upl := (h . clause) . upl; 2949 return upl 2950 end; 2951 2952procedure ibalp_exres2(resultl,fvl); 2953 % Expand the result. [resultl] is the list of results; [fvl] is the 2954 % list of free variables. Returns the complete result in lisp 2955 % prefix. 2956 begin scalar l,tl; 2957 l := length fvl; 2958 if eqn(length resultl,0) then return {'false}; 2959 if eqn(length resultl,1) then return car resultl; 2960 if eqn(length resultl,2^l) then return {'true}; 2961 for each res in resultl do << 2962 tl := res . tl 2963 >>; 2964 tl := 'or . tl; 2965 return tl 2966 end; 2967 2968procedure ibalp_exres(vl); 2969 % Expand result. Expand a single result into Lisp Prefix. [vl] is a 2970 % list of variables. Return the expanded result. 2971 begin scalar tl,var,res; 2972 for each v in vl do << 2973 var := {'equal,ibalp_var!-getid v,ibalp_var!-getval v}; 2974 tl := var . tl; 2975 >>; 2976 if length tl > 1 then << 2977 for each v in tl do 2978 res := v . res; 2979 res := 'and . res 2980 >> else 2981 res := car tl; 2982 return res 2983 end; 2984 2985procedure ibalp_getfree(list); 2986 % Get an unassigned variable. [list] is the list of free 2987 % varibles. Returns a varialbe or [nil] if there is no unassigned. 2988 if null list then nil else 2989 if null ibalp_var!-getval car list then 2990 car list 2991 else 2992 ibalp_getfree cdr list; 2993 2994procedure ibalp_getfree!-dlcs(list); 2995 % Get an unassigned variable. [list] is the list of free 2996 % varibles (following the DLCS strategy). Returns a varialbe 2997 % or [nil] if there is no unassigned. 2998 begin scalar tv,max; 2999 tv := ibalp_getfree list; 3000 if null tv then return nil; 3001 max := ibalp_var!-getnumneg tv + ibalp_var!-getnumpos tv; 3002 for each var in list do 3003 if null ibalp_var!-getval var then 3004 if ibalp_var!-getnumneg var + 3005 ibalp_var!-getnumpos var > max then << 3006 tv := var; 3007 max := ibalp_var!-getnumneg var + ibalp_var!-getnumpos var 3008 >>; 3009 return tv; 3010 end; 3011 3012procedure ibalp_psatp(varal); 3013 % Returns whether a problem is PSAT. 3014 %if null varal then 3015 % t 3016 %else 3017 % ibalp_var!-isex cdar varal and ibalp_psatp cdr varal; 3018 begin scalar ret; 3019 ret := t; 3020 for each v in varal do << 3021 if ibalp_var!-isuni cdr v then 3022 ret := nil; 3023 >>; 3024 return ret; 3025 end; 3026 3027procedure ibalp_splitvars(pqsat,varal); 3028 % Split variables. [pqsat] is the list of free variables; [varal] 3029 % is the A-List of variables. Deletes all the free variables from 3030 % the variable list and returns the two lists of bound and free 3031 % variables. 3032 begin scalar fvl,tv; 3033 for each v in pqsat do << 3034 tv := cdr atsoc(v,varal); 3035 fvl := tv . fvl; 3036 varal := delete((v . tv),varal) 3037 >>; 3038 return (varal . fvl) 3039 end; 3040 3041procedure ibalp_qsat!-dav(varal); 3042 % Delete all assignments to variables. [varal] is the A-List of 3043 % variables; [clausel] is the list of clauses. 3044 for each v in varal do << 3045 if ibalp_var!-getval cdr v then 3046 ibalp_var!-unsetq(cdr v,ibalp_var!-getval cdr v); 3047 ibalp_var!-setflip(cdr v,nil) 3048 >>; 3049 3050endmodule; % ibalpqsat 3051 3052end; % of file 3053