# generated by 'lingeling --pcs-reduced' # version azf 4e2098eff08059de6eb4e49deb1c4b14db949fc0 acts {0,1,2}[2] # activity based reduction: 0=no,1=enable,2=dyn agile {0,1,2}[1] # agility based restart skipping, 1=std, 2=sinus bate {0,1}[1] # basic ATE removal during probing batewait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) bca {0,1,2}[1] # enable blocked clause addition (1=week,2=strong) bcawait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) bva {0,1}[0] # enable bounded variable addition (BVA) bias {-1,0,1,2}[2] # decision order initial bias (0=no,2=cw) blklarge {0,1}[1] # BCE of large clauses blkrtc {0,1}[0] # run BCE until completion blksched2b2 {0,1}[0] # BCE schedule 2x2 first blkschedmin {0,1}[0] # BCE schedule based on minimum of occurrences blkschedprod {0,1}[0] # BCE schedule based on product too blkschedpure {0,1}[1] # BCE schedule pure literals first blkschedsum {0,1}[1] # BCE schedule based on sum of occurrences too blksmall {0,1}[1] # BCE of small clauses block {0,1}[1] # blocked clause elimination (BCE) blockwait {0,1}[1] # wait for BVE boost {0,1}[1] # enable boosting of preprocessors bumpbcplits {0,1}[0] # bump unseen but propagated literals bumpclslits {0,1}[0] # bump literals in minimized clause bumpseenaftermin {0,1}[0] # bump seen after minimization bumpseenbeforemin {0,1}[1] # bump seen before minimization bumpseenlits {0,1}[1] # bump seen literals card {0,1}[1] # cardinality constraint reasoning cardcut {0,1,2}[2] # 1=gomoroy-cuts,2=strengthen cardignused {0,1}[0] # ignored already used literals in extraction carduse {0,1,2,3}[2] # use clauses (1=oneside,2=bothsidetoo,3=anyside) cardwait {0,1,2}[0] # wait for BCE (1) and/or BVE (2) cce {0,1,2,3}[3] # covered clause elimination (1=ate,2=abce,3=acce) cceonlyifstuck {0,1}[0] # ABCE+ACCE only if elm+blk stuck ccertc {0,1}[0] # run CCE until completition ccewait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) cgrclsr {0,1}[1] # gate extraction and congruence closure cgrclsrwait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) cgrextand {0,1}[1] # extract and gates cgrexteq {0,1}[1] # extract equivalences cgrextite {0,1}[1] # extract ite gates cgrextunits {0,1}[1] # extract units cgrextxor {0,1}[1] # extract xor gates cintincdiv {0,1,2,3}[1] # cintinc reduce policy: 0=no,1=div1,2=div2,3=heur cliff {0,1}[1] # cliffing cliffwait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) compact {0,1,2}[0] # compactify after 'lglsat/lglsimp' (1=UNS,2=SAT) deco {0,1,2}[1] # learn decision-only clauses too (2=all-decisions) decompose {0,1}[1] # enable decompose elim {0,1}[1] # bounded variable eliminiation (BVE) elmblk {0,1}[1] # enable BCE during BVE elmblkwait {0,1}[1] # wait for BVE to be completed once elmfull {0,1}[0] # no elimination limits elmrtc {0,1}[0] # run BVE until completion elmsched2b2 {0,1}[0] # BVE schedule 2x2 first elmschediff {0,1}[0] # BVE schedule based on diff of occurrences too elmschedmin {0,1}[0] # BVE schedule based on minimum of occurrences elmschedprod {0,1}[0] # BVE schedule based on product too elmschedpure {0,1}[1] # BVE schedule pure literals first elmschedsum {0,1}[1] # BVE schedule based on sum of occurrences too factor {0,1,2,3}[3] # {cls,occ}lim factors (0=const1,1=ld,2=lin,3=sqr) flipping {0,1}[1] # enable point flipping fliptop {0,1}[1] # flipping only at the top level gauss {0,1}[1] # enable gaussian elimination gaussexptrn {0,1}[1] # export trn cls from gaussian elimination gaussextrall {0,1}[1] # extract all xors (with duplicates) gausswait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) gluescale {1,2,3,4}[4] # glue scaling: 1=linear,2=sqrt,3=ld,4=hybrid import {0,1}[1] # import external indices and map them incsavevisits {0,1}[0] # incremental start new visits counter inprocessing {0,1}[1] # enable inprocessing irrlim {0,1}[1] # use irredundant clauses as limit for simps jwhred {0,1}[1] # compute JWH score based on redundant clauses too keepmaxglue {0,1}[1] # keep maximum glue clauses lhbr {0,1}[1] # enable lazy hyber binary reasoning lift {0,1}[1] # enable double lookahead lifting liftwait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) lkhd {-1,0,1,2,3}[2] # -1=LOCS,0=LIS,1=JWH,2=TREELOOK,3=LENSUM lkhdmisifelmrtc {0,1}[0] # MIS if elimination ran to completion locsdec {0,1,2}[2] # bump 1=mostflipped 2=minlits locset {0,1,2}[2] # initialize local search phases (1=prev,2=cur) locsexport {0,1}[1] # export phases from local search locsred {0,1,2,3,4}[0] # apply local search on redundant clauses too locsrtc {0,1}[0] # run local search until completion locswait {0,1,2}[2] # wait for BCE(1) and/or BVE(2) mega {0,1}[0] # mega probing through preprocessor look-ahead megawait {0,1,2}[2] # mega probing waiting for BCE / BVE minimize {0,1,2}[2] # minimize learned clauses (1=local,2=recursive) move {0,1,2}[2] # move redundant cls (1=only-binary,2=ternary) otfs {0,1}[1] # enable on-the-fly subsumption otfsbump {0,1,2}[0] # bump literals during OTFS (1=conflict,2=drive) otfsconf {0,1}[0] # count on-the-fly restart as conflict phase {-1,0,1}[0] # default phase (-1=neg,0=JeroslowWang,1=pos) phaseflip {0,1}[0] # flip Jeroslow Wang phase plain {0,1}[0] # plain mode disables all preprocessing prbasic {0,1,2}[1] # enable basic probing procedure (1=roots-only) prbasicrtc {0,1}[0] # run basic probing until completion prbrtc {0,1}[0] # run all probing until completion prbsimple {0,1,2,3}[2] # simple probing (1=shallow,2=deep,3=touchall) prbsimpleliftdepth {1,2,3,4}[2] # simple probing lifting depth prbsimplertc {0,1}[0] # run simple probing until completion probe {0,1}[1] # enable probing psm {0,1,2,3}[3] # use PSM metric (1=afteract,2=afterglue,3=first pure {0,1}[1] # enable pure literal elimination during BCE randec {0,1}[0] # enable random decisions rdp {0,1,2,3}[0] # random DP (2=redbin,3=redtrn rdpmodelm {0,1}[0] # use model elimination in RDP rdpwait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) redfixed {0,1}[0] # keep a fixed size of learned clauses redlbound {0,1}[0] # relative and absolute bounds on learned clauses reduce {0,1,2,3,4}[2] # clause reduction (1=noouter,2=luby,3=inout,4=arith) rephase {0,1,2}[1] # enable flushing and recomputation of phases (2=full) restart {0,1,2,3}[2] # enable restarting (0=no,1=fixed,2=luby,3=inout) restartintscale {-1,0,1}[0] # scale restart interval reusetrail {0,1}[1] # reuse trail score {0,1,2,3,4,5,6}[5] # 0=static,1=inc,2=vmtf,3=sum,4=avg,5=evsids,6=vsids256 simplify {0,1,2}[2] # enable simplification smallve {0,1}[1] # enable small number variables elimination smallvevars {4,5,6,7,8,9,10}[10] # variables small variable elimination smallvewait {0,1}[0] # wait with small variable elimination sortlits {0,1}[0] # sort lits of cls during garbage collection synclsall {0,1}[1] # always synchronize all unconsumed clauses tabr {0,1,2,3,4}[3] # tabula rasa (1=red,2=phases,3=cinc,4=scores tabrkeep {1,2,3,4}[3] # 1=none,2=bin,3=bin+trn,4=bin+trn+glue0 ternres {0,1}[1] # generate ternary resolvents ternresrtc {0,1}[0] # run ternary resolvents until completion ternreswait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) transred {0,1}[1] # enable transitive reduction transredwait {0,1,2}[2] # wait for BCE (1) and/or BVE (2) treelook {0,1,2}[1] # enable tree-based look-ahead (2=scheduleprobing) treelookfull {0,1}[0] # do not limit tree-based look-head treelooklrg {0,1}[1] # use large clauses during tree-look treelookrtc {0,1}[0] # run tree-based look-ahead until completion trep {0,1}[0] # enable time based interval reporting unhdatrn {0,1,2}[2] # unhide redundant ternary clauses (1=move,2=force) unhdextstamp {0,1}[1] # used extended stamping features unhdhbr {0,1}[0] # enable unhiding hyper binary resolution unhide {0,1}[1] # enable unhiding unhidewait {0,1,2}[0] # wait for BCE (1) and/or BVE (2) wait {0,1}[1] # enable or disable all waiting