SA      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ 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 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.    >@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 9 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. 0FThe solution to a SAT problem. In each case we return an assignment, ! which is obviously right in the 2 case; in the 1 case, the reason : is to assist in the generation of an unsatisfiable core. 123456789:;<=>?)Transform the number inside the literal. @DThe polarity of the literal. Negative literals are false; positive 0 literals are true. The 0-literal is an error. A$The variable for the given literal. B-The positive literal for the given variable. CDESame as freeze$, but at the right type so GHC doesn't yell at me. FSee E. GHI<Destructively update the assignment with the given literal. J8Destructively undo the assignment to the given literal. K-The assignment as a list of signed literals. > !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJK><=>9:;?@AB834567021C,-./+D*EFGHIJK$%&'()"# !> !!"##$%&'()%&'()*+,-./-./0211234567456789:;:;<=>=>?@ABCDEFGHIJKjL?A circuit problem packages up the CNF corresponding to a given  ? circuit, and the mapping between the variables in the CNF and & the circuit elements of the circuit. MNOP)infinite fresh var source, starting at 1 record var mapping QRno special annotation Sthe edge is the else branch for an  element Tthe edge is the then branch for an  element U!the edge is the condition for an  element VNode type labels for graphs. WXYZ[\]^_`a!A circuit type that constructs a ! representation. This is useful 1 for visualising circuits, for example using the graphviz package. bGA circuit evaluator, that is, a circuit represented as a function from  variable values to booleans. cdefKExplicit tree representation, which is a generic description of a circuit. I This representation enables a conversion operation to any other type of J circuit. Trees evaluate from variable values at the leaves to the root. ghijklmnopqJMaps used to implement the common-subexpression sharing implementation of  the  class. See . rsSource of unique IDs used in ! circuit generation. Should not  include 0 or 1. t/Mapping of generated integer IDs to variables. uvwxyz{|A |" represents a circuit element for  circuits. A | is F a flattened tree node which has been assigned a unique number in the  corresponding map inside rq$, which indicates children, if any.  For example, CAnd i# has the two children of the tuple lookup i (andMap  cmaps) assuming cmaps :: CMaps v. }~J0 is false, 1 is true. Any positive value labels a logical circuit node. 4A shared circuit that has already been constructed. A @ constructed using common-subexpression elimination. This is a A compact representation that facilitates converting to CNF. See .  Instances of 0 admit converting one circuit representation to  another. >A class representing a grammar for logical circuits. Default  implemenations are indicated.  Defined as  p q = not (not p  not q).  Defined as  p q = not (not p  not q). If-then-else circuit.  ite c t e% returns a circuit that evaluates to  t when c evaluates to true, and e otherwise.  Defined as (c  t)  (not c  f).  Defined as  p q = not p  q.  Defined as  p q = (p  q)  (q  p).  Defined as  p q = (p  q)  not (p  q). Reify a sharing circuit. A rq with an initial s of 2. !Find key mapping to given value. prj upd !Evaluate a circuit given inputs. +Given a frozen shared circuit, construct a  that exactly ? represents it. Useful for debugging constraints generated as   circuits. (Performs obvious constant propagations. LProduces a CNF formula that is satisfiable if and only if the input circuit  is satisfiable. 8Note that it does not produce an equivalent CNF formula. G It is not equivalent in general because the transformation introduces N variables into the CNF which were not present as circuit inputs. (Variables J in the CNF correspond to circuit elements.) Returns equisatisfiable CNF O along with the frozen input circuit, and the mapping between the variables of # the CNF and the circuit elements. JThe implementation uses the Tseitin transformation, to guarantee that the N output CNF formula is linear in the size of the circuit. Contrast this with O the naive DeMorgan-laws transformation which produces an exponential-size CNF  formula. GReturns an equivalent circuit with no iff, xor, onlyif, and ite nodes. Projects a funsat 0' back into the original circuit space, I returning a boolean environment containing an assignment of all circuit  inputs to true and false. ZLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~c|~}qrstuvwxyz{fponmlkjihgaV`_^]\[ZYXWQUTSRebcdLMNOPZLMNOPMNOPQUTSRRSTUV `_^]\[ZYXWWXYZ[\]^_`abcdcdef ponmlkjihgghijklmnopq rstuvwxyz{rstuvwxyz{|~}}~  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.  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             !"$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. ?Indicates that the clause id is referenced but has no entry in  . -Indicates that the clause id has an entry in  but  no resolution sources. @Indicates that the variable has no antecedent mapping, in which ( case it should never have been assigned/encountered in the first  place. BIndicates that in the clause-lit pair, the unit literal of clause 2 is the literal, but it ought to be the variable. @Indicates that the constructed antecedent clause not unit under  . BIndicates that the clauses do not have complementary variables or A have too many. The complementary variables (if any) are in the  list. :Indicates that the clauses do not properly resolve on the  variable. FA resolution trace records how the SAT solver proved the original CNF  formula unsatisfiable. ?The id of the last, conflicting clause in the solving process. Final assignment.  Precondition1: All variables assigned at decision level zero.  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.) +Original clauses of the CNF input formula. JCheck the given resolution trace of a (putatively) unsatisfiable formula.  If the result is *, the proof trace has failed to establish K the unsatisfiability of the formula. Otherwise, an unsatisfiable core of  clauses is returned. This function simply calls . The 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. ()P+The show instance uses the wrapped string. (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. 6Total number of decisions since beginning of solving. >Total number of unit implications since beginning of solving. 6Indicates an error in the resultion checking process. 7Indicates 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. 0Same invariant as /%, but only contains learned conflict  clauses. 1;A FIFO queue of literals to propagate. This should not be  manipulated directly; see 2 and 3. 45=Chronological trail of assignments, last-assignment-at-head. 6EFor each variable, the clause that (was unit and) implied its value. 7CThe number of conflicts that have occurred since the last restart. 8The total number of conflicts. 9The total number of decisions. :1The total number of implications (propagations). ;<=)Configuration parameters for the solver. &Number of conflicts before a restart.  is altered after each * restart by multiplying it by this value. (If true, use dynamic variable ordering. 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 1, and thus is only  present when the result is 1. %Solve with the default configuration . >This function applies ?# recursively until SAT instance is M solved, starting with the given initial assignment. It also implements the  conflict-based restarting (see ). @7A 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 ASome kind of preprocessing.  remove duplicates BFSimplify the clause database. Eventually should supersede, probably,  A.  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. C Precondition:! problem determined to be unsat. JRecords id of conflicting clause in trace before failing. Always returns  D. E)Check data structure invariants. Unless -fno-ignore-asserts is passed, + this should be optimised away to nothing. F Value of the 42 array if corresponding variable unassigned. Had  better be less that 0. GJAssign 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. H2Boolean constraint propagation of all literals in 1. If a conflict 2 is found it is returned exactly as described for G. I(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  . JKGAssign given decision variable. Records the current assignment before < deciding on the decision variable indexing the assignment. LHNon-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. MdoWhile cmd test first runs cmd, then loops testing test and  executing cmd. The traditional do-while semantics, in other words. NGAnalyse 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 OGDelete the assignment to last-assigned literal. Undoes the trail, the  assignment, sets F, undoes reason. Does not touch .. P2Increase the recorded activity of given variable. Q'Constant amount by which a variable is Ped. RO(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. S.Keep the smaller half of the learned clauses. TIAdd clause to the watcher lists, unless clause is a singleton; if clause  is a singleton, 2s 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? 2Enqueue literal in the 1) 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 6 map. 3Pop the 1!. Error (crash) if it is empty. U Clear the 1. V+Modify priority of variable; takes care of Double overflow. W@Retrieve the maximum-priority variable from the variable order. X2Generate a new clause identifier (always unique). Y&Add the given clause id to the trace. ZFGuard a transition action. If the boolean is true, return the action * given as an argument. Otherwise, return D. [ flip fmap. \AChoice of state transitions. Choose the leftmost action that isn't  Nothing , or return Nothing otherwise. ]!Verify the solution. In case of 2 , checks that the assignment is 8 well-formed and satisfies the CNF problem. In case of 1 , runs a 8 resolution-based checker on a trace of the SAT solver. 6Convert statistics to a nice-to-display tabular form. <Converts statistics into a tabular, human-readable summary. ^_`012021a       !!"#$%&'()**+,-./01234567889:;<=>?@ABCDEFGHIJKLMNOPPQRSTUVWXYZ[\]^_`abcdeefghijklmnopqrsstuvwxyz{|}~dd                       !""#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcd funsat-0.6.0 Text.TabularControl.Monad.MonadST Funsat.Monad Funsat.TypesFunsat.CircuitFunsat.Resolution Funsat.SolverFunsat.FastDom Funsat.UtilsTablemkTableunTablecombineMonadSTliftST readSTRef writeSTRefnewSTRef modifySTRef SSTErrMonadrunSSTErrMonadevalSSTErrMonadClauseId ReasonMapPartialResolutionTraceresTraceIdCountresTraceresTraceOriginalSingles resSourceMap WatchArray WatchedPairFrozenVarOrderVarOrder varOrderArrFrozenLevelArray LevelArrayLevelModel statusUnder CGNodeAnnotCGNACut reasonSide conflictSidecutUIPcutGraph MAssignment IAssignmentSetlikewithoutwithcontainsSolutionUnsatSatCNFnumVars numClausesclausesClauseLitLunLitVarVunVarinLitlitSignvarlitfinalAssignmentshowAssignment freezeAssunsafeFreezeAssthawAss unsafeThawAssassignunassign litAssignmentCircuitProblem problemCnfproblemCircuitproblemCodeMapEdgeTypeEVoidEElseEThenETestNodeTypeNIteNOnlyIfNIffNXorNNotNOrNAndNFalseNTrueNInputGraphEvalunEvalBEnvTreeTIteTOnlyIfTIffTXorTOrTAndTNotTLeafTFalseTTrueCMaps hashCountvarMapandMaporMapnotMapxorMap onlyifMapiffMapiteMapCCodeCIteCIffCOnlyifCXorCNotCOrCAndCVarCFalseCTrue circuitHash CircuitHash FrozenSharedSharedunShared CastCircuit castCircuitCircuittruefalseinputnotandoriteonlyififfxor runShared falseHashtrueHash emptyCMapsfoldTreerunEvalrunGraph shareGraph simplifyTreetoCNFprojectCircuitSolutionUnsatisfiableCoreResolutionError OrphanSource EmptySourceAntecedentMissingAntecedentImplicationAntecedentNotUnit CannotResolve ResolveErrorResolutionTracetraceFinalClauseIdtraceFinalAssignment traceSourcestraceOriginalClausestraceAntecedentsinitResolutionTrace genUnsatCorecheckDepthFirst ShowWrapped WrapString unwrapStringStats statsNumConflstatsNumConflTotalstatsNumLearntstatsAvgLearntLenstatsNumDecisions statsNumImpl VerifyError UnsatErrorSatError DPLLConfigCfg configRestartconfigRestartBumpconfigUseVSIDSconfigUseRestartssolvesolve1 defaultConfigverify statTable statSummaryFromNodeToNodePredsIDomNode'iDomdomidomWork refineIDom intersectgetDom numberTree numberForest treeEdgesfixEqCell cellWidthcellDataRow colWidths padStringzipnbaseGHC.STST Data.EitherLeftRightGHC.Base>>= mtl-1.1.1.0Control.Monad.Error.Class catchError unSSTErrMonaddpllSTbindSSTErrMonadghc-primGHC.BoolTrueFalseGHC.ShowShowCNFStateCNFS toCnfVarstoCnfMap CNFResultCP fgl-5.4.2.3Data.Graph.Inductive.GraphunGraph getChildrenlookupvrecordC binaryNodenewNodeDynGraph emptyCNFState removeComplexonTup isUndefUnder isTrueUnder isFalseUnder isUnitUndergetUnitmytraceoutputConflictisSingle modifySlot modifyArray newSTUArray newSTArraycountargmin argminimumtracing.&&.uipCutcutLearn mkConflGraphResMUnsatCoreIntSetResState clauseIdMap unsatCore checkDFClauserecursiveBuildrecursiveBuildIdsresolvegetAntecedentId chooseLiteralcheckAnteClause DPLLMonad FunsatStateSCcnfdlwatcheslearntpropQenqueuedequeueleveltrailreasonnumConfl numConflTotal numDecisionsnumImplvarOrderresolutionTrace dpllConfigstepToSolution solveStepreportSolution preprocessCNF simplifyDBpostProcessUnsat Data.MaybeNothingsolveStepInvariantsnoLevelbcpLitbcpselect selectStaticdecidebackJumpdoWhileanalyseundoOnebumpvarIncunsat compactDB watchClause clearQueue varOrderMod varOrderGet nextTraceId traceClauseId==>>=>><initialActivity extractStatsunsafeFreezeWatchArrayconstructResTrace