F5g       !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopq r s t u v w x y z { | } ~     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 integer parse 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]]    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]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 % "# $%&' (!) !"     "  "# $%&' (!) !"Safegh%String from BoolFrom&String from BoolFrom%& %&%&%& Trustworthygh 'Costs of all operations are O(1)(returns the size of ')returns a new '*returns a new ' filled with an Int+gets the nth value,sets the nth value-modify the nth value.sets all elements/swaps two elements0returns a new ' from a [Int]1returns a new ' from a Unboxed Int Vector2calls  unasfeGrow '()*+,-./012 '()*+,-./012 '(+,/-.)*012 '()*+,-./012 Trustworthygh3mutable Double4 mutable Bool5 mutable Int6returns a new 57returns the value8sets the value9modifies the value:returns a new 4;returns the value<sets the value=modifies the value>returns a new 3?returns the value@sets the valueAmodifies the value3456789:;<=>?@A3456789:;<=>?@A4:;<=567893>?@A3456789:;<=>?@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 * 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 + into R as lit2int . int2lit == id int2lit 12 int2lit (-1)3 int2lit 24 int2lit (-2)5b converts R into + as int2lit . lit2int == id lit2int 21 lit2int 3-1 lit2int 42 lit2int 5-2c converts * 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<=gh qUnboxed mutable stack for Int.rreturns the number of elementss clear stackt"returns a new stack which size is sizeupushs an int to qvdrops the first element from qwpeeks the last element in qxqShrink the stack. The given arg means the number of discards. therefore, shrink s n == for [1 .. n] $ _ -> pop syJconverts Stack to sized Vec; this is the method to get the internal vector q,rstuvwxyz qrstuvwxy qtsruvwxy q,rstuvwxyz  Trustworthy9;<=gh{Mutable unboxed Bool Vector|returns 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 Safegh6solver's parameters; random decision rate was dropped.~decay rate for variable activity , clauseDecayRate :: !Double -- ^ decay rate for clause activity 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).qrstuvwxy{|}~ Safeghconfiguration swithcesdefault option settingsdefinition of mios optiongenerates help messagebuilds MiosProgramOption$ from string given as command optionbuilds MiosProgramOption from a String converts MiosProgramOption into SIHConfiguration  Trustworthy !"$9;<=BghMutable  Vector Fig. 7.(p.11)5 clause, null, binary clause. This matches both of Clause and GClause# in MiniSat TODO: GADTs is better?swhether this is a learnt clause , rank :: !IntSingleton -- ^ goodness like LBD; computed in Rankingactivity of this clauseprotected from reducewhich this clause consists ofcopies vec and return a new O 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 clausedrop the last N literals in a " to eliminate unsatisfied literalsreturns a new returns the nth  sets the nth swaps the two ssupports a restricted set of T methodsThe equality on  is defined with reallyUnsafePtrEquality.  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 -./012 -./012Safe !"$LTgh733 is a heap tree built from two '[ 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 solver stat index 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 variables , claInc :: !DoubleSingleton -- ^ Clause 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 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 onlyreturns the value of sets to (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.4Fig. 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)5Fig. 14 (p.19)Fig. 14 (p.19)6Fig. 14 (p.19)Fig. 14 (p.19)7 renamed from getmin>Interfate to select a decision var based on variable activity.F389:4;56<=>?@AB755&389:4;56<=>?@AB7Safe!"$Tgh Ca special version of rankingD#114:  RemoveWatchEFig. 8. (p.12)^ create a new LEARNT clause and adds it to watcher lists This is a strippped-down version of  newClause in SolverF 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.GM114: 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 -}H#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 -). This is used only in this function and analyze.IE#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).J&M114: propagate : [void] -> [Clause+] Description:u Porpagates all enqueued facts. If a conflict arises, the conflicting 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 K#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.L(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 rank 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.M#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.CDEFGHIJKLNMOPCDEFGHIJKLNMOPSafe$gh7validates the assignment even if the implementation of / is wrong; we re-implement some functions here. 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.hs greturns 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 sQskip comment lines Pre-condition:# we are on the benngining of a lineR   STUQVWX)BCDEF   BCDEF   R   STUQVWXY !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVVWXYZ[\]^_`abcdefghij.klmnopqrstuvwxyz{|}~        "      !"#$%&'(&)*++,-./01234235 6789:;<=>?;@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_!mios-1.3.0-EBvd1AuOVYy4W7RmEw4QWWSAT.Mios.Util.CNFIO.WriterSAT.Mios.Util.CNFIO.Reader!SAT.Mios.Util.CNFIO.MinisatReaderSAT.Mios.Util.BoolExpSAT.Mios.Util.CNFIOSAT.Mios.Data.VecSAT.Mios.Data.SingletonSAT.Mios.TypesSAT.Mios.Data.StackSAT.Mios.Data.VecBoolSAT.Mios.Data.VecDoubleSAT.Mios.InternalSAT.Mios.OptionParserSAT.Mios.ClauseSAT.Mios.ClauseManagerSAT.Mios.Solver SAT.Mios.MainSAT.Mios.ValidatorSAT.MiostoFile toCNFStringtoString toLatexStringfromFileclauseListFromFilefromMinisatOutputclauseListFromMinisatOutputBoolFormCnf BoolComponenttoBF tseitinBasenumberOfVariablesnumberOfClauses-|--&-neg-=--!-->- disjunctionOf-|||- conjunctionOf-&&&-asList_asListasLatex_asLatex $fOrdBoolForm$fBoolComponentBool$fBoolComponentBoolForm$fBoolComponent[]$fBoolComponentL$fBoolComponentInt $fEqBoolForm$fShowBoolForm asCNFString asCNFString_Vec sizeOfVectornewVec newVecWithgetNthsetNth modifyNthsetAll swapBetweennewSizedVecIntFromListnewSizedVecIntFromUVectorvecGrowDoubleSingleton BoolSingleton IntSingletonnewIntgetIntsetInt modifyIntnewBoolgetBoolsetBool modifyBool newDouble getDouble setDouble modifyDoubleCNFDescription_numberOfVariables_numberOfClauses _pathnameVarOrder newVarOrdernewVarupdate updateAllundoselect LiftedBoolBottomLFalseLTrueLitVar VectorFamilycleardumpasVec bottomVarint2var bottomLitnewLit positiveLit negateLitlit2varvar2litint2litlit2intlboollFalselTruelBottom$fEnumLiftedBool$fVectorFamilyMVectorInt$fBoundedLiftedBool$fEqLiftedBool$fOrdLiftedBool$fReadLiftedBool$fShowLiftedBool$fEqCNFDescription$fOrdCNFDescription$fShowCNFDescriptionStack sizeOfStack clearStacknewStack pushToStack popFromStack lastOfStack shrinkStack asSizedVec$fVectorFamilyStackIntVecBool newVecBool getNthBool setNthBool modifyNthBool$fVectorFamilyMVectorBool VecDouble newVecDouble getNthDouble setNthDoublemodifyNthDouble$fVectorFamilyMVectorDoubleMiosConfigurationvariableDecayRate versionIddefaultConfigurationMiosProgramOption _targetFile _outputFile_confVariableDecayRate_confCheckAnswer _confVerbose_confTimeProbe_confStatProbe _confNoAnswer_validateAssignment _displayHelp_displayVersionmiosDefaultOption miosOptions miosUsagemiosParseOptionsmiosParseOptionsFromArgs toMiosConf ClauseVectorClause NullClauselearntactivity protectedlitsnewClauseFromVec sizeOfClause shrinkClausenewClauseVector getNthClause setNthClause swapClauses$fVectorFamilyMVectorClause$fVectorFamilyClauseInt $fShowClause $fEqClause WatcherListClauseExtManager ClauseManager newManager clearManager shrinkManagergetClauseVector pushClause markClause getKeyVectorpushClauseWithKeynewWatcherList getNthWatchergarbageCollect$fVectorFamilyVectorClause$$fVectorFamilyClauseExtManagerClause$fClauseManagerClauseExtManager StatIndex NumOfBackjump NumOfRestartSolvermodelconflictclauseslearntswatchesassignsphasestrailtrailLimqHeadreasonlevel activitiesorderconfignVarsvarInc rootLevelokan'seen an'toClearan'stackpr'seen litsLearntlastDLstats newSolvernAssignsnClausesnLearntsgetModel decisionLevelvalueVarvalueLitlockedgetStatsetStat incrementStatgetStats addClauseenqueueassume cancelUntilclaActivityThresholdvarBumpActivityvarDecayActivityclaBumpActivityclaRescaleActivityAfterRestart$fVarOrderSolver$fBoundedStatIndex$fEnumStatIndex $fEqStatIndex$fOrdStatIndex$fReadStatIndex$fShowStatIndex simplifyDBsolvevalidateexecuteSolverOn executeSolver runSolversolveSATsolveSATWithConfigurationexecuteValidatorOnexecuteValidatorvalidateAssignmentdumpAssigmentAsCNFpintint problemLine commentLines preambleCNFseqNums parseClausesparseCNFdrivernewlinedigitspacesnoneOfmint _commentLinesparseMinisatOutput clausesOf tseitinNumberL boolFormTrue boolFormFalseisTrueisFalsemaxRankrenumberghc-prim GHC.TypesBoolInt$sel:_nActives:ClauseExtManager$sel:_purged:ClauseExtManager#$sel:_clauseVector:ClauseExtManager $sel:_keyVector:ClauseExtManager purifyManagerVarHeap clauseNewvarRescaleActivityclaRescaleActivity getHeapRootheapidxsvarActivityThreshold newVarHeapnumElementsInHeapinHeap increaseHeap percolateUp percolateDown insertHeapranking' removeWatchnewLearntClausesimplifyanalyzeanalyzeRemovable analyzeFinal propagatereduceDB rankWidthsearch sortClauses unsafeEnqueue unsafeAssume skipCommentsreportElapsedTime parseHeaderskipWhitespaceparseInt readClauseshowPath