N.<      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopq r s t u v w x y z { | } ~       Safeghparse a non-signed integerparse a (signed) integer+return integer list that terminates at zero#top level interface for parsing CNF;read a minisat output: ((numbefOfVariables, 0), [Literal])fromFile "result"((3, 0), [1, -2, 3])return clauses as [[Int]] from file$clauseListFromMinisatOutput "result"[1,-2,3]SafeghWrite the CNF to file f, using 1Convert [Clause] to String, where Clause is [Int]toCNFString [] "p cnf 0 0\n"toCNFString [[-1, 2], [-3, -4]]"p cnf 4 2\n-1 2 0\n-3 -4 0\n",toCNFString [[1], [-2], [-3, -4], [1,2,3,4]],"p cnf 4 4\n1 0\n-2 0\n-3 -4 0\n1 2 3 4 0\n" converts [[Int]] to a String converts [[Int]] to a LaTeX expressionSafegh parse a non-signed integerparse a (signed) integer0Parse something like: p FORMAT VARIABLES CLAUSES=Parse something like: c This in an example of a comment line. Parse the preamble part!+return integer list that terminates at zero"%Parse something like: 1 -2 0 4 0 -3 0##top level interface for parsing CNF$(driver:: String -> Either ParseError IntNread a CNF file and return: ((numbefOfVariables, numberOfClauses), [Literal])fromFile "acnf",((3, 4), [[1, 2], [-2, 3], [-1, 2, -3], [3]]return clauses as [[Int]] from fileclauseListFromFile "a.cnf"#[[1, 2], [-2, 3], [-1, 2, -3], [3]]%&'()* !"#$%&'()* !"#$Safe$9;ghCNF expression <class of objects that can be interpeted as a bool expression ?the start index for the generated variables by Tseitin encoding 'returns the number of variables in the %returns the number of clauses in the + return a clause: list only if it contains some real clause (not a literal),returns the number of valiable used as the output of this expression. and returns itself it the expression is a literal. Otherwise the number is a integer larger than   . Therefore &1 + max tseitinBase the-returned-value) is the next literal variable for future.disjunction constructorasList $ "3" -|- "4"[[3,4,-5],[-3,5],[-4,5]]asList (("3" -|- "4") -|- "-1")/[[3,4,-5],[-3,5],[-4,5],[5,-1,-6],[-5,6],[1,6]]conjunction constructorasList $ "3" -&- "-2"[[-3,2,4],[3,-4],[-2,-4]]asList $ "3" -|- ("1" -&- "2")0[[-1,-2,4],[1,-4],[2,-4],[3,4,-5],[-3,5],[-4,5]] negate a formasList $ neg ("1" -|- "2")&[[1,2,-3],[-1,3],[-2,3],[-3,-4],[3,4]]equal on BoolFormnegation on BoolFormimplication as a short cutasList ("1" ->- "2")&[[-1,-3],[1,3],[3,2,-4],[-3,4],[-2,4]]merge [BoolForm] by '(-|-)' an alias of merge [BoolForm] by '(-&-)' an alias of  converts a BoolForm to "[[Int]]",converts a *satisfied* BoolForm to "[[Int]]""make latex string from CNF, using asLatex $ "3" -|- "4"C"\\begin{displaymath}\n( x_{3} \\vee x_{4} )\n\\end{displaymath}\n""make latex string from CNF, using % -. /012+3,4 !"     "  -. /012+3,4 !"Safegh%String from BoolFrom&String from BoolFrom%& %&%&%& Trustworthygh'mutable Double( mutable Bool) mutable Int*returns a new )+returns the value,sets the value-modifies the value.returns a new (/returns the value0sets the value1modifies the value2returns a new '3returns the value4sets the value5modifies the value'()*+,-./012345'()*+,-./012345(./01)*+,-'2345'()*+,-./012345 Trustworthygh 6Costs of all operations are O(1)7returns the size of 68returns a new 69returns a new 6 filled with an Int:gets the nth value;sets the nth value<modify the nth value=sets all elements>swaps two elements?returns a new 6 from a [Int]@returns a new 6 from a Unboxed Int VectorAcalls  unasfeGrow 6789:;<=>?@A 6789:;<=>?@A 67:;><=89?@A 6789:;<=>?@A Trustworthy 9:;<=?gh"Bmisc information on CNFDnumber of variablesEnumber of clausesFgiven filenameGAssisting ADT for the dynamic variable ordering of the solver. The constructor takes references to the assignment vector and the activity vector of the solver. The method M@ will return the unassigned variable with the highest activity.H constructorI&Called when a new variable is created.J/Called when variable has increased in activity.K<Called when all variables have been assigned new activities.L8Called when variable is unbound (may be selected again).M,Called to select a new, unassigned variable.N)Lifted Boolean domain (p.7) that extends 5 with """ means  undefinedb design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.RThe literal data has an indexZ method which converts the literal to a "small" integer suitable for array indexing. The varB method returns the underlying variable of the literal, and the sign- method if the literal is signed (False for x and True for -x).S represents VarTPublic interface as  ContainerUerases all elements in itVdump the contentsWget a raw dataXconverts into a listYSpecial constant in S (p.7)Z/converts a usual Int as literal to an internal S presentation int2var 1-1 -- the first literal is the first variable int2var 22 -- literal @2@ is variable 2 int2var (-2)02 -- literal @-2@ is corresponding to variable 2[Special constant in R (p.7)\ converts Var into R]returns True if the literal is positive^negates literal negateLit 23 negateLit 32 negateLit 45 negateLit 54_ converts R into S lit2var 21 lit2var 31 lit2var 42 lit2var 52` converts a S to the corresponing literalvar2lit 1 True2var2lit 1 False3var2lit 2 True4var2lit 2 False5a converts 6 into R as lit2int . int2lit == id int2lit 12 int2lit (-1)3 int2lit 24 int2lit (-2)5b converts R into 6 as int2lit . lit2int == id lit2int 21 lit2int 3-1 lit2int 42 lit2int 5-2c converts 5 into LBooldA contant representing FalseeA constant representing TruefA constant for "undefined"h provides U and size'BCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefgh@'()*+,-./0123456789:;<=>?@ABCDEFGMJHIKLNOPQRSTUXVWYZ[\]^_`abcdef%TUVWXSYZRba[\]_`^NOPQcdefGHIJKLMBCDEFBCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefgh  Trustworthy !"$9;<=BghqMutable r Vectorr Fig. 7.(p.11)5 clause, null, binary clause. This matches both of Clause and GClause# in MiniSat TODO: GADTs is better?uwhether this is a learnt clausevactivity of this clausewprotected from reducex.storing the LBD; values are computed in Solverywhich this clause consists ofzdrop the last N literals in a r" to eliminate unsatisfied literals{copies vec and return a new rO Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.|Wreturns the number of literals in a clause, even if the given clause is a binary clause}returns a new q~returns the nth r sets the nth rswaps the two rssupports a restricted set of T methodsThe equality on r is defined with reallyUnsafePtrEquality.qrstuvwxyz{|}~qrstuvwxyz{|}~rstuvwxyz{|q}~ qrstuvwxyz{|}~  Trustworthy !"$9;<=_gh  Vector of Clause + Blocking Literalresizable clause vector sets the expire flag to a clause!returns the associated Int vector O(1) insertern is the number of S, m- is default size of each watcher list | For n2 vars, we need [0 .. 2 + 2 * n - 1] slots, namely  2 * (n + 1)-length vectorreturns the watcher List ::  ClauseManager for Literal l purges all expirable clauses in 789:;<=789:;<=  Trustworthy9;<=ghMutable unboxed Bool Vectorreturns a new returns the nth value in sets the nth valuesets the nth value provides U and size  Trustworthy9;<=ghMutable unboxed Double Vectorreturns a new returns the nth value in sets the nth valueupdates the nth value  Trustworthy9;<=gh Unboxed mutable stack for Int.returns the number of elements clear stack"returns a new stack which size is sizepushs an int to drops the first element from peeks the last element in qShrink the stack. The given arg means the number of discards. therefore, shrink s n == for [1 .. n] $ _ -> pop sJconverts Stack to sized Vec; this is the method to get the internal vectorisomorphic conversion to 6Note: W7 drops the 1st element and no copy (unsafe operation);  really copies the real elements >? >?Safegh6solver's parameters; random decision rate was dropped. decay rate for variable activitydecay rate for clause activity%whether collect and report statistics version namedafault configurationMinisat-1.14 uses (0.95, 0.999, 0.2 = 20 / 1000).Minisat-2.20 uses (0.95, 0.999, 0).Gulcose-4.0 uses (0.8 , 0.999, 0).Mios-1.2 uses (0.95, 0.999, 0).Safe !"$LTgh8 is a heap tree built from two 6[ This implementation is identical wtih that in Minisat-1.14 Note: the zero-th element of heapK is used for holding the number of elements Note: VarHeap itself is not a VarOrder), because it requires a pointer to solverstats Fig. 2.(p.9) Internal State of the solver#If found, this vector has the model9set of literals in the case of conflicts Clause DatabaseList of problem constraints.List of learnt clauses.a list of constraint wathing p(, literal-indexed Assignment Management9The current assignments indexed on variables; var-indexed6The last assignments indexed on variables; var-indexed7List of assignments in chronological order; var-indexed3Separator indices for different decision levels in .+ is divided at qHead; assignments and queueEFor each variable, the constraint that implied its value; var-indexedRFor each variable, the decision level it was assigned; var-indexed Variable Order@Heuristic measurement of the activity of a variable; var-indexed9Keeps track of the dynamic variable order. Configurationsearch paramertersnumber of variablesoClause activity increment amount to bump with. , varDecay :: !DoubleSingleton -- ^ used to set 0Variable activity increment amount to bump with.=Separates incremental and search assumptions. Working Memoryreturn value holderscratch var for analyze ; var-indexeddittodittoused in propagateused in lbd computationused in lbd computationused to create a learnt clause#last decision level used in analyzestatistics information holder>returns an everything-is-initialized solver from the arguments(returns the number of current assigments+returns the number of constraints (clauses)$returns the number of learnt clauses%return the model as a list of literal"returns the current decision levelreturns the assignment (:: N =  [-1, 0, -1]) from Sreturns the assignment (:: N =  [-1, 0, -1]) from RFig. 7. (p.11) returns True- if the clause is locked (used as a reason). Learnt clauses only(increments a stat data corresponding to returns the statistics as listreturns Falseq if a conflict has occured. This function is called only before the solving phase to register the given clauses.@Fig. 8. (p.12)] create a new clause and adds it to watcher lists Constructor function for clauses. Returns False' if top-level conflict is determined.  outClausec may be set to Null if the new clause is already satisfied under the current top-level assignment.Post-condition: psD is cleared. For learnt clauses, all literals will be false except lits[0] (this by design of the analyze method). For the propagation to work, the second watch must be put on the literal which will first be unbound by backtracking. (Note that none of the learnt-clause specific things needs to done for a user defined contraint type.) Fig. 9 (p.14) Puts a new fact on the propagation queue, as well as immediately updating the variable's value in the assignment vector. If a conflict arises, FalseB is returned and the propagation queue is cleared. The parameter from3 contains a reference to the constraint from which p was propagated (defaults to Nothing if omitted).Fig. 12 (p.17) returns False if immediate conflict.Pre-condition: propagation queue is emptyE#M22: Revert to the states at given level (keeping all assignment at  but not beyond).Fig. 14 (p.19) Bumping of clause activityFig. 14 (p.19)AFig. 14 (p.19)Fig. 14 (p.19)Fig. 14 (p.19)BFig. 14 (p.19)C renamed from getmin>Interfate to select a decision var based on variable activity.EDEF@ABGHIJKLMC66"DEF@ABGHIJKLMCSafe$gh7validates the assignment even if the implementation of / is wrong; we re-implement some functions here.Safe!"$Tgh%returns the LBD vaule for 'Vec[1 ..]'returns the LBD value of rupdate the LBD field in rupdate the lbd field of c0 basednextReduction 020000nextReduction 1!40000 + 200 = 20000 + 20000 + 200nextReduction 2(6000 + 600 = 20000 + 20200 + 20000 + 400nextReduction 3280000 + 1200 = 20000 + 20200 + 20400 + 20000 + 600Safe!"$Tgh N#114:  RemoveWatchOFig. 8. (p.12)^ create a new LEARNT clause and adds it to watcher lists This is a strippped-down version of  newClause in SolverP Simplify.f At the top-level, a constraint may be given the opportunity to simplify its representation (returns Falsef) or state that the constraint is satisfied under the current assignment and can be removed (returns True). A constraint must not be simplifiable to produce unit information or to be conflicting; in that case the propagation has not been correctly defined.OMIOS NOTE: the original doesn't update watchers; only checks its satisfiabiliy.QM114: Fig. 10. (p.15)-analyze : (confl : Clause*) (out_learnt : vec Lit"&) (out_btlevel :: int&) -> [void]A__Description:_- Analzye confilct and produce a reason clause.Pre-conditions: *  out_learntW is assumed to be cleared. * Corrent decision level must be greater than root level.Post-conditions:8 * 'out_learnt[0]' is the asserting literal at level  out_btlevel. * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the rest of literals. There may be others from the same level though.analyze is invoked from search {- INLINEABLE analyze -}R#M114 Check if p can be removed, abstract_levelsf is used to abort early if the algorithm is visiting literals at levels that cannot be removed later.Implementation memo: an'toClear is initialized by ps in analyze (a copy of u-). This is used only in this function and analyze.SE#114 analyzeFinal : (confl : Clause *) (skip_first : boot) -> [void] Description:] Specialized analysis proceduce to express the final conflict in terms of assumptions.  root_levelk is allowed to point beyond end of trace (useful if called after conflict while making assumptions). If  skip_first is TRUE, the first literal of conflE is ignored (needed if conflict arose before search even started).T&M114: propagate : [void] -> [Clause+] Description:v Porpagates all enqueued facts. If a conflict arises, the cornflicting clause is returned. otherwise CRef_undef.Post-conditions:C * the propagation queue is empty, even if there was a conflict.memo:  propagate is invoked by search,simpleDB and U#M22 reduceDB: () -> [void] Description: Remove half of the learnt clauses, minus the clauses locked by the current assigmnent. Locked clauses are clauses that are reason to some assignment. Binary clauses are never removed.V(Good to Bad) Quick sort the key vector based on their activities and returns number of privileged clauses. this function uses the same metrix as reduceDB_lt in glucose 4.0: 1. binary clause 2. smaller lbd 3. larger activity defined in MiniSat , where smaller value is better.3they are coded into an Int as the following layout:&14 bit: LBD or 0 for preserved clauses19 bit: converted activityremain: clauseVector index#M22simplify : [void] -> [bool] Description: Simplify the clause database according to the current top-level assigment. Currently, the only thing done here is the removal of satisfied clauses, but more things can be put here.W#M22Hsearch : (nof_conflicts : int) (params : const SearchParams&) -> [lbool] Description:Z Search for a model the specified number of conflicts. NOTE: Use negative value for  nof_conflicts indicate infinity.Output: l_True if a partial assigment that is consistent with respect to the clause set is found. If all variables are decision variables, that means that the clause set is satisfiable. l_False( if the clause set is unsatisfiable. l_Undef0 if the bound on number of conflicts is reached.Fig. 16. (p.20) Main solve method.Pre-condition: If assumptions are used,  must be called right before using this method. If not, a top-level conflict (resulting in a non-usable internal state) cannot be distinguished from a conflict under assumptions.NOPQRSTUVXWYZNOPQRSTUVXWYZSafeghconfiguration swithcesdefault option settings definition of mios option generates help message builds MiosProgramOption$ from string given as command option builds MiosProgramOption from a String  converts MiosProgramOption into SIHConfiguration                      Trustworthy$gh texecutes a solver on the given CNF file This is the simplest entry to standalone programs; not for Haskell programsqexecutes a solver on the given 'arg :: MiosConfiguration' | This is another entry point for standalone programs.$new top-level interface that returns%conflicting literal set :: Left [Int]%satisfiable assignment :: Right [Int]Dthe easiest interface for Haskell programs This returns the result  ::[[Int]] for a given (CNFDescription, [[Int]]) The first argument target can be build by %Just target <- cnfFromFile targetfiler. The second part of the first argument is a list of vector, which 0th element is the number of its real elementstsolves the problem (2rd arg) under the configuration (1st arg) and returns an assignment as list of literals :: Intsvalidates a given assignment from STDIN for the CNF file (2nd arg) this is the entry point for standalone programs|validates a given assignment for the problem (2nd arg) this is another entry point for standalone programs; see app/mios.hsgreturns True if a given assignment (2nd arg) satisfies the problem (1st arg) if you want to check the answer which a slover returned, run solver  answer , where  / :: Traversable t => Solver -> t Lit -> IO Bool'dumps an assigment to file. 2nd arg isTrue* if the assigment is satisfiable assigmentFalse if notCdo y <- solve s ... ; dumpAssigmentAsCNF "result.cnf" y <$> model s[skip comment lines Pre-condition:# we are on the benngining of a line\]^_[`ab,BCDEF     BCDEF\]^_[`abc !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWWXYZ[\]^_`abcdefghijk/lmnopqrstuvwxyz{|}~        #           !"#$%&'()%&*+,'-./0123)4567789:;<=>?@>?A  B C D E F G  HIJKLMNOPQRSTUVWXYZ[\]^_`abcde-fghij!mios-1.2.1-DKdDs6SPjM0C6PcWKTG0WESAT.Util.CNFIO.MinisatReaderSAT.Util.CNFIO.WriterSAT.Util.CNFIO.ReaderSAT.Util.BoolExpSAT.Util.CNFIOSAT.Solver.Mios.Data.SingletonSAT.Solver.Mios.Data.VecSAT.Solver.Mios.TypesSAT.Solver.Mios.ClauseSAT.Solver.Mios.ClauseManagerSAT.Solver.Mios.Data.VecBoolSAT.Solver.Mios.Data.VecDoubleSAT.Solver.Mios.Data.StackSAT.Solver.Mios.InternalSAT.Solver.Mios.SolverSAT.Solver.Mios.ValidatorSAT.Solver.Mios.GlucoseSAT.Solver.Mios.M114SAT.Solver.Mios.OptionParserSAT.Solver.MiosfromMinisatOutputclauseListFromMinisatOutputtoFile toCNFStringtoString toLatexStringfromFileclauseListFromFileBoolFormCnf BoolComponenttoBF tseitinBasenumberOfVariablesnumberOfClauses-|--&-neg-=--!-->- disjunctionOf-|||- conjunctionOf-&&&-asList_asListasLatex_asLatex $fOrdBoolForm$fBoolComponentBool$fBoolComponentBoolForm$fBoolComponent[]$fBoolComponentL$fBoolComponentInt $fEqBoolForm$fShowBoolForm asCNFString asCNFString_DoubleSingleton BoolSingleton IntSingletonnewIntgetIntsetInt modifyIntnewBoolgetBoolsetBool modifyBool newDouble getDouble setDouble modifyDoubleVec sizeOfVectornewVec newVecWithgetNthsetNth modifyNthsetAll swapBetweennewSizedVecIntFromListnewSizedVecIntFromUVectorvecGrowCNFDescription_numberOfVariables_numberOfClauses _pathnameVarOrder newVarOrdernewVarupdate updateAllundoselect LiftedBoolBottomLFalseLTrueLitVar VectorFamilycleardumpasVec bottomVarint2var bottomLitnewLit positiveLit negateLitlit2varvar2litint2litlit2intlboollFalselTruelBottom$fEnumLiftedBool$fVectorFamilyMVectorInt$fBoundedLiftedBool$fEqLiftedBool$fOrdLiftedBool$fReadLiftedBool$fShowLiftedBool$fEqCNFDescription$fOrdCNFDescription$fShowCNFDescription ClauseVectorClause NullClauselearntactivity protectedlbdlits shrinkClausenewClauseFromVec sizeOfClausenewClauseVector getNthClause setNthClause swapClauses$fVectorFamilyMVectorClause$fVectorFamilyClauseInt $fShowClause $fEqClause WatcherListClauseExtManager ClauseManager newManager clearManager shrinkManagergetClauseVector pushClause markClause getKeyVectorpushClauseWithKeynewWatcherList getNthWatchergarbageCollect$fVectorFamilyVectorClause$$fVectorFamilyClauseExtManagerClause$fClauseManagerClauseExtManagerVecBool newVecBool getNthBool setNthBool modifyNthBool$fVectorFamilyMVectorBool VecDouble newVecDouble getNthDouble setNthDoublemodifyNthDouble$fVectorFamilyMVectorDoubleStack sizeOfStack clearStacknewStack pushToStack popFromStack lastOfStack shrinkStack asSizedVecisoVec$fVectorFamilyStackIntMiosConfigurationvariableDecayRateclauseDecayRate collectStats versionIddefaultConfigurationVarHeap StatIndex NumOfBackjump NumOfRestartSolvermodelconflictclauseslearntswatchesassignsphasestrailtrailLimqHeadreasonlevel activitiesorderconfignVarsclaIncvarInc rootLevelokan'seen an'toClearan'stackpr'seenlbd'seenlbd'key litsLearntlastDLstats newSolvernAssignsnClausesnLearntsgetModel decisionLevelvalueVarvalueLitlocked incrementStatgetStats addClauseenqueueassume cancelUntilvarBumpActivityvarDecayActivityclaBumpActivityclaDecayActivity$fVarOrderSolver$fBoundedStatIndex$fEnumStatIndex $fEqStatIndex$fOrdStatIndex$fReadStatIndex$fShowStatIndexvalidate computeLBDlbdOfsetLBD updateLBD nextReduction simplifyDBsolveMiosProgramOption _targetFile _outputFile_confVariableDecayRate_confClauseDecayRate_confCheckAnswer _confVerbose_confTimeProbe_confStatProbe _confNoAnswer_validateAssignment _displayHelp_displayVersionmiosDefaultOption miosOptions miosUsagemiosParseOptionsmiosParseOptionsFromArgs toMiosConfexecuteSolverOn executeSolver runSolversolveSATsolveSATWithConfigurationexecuteValidatorOnexecuteValidatorvalidateAssignmentdumpAssigmentAsCNFpintintseqNumsparseMinisatOutputmint problemLine commentLines preambleCNF parseClausesparseCNFdrivernewlinedigitspacesnoneOf _commentLines clausesOf tseitinNumberL boolFormTrue boolFormFalseisTrueisFalsemaxRankrenumberghc-prim GHC.TypesBoolInt$sel:_nActives:ClauseExtManager$sel:_purged:ClauseExtManager#$sel:_clauseVector:ClauseExtManager $sel:_keyVector:ClauseExtManager purifyManagernumberOfRegisteredClausesivec clauseNewvarRescaleActivityclaRescaleActivity getHeapRootheapidxs newVarHeapnumElementsInHeapinHeap increaseHeap percolateUp percolateDown insertHeap removeWatchnewLearntClausesimplifyanalyzeanalyzeRemovable analyzeFinal propagatereduceDBlbdWidthsearch sortClauses unsafeEnqueue unsafeAssume skipCommentsreportElapsedTime parseHeaderskipWhitespaceparseInt readClauseshowPath