>U      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTHUHThe union of the reason side and the conflict side are all the nodes in  the V6 (excepting, perhaps, the nodes on the reason side at G decision level 0, which should never be present in a learned clause). WJAnnotate 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 X instance. Y@Each pair of watched literals is paired with its clause and id. Z*The VSIDS-like dynamic variable ordering. [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 \ otherwise. #Whenever an assignment of variable v is made at decision level i,   level[unVar v] is set to i. <+The show instance uses the wrapped string. @DRun 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 =, and thus is only  present then. BHThe solution to a SAT problem is either an assignment or unsatisfiable. C)Configuration parameters for the solver. D%Solve with the default configuration E. E7A 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 F!Verify the solution. In case of > , checks that the assignment is 8 well-formed and satisfies the CNF problem. In case of = , runs a 8 resolution-based checker on a trace of the SAT solver. G6Convert statistics to a nice-to-display tabular form. H<Converts statistics into a tabular, human-readable summary. J(Number of conflicts since last restart. K0Number of conflicts since beginning of solving. LDNumber of learned clauses currently in DB (fluctuates because DB is  compacted every restart). M+Avg. number of literals per learnt clause. N6Total number of decisions since beginning of solving. O>Total number of unit implications since beginning of solving. ]:The reason side contains at least the decision variables. ^4The conflict side contains the conflicting literal. _.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. a The problem. b4The decision level (last decided literal on front). cInvariant: if l maps to  ((x, y), c), then x == l || y == l. dSame invariant as c%, but only contains learned conflict  clauses. e;A FIFO queue of literals to propagate. This should not be  manipulated directly; see f and g. h=Chronological trail of assignments, last-assignment-at-head. iEFor each variable, the clause that (was unit and) implied its value. jCThe number of conflicts that have occurred since the last restart. kThe total number of conflicts. lThe total number of decisions. m1The total number of implications (propagations). nImmutable version. oA state transition, or step-, produces either an intermediate assignment  (using p !) or a solution to the instance. Q&Number of conflicts before a restart. RQ is altered after each * restart by multiplying it by this value. S(If true, use dynamic variable ordering. qSome kind of preprocessing.  remove duplicates rFSimplify the clause database. Eventually should supersede, probably,  q.  Precondition: decision level 0. sBThe 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. t Precondition:! problem determined to be unsat. +Records id of conflicting clause in trace. u)Check data structure invariants. Unless -fno-ignore-asserts is passed, + this should be optimised away to nothing. vThis function applies s# recursively until SAT instance is @ solved. It also implements the conflict-based restarting (see  C). \ Value of the w2 array if corresponding variable unassigned. Had  better be less that 0. xJAssign 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. y2Boolean constraint propagation of all literals in e. If a conflict 2 is found it is returned exactly as described for x. z(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  Z{. |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. ~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. GDelete the assignment to last-assigned literal. Undoes the trail, the  assignment, sets \, undoes reason. Does not touch b. 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, fs 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. fEnqueue literal in the e) 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. gPop the e!. Error (crash) if it is empty.  Clear the e. +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. 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. 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. 89:;<=>?@ABCDEFGHIJKLMNOPQRST@DB=>F?89C:QRSTEAPJKLMNO<I;GHIWhether all the elements of the model in the list are false but one, and  none is true, under 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. GGet the element of the list which is not false under the model. If no  such element, throws an error. 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.  ''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 easily get a   instance. ?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: , , #. 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. #Mutable array corresponding to the  representation. 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 . <Destructively update the assignment with the given literal. !8Destructively undo the assignment to the given literal. "-The assignment as a list of signed literals. # 6 if and only if the object is undefined in the model. 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. $ !"#$$ !"# &$Unsatisfiable cores are not unique. 'CA 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. +The depth-first method. 3?The id of the last, conflicting clause in the solving process. 4Final assignment.  Precondition1: All variables assigned at decision level zero. 5 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.) 6+Original clauses of the CNF input formula. 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. %&'()*+,-./01234567+(%34567*'210/.-,&) 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 p  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.  !"#$%&'()*+,-./01234567897:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`Rabcdefghijklmnopqrstuvwxyz{|}~ k  6  funsat-0.5 Text.TabularControl.Monad.MonadST Funsat.Monad Funsat.TypesFunsat.Resolution Funsat.SolverbasePrelude Data.Either Data.Bool Data.Maybe Data.Foldable Control.Monad mtl-1.1.0.1Control.Monad.Error.ClassControl.Monad.STFunsat.FastDom Funsat.UtilsTablemkTableunTablecombineMonadST readSTRef writeSTRefnewSTRef modifySTRefliftSTrunSSTErrMonad SSTErrMonadevalSSTErrMonad isUnitUnder isTrueUnder isFalseUndergetUnitSetlikeClauseGenCNFModel IAssignment MAssignmentVarLitlitSignvar freezeAssunsafeFreezeAssthawAss unsafeThawAssassignunassign litAssignment isUndefUnderCNFResolutionTraceUnsatisfiableCoreResolutionErrorClauseIdinitResolutionTracecheckDepthFirst ResolveError CannotResolveAntecedentNotUnitAntecedentImplicationAntecedentMissing EmptySource OrphanSourcetraceFinalClauseIdtraceFinalAssignment traceSourcestraceOriginalClausestraceAntecedents UnsatErrorSatErrorCfg unwrapString ShowWrappedUnsatSat VerifyErrorsolveStatsSolution DPLLConfigsolve1 defaultConfigverify statTable statSummary WrapString statsNumConflstatsNumConflTotalstatsNumLearntstatsAvgLearntLenstatsNumDecisions statsNumImpl configRestartconfigRestartBumpconfigUseVSIDSconfigUseRestartsCutcutGraph CGNodeAnnotGHC.ShowShow WatchedPairVarOrder LevelArraynoLevel reasonSide conflictSide DPLLMonad FunsatStatecnfdlwatcheslearntpropQenqueuedequeuetrailreasonnumConfl numConflTotal numDecisionsnumImplFrozenLevelArrayStepLeft preprocessCNF simplifyDB solveSteppostProcessUnsatsolveStepInvariantsstepToSolutionlevelbcpLitbcpselectdecidebackJumpdoWhileanalyseundoOnebumpvarIncunsat compactDB watchClauseGHC.BaseFalseTrue clearQueue varOrderMod varOrderGet nextTraceId traceClauseId==>Nothing>=>><uipCutcutLearn mkConflGraphFoldable statusUnderwithoutwithcontainsunVarinLitnumVars numClausesclausesunLitLVresolvegetAntecedentIdRight>>= catchErrordpllSTGHC.STSTiDomdomisSingle modifySlot modifyArray newSTUArraycountargmin argminimumtracingmytraceoutputConflict newSTArray.&&.