m      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijkl1A type class for monads that are able to perform m 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 n  and o  for every  p ; instead only checks on q . Idea adapted from   1http://haskell.org/haskellwiki/Performance/Monads. r 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.   @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: s  (''the  object is true under m''), t  (''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 u 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 0 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. 5DThe polarity of the literal. Negative literals are false; positive 0 literals are true. The 0-literal is an error. 6$The variable for the given literal. 7Same as freeze$, but at the right type so GHC doesn't yell at me. 8See 7. ;<Destructively update the assignment with the given literal. <8Destructively undo the assignment to the given literal. =-The assignment as a list of signed literals. 8vwxy z!"#$%&'()*+{,-./0|12}3456789:;<=0 !"#$%&'()*+,-./0123456789:;<= >$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. I?The id of the last, conflicting clause in the solving process. JFinal assignment.  Precondition1: All variables assigned at decision level zero. K 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.) L+Original clauses of the CNF input formula. OThe 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. >?@ABCDEFGHIJKLMNOOGHIJKLMN?@ABCDEF><P+The show instance uses the wrapped string. U(Number of conflicts since last restart. V0Number of conflicts since beginning of solving. WDNumber of learned clauses currently in DB (fluctuates because DB is  compacted every restart). X+Avg. number of literals per learnt clause. Y6Total number of decisions since beginning of solving. Z>Total number of unit implications since beginning of solving. .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). ^FThe solution to a SAT problem. In each case we return an assignment, ! which is obviously right in the ` case; in the _ case, the reason : is to assist in the generation of an unsatisfiable core. a)Configuration parameters for the solver. c&Number of conflicts before a restart. dc is altered after each * restart by multiplying it by this value. e(If true, use dynamic variable ordering. gDRun 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 when the result is _. h%Solve with the default configuration i. This function applies # recursively until SAT instance is M solved, starting with the given initial assignment. It also implements the  conflict-based restarting (see a). i7A 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. 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. 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 . 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 t  if fact is in conflict,  s 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. 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. 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. j!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. k6Convert statistics to a nice-to-display tabular form. l<Converts statistics into a tabular, human-readable summary. PQRSTUVWXYZ[\]^_`abcdefghijklgh^_`j[\]abcdefiSTUVWXYZPQRkl !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWWXYZ[\]^_`abbcdefghijklmnopqrstuvwxyz{| } ~    '(0; funsat-0.5.1 Text.TabularControl.Monad.MonadST Funsat.Monad Funsat.TypesFunsat.Resolution Funsat.SolverbaseControl.Monad.ST Data.Either Control.Monad mtl-1.1.0.2Control.Monad.Error.Classghc-primGHC.Bool Text.Show Data.MaybeTablemkTableunTablecombineMonadSTliftST readSTRef writeSTRefnewSTRef modifySTRef SSTErrMonadrunSSTErrMonadevalSSTErrMonadClauseId ReasonMapPartialResolutionTraceresTraceIdCountresTraceresTraceOriginalSingles resSourceMap WatchArray WatchedPairFrozenVarOrderVarOrder varOrderArrFrozenLevelArray LevelArrayLevelModel statusUnder CGNodeAnnotCut reasonSide conflictSidecutUIPcutGraph MAssignment IAssignmentSetlikewithoutwithcontainsCNFnumVars numClausesclausesClauseLitunLitVarunVarinLitlitSignvar freezeAssunsafeFreezeAssthawAss unsafeThawAssassignunassign litAssignmentUnsatisfiableCoreResolutionError OrphanSource EmptySourceAntecedentMissingAntecedentImplicationAntecedentNotUnit CannotResolve ResolveErrorResolutionTracetraceFinalClauseIdtraceFinalAssignment traceSourcestraceOriginalClausestraceAntecedentsinitResolutionTracecheckDepthFirst ShowWrapped WrapString unwrapStringStats statsNumConflstatsNumConflTotalstatsNumLearntstatsAvgLearntLenstatsNumDecisions statsNumImpl VerifyError UnsatErrorSatErrorSolutionUnsatSat DPLLConfigCfg configRestartconfigRestartBumpconfigUseVSIDSconfigUseRestartssolvesolve1 defaultConfigverify statTable statSummaryGHC.STSTLeftRightGHC.Base>>= catchErrordpllSTTrueFalseGHC.ShowShowCGNALVresolvegetAntecedentId DPLLMonad FunsatStatecnfdlwatcheslearntpropQenqueuedequeuetrailreasonnumConfl numConflTotal numDecisionsnumImplstepToSolution solveStep preprocessCNF simplifyDBpostProcessUnsatNothingsolveStepInvariantsnoLevellevelbcpLitbcpselectdecidebackJumpdoWhileanalyseundoOnebumpvarIncunsat compactDB watchClause clearQueue varOrderMod varOrderGet nextTraceId traceClauseId==>>=>><