u      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyzCreturn immediate dominators for each node of a graph, given a root {Creturn the set of dominators of the nodes of a graph, given a root |}~z{z{ 1A type class for monads that are able to perform  actions.      SSTErrMonad e st s a: the error type e , state type st, ST thread  s and result type a. This is a monad embedding ST) and supporting error handling and state + threading. It uses CPS to avoid checking  and  for every  ; instead only checks on . Idea adapted from   1http://haskell.org/haskellwiki/Performance/Monads.  Perform an ST action in the DPLL monad. runSSTErrMonad m s executes a   action with initial state s 0 until an error occurs or a result is returned.    8@Each pair of watched literals is paired with its clause and id. *The VSIDS-like dynamic variable ordering. Immutable version. A  level array; maintains a record of the decision level of each variable  in the solver. If level is such an array, then level[i] == j means the  decision level for var number i is j. j must be non-negative when  the level is defined, and noLevel otherwise. #Whenever an assignment of variable v is made at decision level i,   level[unVar v] is set to i.  ?An instance of this class is able to answer the question, Is a  truth-functional object x true under the model m ? Or is m a model  for x7? There are three possible answers for this question:  (''the  object is true under m''),  (''the object is false under m''), K and undefined, meaning its status is uncertain or unknown (as is the case  with a partial assignment). LThe only method in this class is so named so it reads well when used infix.  Also see:  isTrueUnder,  isFalseUnder,  isUndefUnder. !x `!` m should use Right if the status of x is  defined, and Left otherwise. "JAnnotate each variable in the conflict graph with literal (indicating its M assignment) and decision level. The only reason we make a new datatype for  this is for its  instance. #$HThe union of the reason side and the conflict side are all the nodes in  the )6 (excepting, perhaps, the nodes on the reason side at G decision level 0, which should never be present in a learned clause). %&:The reason side contains at least the decision variables. '4The conflict side contains the conflicting literal. ()*#Mutable array corresponding to the + representation. +An ''immutable assignment''.. Stores the current assignment according to & the following convention. A literal L i is in the assignment if in  location (abs i) in the array, i is present. Literal L i is absent  if in location (abs i)- there is 0. It is an error if the location (abs  i) is any value other than 0 or i or negate i. Note that the   instance for 6 and + takes constant G time to execute because of this representation for assignments. Also J updating an assignment with newly-assigned literals takes constant time, , and can be done destructively, but safely. ,Represents a container of type t storing elements of type a that . support membership, insertion, and deletion. LThere are various data structures used in funsat which are essentially used  as  ''set-like'' objects. I'(ve distilled their interface into three K methods. These methods are used extensively in the implementation of the  solver. --The set-like object with an element removed. ..The set-like object with an element included. /8Whether the set-like object contains a certain element. 0123456789:;<=DThe polarity of the literal. Negative literals are false; positive 0 literals are true. The 0-literal is an error. >$The variable for the given literal. ?Same as freeze$, but at the right type so GHC doesn't yell at me. @See ?. ABC<Destructively update the assignment with the given literal. D8Destructively undo the assignment to the given literal. E-The assignment as a list of signed literals. 8 !"#$%&'()*+,-./0123456789:;<=>?@ABCDE89:;678<=>501234,-./+*?@ABCDE$%&'()"# !8 !!"##$%&'()%&'()*+,-./-./0123412345678789:;:;<=>?@ABCDE6 if and only if the object is undefined in the model. 1 if and only if the object is true in the model. 2 if and only if the object is false in the model. IWhether all the elements of the model in the list are false but one, and  none is true, under the model. GGet the element of the list which is not false under the model. If no  such element, throws an error. O(1)+ Whether a list contains a single element. !Modify a value inside the state. modifyArray arr i f applies the function f to the index i and the % current value of the array at index i, then writes the result into i in  the array. Same as newArray&, but helping along the type checker. ECount the number of elements in the list that satisfy the predicate. O(1)  argmin f x y, is the argument whose image is least under f; if * the images are equal, returns the first.  O(length xs) argminimum f xs returns the value in xs whose image  is least under f; if xs is empty, throws an error. HShow the value with trace, then return it. Useful because you can wrap < it around any subexpression to print it when it is forced. JReturns a predicate which holds exactly when both of the given predicates  hold. EGenerate a cut using the given UIP node. The cut generated contains L exactly the (transitively) implied nodes starting with (but not including) H the UIP on the conflict side, with the rest of the nodes on the reason  side. decision literals conflict graph %unassigned, implied conflicting node a UIP in the conflict graph JGenerate a learned clause from a cut of the graph. Returns a pair of the > learned clause and the decision level to which to backtrack. JCreates the conflict graph, where each node is labeled by its literal and  level. 9Useful for getting pretty graphviz output of a conflict. $decision lits, in rev. chron. order conflict info F$Unsatisfiable cores are not unique. GCA type indicating an error in the checking process. Assuming this  checker'Ds code is correct, such an error indicates a bug in the SAT solver. H?Indicates that the clause id is referenced but has no entry in  S. I-Indicates that the clause id has an entry in S but  no resolution sources. J@Indicates that the variable has no antecedent mapping, in which ( case it should never have been assigned/encountered in the first  place. KBIndicates that in the clause-lit pair, the unit literal of clause 2 is the literal, but it ought to be the variable. L@Indicates that the constructed antecedent clause not unit under  R. MBIndicates that the clauses do not have complementary variables or A have too many. The complementary variables (if any) are in the  list. N:Indicates that the clauses do not properly resolve on the  variable. OPQ?The id of the last, conflicting clause in the solving process. RFinal assignment.  Precondition1: All variables assigned at decision level zero. S Invariant5: Each id has at least one source (otherwise that id " should not even have a mapping).  Invariant9: Should be ordered topologically backward (?) from each G conflict clause. (IOW, record each clause id as its encountered when " generating the conflict clause.) T+Original clauses of the CNF input formula. UWThe depth-first method. IResolve both clauses on the given variable, and throw a resolution error J if anything is amiss. Specifically, it checks that there is exactly one M occurrence of a literal with the given variable (if variable given) in each + clause and they are opposite in polarity. EIf no variable specified, finds resolving variable, and ensures there's  only one such variable. HGet the antecedent (reason) for a variable. Every variable encountered  ought to have a reason. FGHIJKLMNOPQRSTUVWWOPQRSTUVGNMLKJIHFFGNMLKJIHHIJKLMNOPQRSTUPQRSTUWTX+The show instance uses the wrapped string. YZ[\](Number of conflicts since last restart. ^0Number of conflicts since beginning of solving. _DNumber of learned clauses currently in DB (fluctuates because DB is  compacted every restart). `+Avg. number of literals per learnt clause. a6Total number of decisions since beginning of solving. b>Total number of unit implications since beginning of solving. cd6Indicates an error in the resultion checking process. e7Indicates a unsatisfactory assignment that was claimed < satisfactory. Each clause is tagged with its status using    .statusUnder. .Our star monad, the DPLL State monad. We use ST for mutable arrays and E references, when necessary. Most of the state, however, is kept in   and is not mutable.  The problem. 4The decision level (last decided literal on front). Invariant: if l maps to  ((x, y), c), then x == l || y == l. Same invariant as %, but only contains learned conflict  clauses. ;A FIFO queue of literals to propagate. This should not be  manipulated directly; see  and . =Chronological trail of assignments, last-assignment-at-head. EFor each variable, the clause that (was unit and) implied its value. CThe number of conflicts that have occurred since the last restart. The total number of conflicts. The total number of decisions. 1The total number of implications (propagations). fFThe solution to a SAT problem. In each case we return an assignment, ! which is obviously right in the h case; in the g case, the reason : is to assist in the generation of an unsatisfiable core. ghi)Configuration parameters for the solver. jk&Number of conflicts before a restart. lk is altered after each * restart by multiplying it by this value. m(If true, use dynamic variable ordering. noDRun the DPLL-based SAT solver on the given CNF instance. Returns a K solution, along with internal solver statistics and possibly a resolution . trace. The trace is for checking a proof of g, and thus is only  present when the result is g. p%Solve with the default configuration q. This function applies # recursively until SAT instance is M solved, starting with the given initial assignment. It also implements the  conflict-based restarting (see i). q7A default configuration based on the formula to solve.  restarts every 100 conflicts E requires 1.5 as many restarts after restarting as before, each time  VSIDS to be enabled  restarts to be enabled Some kind of preprocessing.  remove duplicates FSimplify the clause database. Eventually should supersede, probably,  .  Precondition: decision level 0. BThe DPLL procedure is modeled as a state transition system. This M function takes one step in that transition system. Given an unsatisfactory L assignment, perform one state transition, producing a new assignment and a  new state.  Precondition:! problem determined to be unsat. JRecords id of conflicting clause in trace before failing. Always returns  . )Check data structure invariants. Unless -fno-ignore-asserts is passed, + this should be optimised away to nothing.  Value of the 2 array if corresponding variable unassigned. Had  better be less that 0. JAssign a new literal, and enqueue any implied assignments. If a conflict  is detected, return $Just (impliedLit, conflictingClause) ; otherwise  return Nothing. The  impliedLit) is implied by the clause, but conflicts  with the assignment. HIf no new clauses are unit (i.e. no implied assignments), simply update  watched literals. (Assigned literal which might propagate. 2Boolean constraint propagation of all literals in . If a conflict 2 is found it is returned exactly as described for . (Find and return a decision variable. A decision variable must be (1) H undefined under the assignment and (2) it or its negation occur in the  formula. HSelect a decision variable, if possible, and return it and the adjusted  . GAssign given decision variable. Records the current assignment before < deciding on the decision variable indexing the assignment. HNon-chronological backtracking. The current returns the learned clause J implied by the first unique implication point cut of the conflict graph. (l, c), where attempting to assign l conflicted with  clause c. doWhile cmd test first runs cmd, then loops testing test and  executing cmd. The traditional do-while semantics, in other words. GAnalyse a the conflict graph and produce a learned clause. We use the & First UIP cut of the conflict graph. EMay undo part of the trail, but not past the current decision level. &learned clause and new decision level GDelete the assignment to last-assigned literal. Undoes the trail, the  assignment, sets , undoes reason. Does not touch . 2Increase the recorded activity of given variable. 'Constant amount by which a variable is ed. O(1). Test for unsatisfiability. The DPLL paper says, ''5A problem is unsatisfiable if there is a conflicting . clause and there are no decision literals in m.'' But we were deciding J on all literals *without* creating a conflicting clause. So now we also  test whether we'%ve made all possible decisions, too. .Keep the smaller half of the learned clauses. IAdd clause to the watcher lists, unless clause is a singleton; if clause  is a singleton, s fact and returns  if fact is in conflict,  E otherwise. This function should be called exactly once per clause, H per run. It should not be called to reconstruct the watcher list when  propagating. ACurrently the watched literals in each clause are the first two. &Also adds unique clause ids to trace. Is this clause learned? Enqueue literal in the ) and place it in the current assignment. 8 If this conflicts with an existing assignment, returns False ; otherwise  returns True2. In case there is a conflict, the assignment is not  altered. DAlso records decision level, modifies trail, and records reason for  assignment. )The literal that has been assigned true. 3The reason for enqueuing the literal. Including a  non-Nothing value here adjusts the  map. Pop the !. Error (crash) if it is empty.  Clear the . +Modify priority of variable; takes care of Double overflow. @Retrieve the maximum-priority variable from the variable order. 2Generate a new clause identifier (always unique). &Add the given clause id to the trace. FGuard a transition action. If the boolean is true, return the action * given as an argument. Otherwise, return .  flip fmap. AChoice of state transitions. Choose the leftmost action that isn't  Nothing , or return Nothing otherwise. r!Verify the solution. In case of h , checks that the assignment is 8 well-formed and satisfies the CNF problem. In case of g , runs a 8 resolution-based checker on a trace of the SAT solver. s6Convert statistics to a nice-to-display tabular form. t<Converts statistics into a tabular, human-readable summary. XYZ[\]^_`abcdefghijklmnopqrstopfhgrcedijklmnq[\]^_`abXYZstXYZYZ[\]^_`ab\]^_`abceddefhgghijklmnjklmnopqrst        !"#$%&'())*+,-./01234456789:;<=>?@ABCDEFGHIJKLMNOPQRRSTUVWXYZ[\]]^_`abcdefghijklmnopqrstuvwxyz{|}~ funsat-0.5.2 Text.TabularControl.Monad.MonadST Funsat.Monad Funsat.TypesFunsat.Resolution Funsat.SolverFunsat.FastDom Funsat.UtilsTablemkTableunTablecombineMonadSTliftST readSTRef writeSTRefnewSTRef modifySTRef SSTErrMonadrunSSTErrMonadevalSSTErrMonadClauseId ReasonMapPartialResolutionTraceresTraceIdCountresTraceresTraceOriginalSingles resSourceMap WatchArray WatchedPairFrozenVarOrderVarOrder varOrderArrFrozenLevelArray LevelArrayLevelModel statusUnder CGNodeAnnotCGNACut reasonSide conflictSidecutUIPcutGraph MAssignment IAssignmentSetlikewithoutwithcontainsCNFnumVars numClausesclausesClauseLitLunLitVarVunVarinLitlitSignvar freezeAssunsafeFreezeAssthawAss unsafeThawAssassignunassign litAssignmentUnsatisfiableCoreResolutionError OrphanSource EmptySourceAntecedentMissingAntecedentImplicationAntecedentNotUnit CannotResolve ResolveErrorResolutionTracetraceFinalClauseIdtraceFinalAssignment traceSourcestraceOriginalClausestraceAntecedentsinitResolutionTracecheckDepthFirst ShowWrapped WrapString unwrapStringStats statsNumConflstatsNumConflTotalstatsNumLearntstatsAvgLearntLenstatsNumDecisions statsNumImpl VerifyError UnsatErrorSatErrorSolutionUnsatSat DPLLConfigCfg configRestartconfigRestartBumpconfigUseVSIDSconfigUseRestartssolvesolve1 defaultConfigverify statTable statSummaryFromNodeToNodePredsIDomNode'iDomdomidomWork refineIDom intersectgetDom numberTree numberForest treeEdgesfixEqCell cellWidthcellDataRow colWidthsbaseGHC.STST Data.EitherLeftRightGHC.Base>>= mtl-1.1.1.0Control.Monad.Error.Class catchError unSSTErrMonaddpllSTbindSSTErrMonadghc-primGHC.BoolTrueFalseGHC.ShowShow isUndefUnder isTrueUnder isFalseUnder isUnitUndergetUnitisSingle modifySlot modifyArray newSTUArray newSTArraycountargmin argminimumtracinguipCutcutLearn mkConflGraphmytraceoutputConflict.&&.ResMUnsatCoreIntSetResState clauseIdMap unsatCore checkDFClauserecursiveBuildresolvegetAntecedentId chooseLiteralcheckAnteClause DPLLMonad FunsatStateSCcnfdlwatcheslearntpropQenqueuedequeueleveltrailreasonnumConfl numConflTotal numDecisionsnumImplvarOrderresolutionTrace dpllConfigstepToSolution solveStepreportSolution preprocessCNF simplifyDBpostProcessUnsat Data.MaybeNothingsolveStepInvariantsfinalAssignmentnoLevelbcpLitbcpselect selectStaticdecidebackJumpdoWhileanalyseundoOnebumpvarIncunsat compactDB watchClause clearQueue varOrderMod varOrderGet nextTraceId traceClauseId==>>=>><initialActivity extractStatsunsafeFreezeWatchArrayconstructResTrace