9      !"#$%&'()*+,-./012345678O9GThere are a bunch of things in the state which are essentially used as   ''set-like'' objects. I'1ve distilled their interface into three methods. I These methods are used extensively in the implementation of the solver. :?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: =, >, ?. @.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  A and is not mutable. BHThe union of the reason side and the conflict side are all the nodes in  the C6 (excepting, perhaps, the nodes on the reason side at G decision level 0, which should never be present in a learned clause). DJAnnotate 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 E instance. F#Mutable array corresponding to the  representation.  ''Generic'' conjunctive normal form. It's  ''generic'' because the J elements of the clause set are polymorphic. And they are polymorphic so  that I can get a G instance. H9Each pair of watched literals is paired with its clause. I*The VSIDS-like dynamic variable ordering. JA  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 K otherwise. #Whenever an assignment of variable v is made at decision level i,   level[unVar v] is set to i. 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  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. 9Run the DPLL-based SAT solver on the given CNF instance. HThe solution to a SAT problem is either an assignment or unsatisfiable. )Configuration parameters for the solver. #Solve with a default configuration L (for debugging). DThe polarity of the literal. Negative literals are false; positive  literals are true. !$The variable for the given literal. #-The assignment as a list of signed literals. $IVerify the assigment is well-formed and satisfies the CNF problem. This B function is run after a solution is discovered, just to be safe. CMakes sure each slot in the assignment is either 0 or contains its L (possibly negated) corresponding literal, and verifies that each clause is  made true by the assignment. M:The reason side contains at least the decision variables. N4The conflict side contains the conflicting literal. O The problem. P4The decision level (last decided literal on front). QInvariant: if l maps to  ((x, y), c), then x == l || y == l. RSame invariant as Q%, but only contains learned conflict  clauses. S;A FIFO queue of literals to propagate. This should not be  manipulated directly; see T and U. V=Chronological trail of assignments, last-assignment-at-head. WEFor each variable, the clause that (was unit and) implied its value. XCThe number of conflicts that have occurred since the last restart. YThe total number of conflicts. ZThe total number of decisions. [1The total number of implications (propagations). \Immutable version. ]x `]` m should use Right if the status of x is  defined, and Left otherwise. ^-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. aA state transition, or step-, produces either an intermediate assignment  (using b !) or a solution to the instance. 3&Number of conflicts before a restart. 43 is altered after each * restart by multiplying it by this value. 5(If true, use dynamic variable ordering. 6If true, use watched literals  scheme. L7A default configuration based on the formula to solve. cSome kind of preprocessing.  remove duplicates dFSimplify the clause database. Eventually should supersede, probably,  c. Precondition: no decisions. eBThe 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. f)Check data structure invariants. Unless -fno-ignore-asserts is passed, + this should be optimised away to nothing. gThis function applies e# recursively until SAT instance is @ solved. It also implements the conflict-based restarting (see  ). hSame as freeze$, but at the right type so GHC doesn't yell at me. iSee h. j<Destructively update the assignment with the given literal. k8Destructively undo the assignment to the given literal. ?;6 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. K Value of the l2 array if corresponding variable unassigned. Had  better be less that 0. mJAssign 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. n2Boolean constraint propagation of all literals in S. If a conflict 2 is found it is returned exactly as described for m. o(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  Ip. qGAssign given decision variable. Records the current assignment before < deciding on the decision variable indexing the assignment. rHNon-chronological backtracking. The current returns the learned clause J implied by the first unique implication point cut of the conflict graph. sdoWhile cmd test first runs cmd, then loops testing test and  executing cmd. The traditional do-while semantics, in other words. tGAnalyse 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. uEGenerate 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. vJGenerate a learned clause from a cut of the graph. Returns a pair of the > learned clause and the decision level to which to backtrack. wJCreates the conflict graph, where each node is labeled by its literal and  level. 9Useful for getting pretty graphviz output of a conflict. xGDelete the assignment to last-assigned literal. Undoes the trail, the  assignment, sets K, undoes reason. Does not touch P. y2Increase the recorded activity of given variable. zO(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, Ts 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. TEnqueue literal in the S) 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. UPop the S!. Error (crash) if it is empty. } Clear the S. ~+Modify priority of variable; takes care of Double overflow. @Retrieve the maximum-priority variable from the variable order. 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. + !"#$%&'()*+,-./012345678+345678# ,&'()*+-./102!%"$ runSSTErrMonad m s executes a   action with initial state s 0 until an error occurs or a result is returned. 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 b  and   for every   ; instead only checks on  . Idea adapted from   1http://haskell.org/haskellwiki/Performance/Monads.  Perform an ST action in the DPLL monad.   1A type class for monads that are able to perform  actions.   Creturn 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 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.  !"#$%&'()*+,!-./0123456789:+;<=>?@ABCDEFGHIJIKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopq rstuvwxyz{|}~Y  I  funsat-0.4 Text.TabularControl.Monad.MonadST DPLL.Monad Funsat.Solverbase Data.BoolPrelude Data.Foldable Data.Either Data.Maybe Control.Monad mtl-1.1.0.1Control.Monad.Error.ClassControl.Monad.STFunsat.FastDom Funsat.UtilsTmkTableunTablecombineMonadST readSTRef writeSTRefnewSTRef modifySTRefliftSTrunSSTErrMonad SSTErrMonadevalSSTErrMonadUnsatSatCfgCNFunVarstupefyGenCNFClause IAssignmentNonStupidStringVarLitsolveStatsSolution DPLLConfigsolve1litSignvar statTable litAssignmentverifyStupid statsNumConflstatsNumConflTotalstatsNumLearntstatsAvgLearntLenstatsNumDecisions statsNumImplnumVars numClausesclausesunLitLV configRestartconfigRestartBumpconfigUseVSIDSconfigUseWatchedLiteralsconfigUseRestartsconfigUseLearningSetlikeModelGHC.BaseTrueFalse isTrueUnder isFalseUnder isUndefUnder DPLLMonad'DPLLStateContentsCutcutGraph CGNodeAnnotGHC.ShowShow MAssignmentFoldable WatchedPairVarOrder LevelArraynoLevel defaultConfig reasonSide conflictSidecnfdlwatcheslearntpropQenqueuedequeuetrailreasonnumConfl numConflTotal numDecisionsnumImplFrozenLevelArray statusUnderwithoutwithcontainsStepLeft preprocessCNF simplifyDB solveStepsolveStepInvariantsstepToSolution freezeAssunsafeFreezeAssassignunassignlevelbcpLitbcpselectdecidebackJumpdoWhileanalyseuipCutcutLearn mkConflGraphundoOnebumpunsat compactDB watchClause clearQueue varOrderMod varOrderGet==>Nothing>=>><Right>>= catchErrordpllSTGHC.STSTiDomdomisSingle modifySlot modifyArray newSTUArraycountargmin argminimumtracingmytraceoutputConflict newSTArray.&&.