7(:      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~ 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 BoolForm negation on BoolForm implication 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 %   " SafeghWrite the DIMACS to file f, using 1Convert [Clause] to String, where Clause is [Int]toDIMACSString [] "p cnf 0 0\n""toDIMACSString [[-1, 2], [-3, -4]]"p cnf 4 2\n-1 2 0\n-3 -4 0\n"/toDIMACSString [[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 expression    Safegh 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 Int!Nread 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]#$#$#$#$Safegh%String from BoolFrom&String from BoolFrom%& !"#$%&!"#$%&%& Trustworthy 9:;<=?DRgh' Alias of Vec Int0. The 0-th element holds the number of elements.(Interface on stacks)returns a new stack.*(pushs an value to the tail of the stack.+pops the last element.,peeks the last element.-shrinks the stack..Mutable Double/ Mutable Bool0 Mutable Int Note: Int' is the same with '1!Interface for single mutable data2"allocates and returns an new data.3gets the value.4sets the value.5calls an update function on it.6Another abstraction layer on 8.Note: the 0-th element of Vec Int< is reserved for internal tasks. If you want to use it, use  UVector Int.80A thin abstract layer for Mutable unboxed Vector9Interface on vectors.: returns the n -th value.; sets the n -th value.<erases all elements in it.=converts to an Int vector.> returns the nF-th value (index starts from zero in any case). | swaps two elements.?calls the update function.@returns a new vector.Asets all elements.Bextends the size of stack by n8; note: values in new elements aren't initialized maybe.Cconverts to a list.Dreturns a new ' from [Int].''()*+,-./0123456789:;<=>?@ABCDEFGHIJKLM'()*+,-./0152346789<C:;=>?@ABD9:;<=>?@ABC86712345/.0()*+,-'D'()*+,-./0123456789 :;<=>?@ABCDEFGHIJKLMSafe<=ghN6Solver's parameters; random decision rate was dropped.P~decay rate for variable activity , clauseDecayRate :: !Double -- ^ decay rate for clause activityQMisc information on a CNFSthe number of variablesTthe number of clausesUgiven filenameVAssisting 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 Y@ will return the unassigned variable with the highest activity.W;should be called when a variable has increased in activity.XIshould be called when a variable becomes unbound (may be selected again).Y3returns a new, unassigned var as the next decision.ZThe 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).[ represents Var.\Special constant in [ (p.7)]/converts a usual Int as literal to an internal [ 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 Z (p.7)_returns True if the literal is positive`negates literal negateLit 23 negateLit 32 negateLit 45 negateLit 54a converts Z into [. lit2var 21 lit2var 31 lit2var 42 lit2var 52b converts a [ to the corresponing literal.var2lit 1 True2var2lit 1 False3var2lit 2 True4var2lit 2 False5c converts  into Z as lit2int . int2lit == id. int2lit 12 int2lit (-1)3 int2lit 24 int2lit (-2)5d converts Z into  as int2lit . lit2int == id. lit2int 21 lit2int 3-1 lit2int 42 lit2int 5-2eFALSE on the Lifted Bool domainfTRUE on the Lifted Bool domaing UNDEFINED on the Lifted Bool domainhdafault 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).NOPQRSTUVWXYZ[\]^_`abcdefgh9'()*+,-./0152346789<C:;=>?@ABDNOPQRSTUVYWXZ[\]^_`abcdefgh[\]Zdc^_ab`efgVWXYQRSTUNOPhNOPQRSTUVWXYZ[\]^_`abcdefghSafeghlconfiguration swithcesydefault option settingszdefinition of mios option{generates help message|builds MiosProgramOption$ from string given as command option}builds MiosProgramOption from a String~ converts MiosProgramOption into SIHConfigurationlmnopqrstuvwxyz{|}~NOPhlmnopqrstuvwxyz{|}~NOPhlmnopqrstuvwxyz{|}~l mnopqrstuvwxyz{|}~  Trustworthy !"$9;<=Bgh Mutable  Vector Fig. 7.(p.11): normal, null (and binary) clause. This matches both of Clause and GClause in MiniSat.jwhether this is a learnt clause , rank :: !Int' -- ^ goodness like LBD; computed in Rankingactivity of this clauseprotected from reducewhich this clause consists ofcopies vec and return a new P. Since 1.0.100 DIMACS reader should use a scratch buffer allocated statically.returns a new . is a vector of . is a  StackfamilyLon literals since literals in it will be discared if satisifed at level = 0. is a 1! on the number of literals in it. is a 9 of Z.The equality on  is defined with reallyUnsafePtrEquality.     Trustworthy !"$9;<=gh Immutable Vector of Clause + Blocking LiteralResizable vector of .!sets the expire flag to a clause./returns the associated Int vector, which holds blocking literals. O(1) insertern is the number of [, 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 for Literal l. is an Z-indexed collection of . is a collection of  is a  is a ( on clauses. is a 1! on the numeber of clauses in it.        Safe !"$LTgh:A heap tree built from two 6]. This implementation is identical wtih that in Minisat-1.14. Note: the zero-th element of heapL is used for holding the number of elements. Note: VarHeap itself is not a VarOrder*, because it requires a pointer to solver. stat indexthe number of backjumpthe number of restartDon't use this dummy. Fig. 2.(p.9) Internal State of the solver#If found, this vector has the model(Set of literals in the case of conflictsList of problem constraints.List of learnt clauses.list of constraint wathing p, literal-indexed,The current assignments indexed on variables)The last assignments indexed on variables*List of assignments in chronological order3Separator indices for different decision levels in .4 is divided at qHead; assignment part and queue part8For each variable, the constraint that implied its value5For each variable, the decision level it was assigned3Heuristic measurement of the activity of a variable*Keeps track of the dynamic variable order.search paramertersnumber of variables0Variable activity increment amount to bump with.-Separates incremental and search assumptions. return value holderused in  used in  used in  last decision level used in  used in   and   to create a learnt clausestatistics 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.'returns the model as a list of literal.#returns the current decision level.returns the assignment (::  LiftedBool =  [-1, 0, -1]) from [.returns the assignment (::  LiftedBool =  [-1, 0, -1]) from Z.Fig. 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 a list.returns 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.) Left False if the clause is in a confilct Left True if the clause is satisfied Right clause' if the clause is enqueued successfully 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).$value for rescaling clause activity.Fig. 14 (p.19) Bumping of clause activityFig. 14 (p.19)Fig. 14 (p.19)Fig. 14 (p.19)Fig. 14 (p.19)Fig. 14 (p.19),returns the value on the root (renamed from getmin).>Interfate to select a decision var based on variable activity.F 66&  Safe!"$Tghreturns a rank of . Smaller value is better.#114:  RemoveWatchFig. 8. (p.12)` creates a new LEARNT clause and adds it to watcher lists. This is a strippped-down version of  newClause in Solver. 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. M114: 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!#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."E#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).#&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 $#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.%(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.&#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.'Though  is defined in , most functions in M114 use  unsafeEnqueue.(Pre-condition: propagation queue is empty. !"#$%)&'( !"#$%)&'( Safe$gh7validates the assignment even if the implementation of / is wrong; we re-implement some functions here.Safe$gh  version namevexecutes a solver on the given CNF file. This is the simplest entry to standalone programs; not for Haskell programs.pexecutes 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]EThe 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 targetfiles. The second part of the first argument is a list of vector, which 0th element is the number of its real elements.vsolves the problem (2rd arg) under the configuration (1st arg). and returns an assignment as list of literals :: Int.uvalidates 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.hreturns 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+,-.*/01)NOPQRSTUhlmnopqrstuvwxyz{|}~QRSTU+,-.*/012 !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGGHIJKLMNOPQR#STUVWXYZ[\]]^__`abcdefghijklmnopqrstuvwxyyz{|}~                                         ! " # $  % & ' ( )  * + ,-./01234!mios-1.4.0-BdbgQDlfNC6JnyS7AkH7CwSAT.Mios.Util.BoolExpSAT.Mios.Util.DIMACS.WriterSAT.Mios.Util.DIMACS.Reader"SAT.Mios.Util.DIMACS.MinisatReaderSAT.Mios.Util.DIMACS SAT.Mios.VecSAT.Mios.TypesSAT.Mios.OptionParserSAT.Mios.ClauseSAT.Mios.ClauseManagerSAT.Mios.Solver SAT.Mios.MainSAT.Mios.ValidatorSAT.MiosanalyzesearchBoolFormCnf BoolComponenttoBF tseitinBasenumberOfVariablesnumberOfClauses-|--&-neg-=--!-->- disjunctionOf-|||- conjunctionOf-&&&-asList_asListasLatex_asLatex $fOrdBoolForm$fBoolComponentBool$fBoolComponentBoolForm$fBoolComponent[]$fBoolComponentL$fBoolComponentInt $fEqBoolForm$fShowBoolFormtoFiletoDIMACSStringtoString toLatexStringfromFileclauseListFromFilefromMinisatOutputclauseListFromMinisatOutputasDIMACSStringasDIMACSString_Stack StackFamilynewStackpushTopopFromlastOfshrinkByDouble'Bool'Int' SingleStoragenew'get'set'modify'VecUVector VecFamilygetNthsetNthreset asUVector swapBetween modifyNthnewVecsetAllgrowBynewStackFromList$fStackFamilyVecInt$fSingleStorageVecInt$fSingleStorageMVectorDouble$fSingleStorageMVectorBool$fSingleStorageMVectorInt$fVecFamilyVecDouble$fVecFamilyVecInt$fVecFamilyMVectorDouble$fVecFamilyMVectorIntMiosConfigurationvariableDecayRateCNFDescription_numberOfVariables_numberOfClauses _pathnameVarOrderupdateundoselectLitVar bottomVarint2var bottomLit positiveLit negateLitlit2varvar2litint2litlit2intlFalselTruelBottomdefaultConfiguration$fEqCNFDescription$fOrdCNFDescription$fShowCNFDescriptionMiosProgramOption _targetFile _outputFile_confVariableDecayRate_confCheckAnswer _confVerbose_confTimeProbe_confStatProbe _confNoAnswer_validateAssignment _displayHelp_displayVersionmiosDefaultOption miosOptions miosUsagemiosParseOptionsmiosParseOptionsFromArgs toMiosConf ClauseVectorClause NullClauselearntactivity protectedlitsnewClauseFromStacknewClauseVector$fVecFamilyMVectorClause$fStackFamilyClauseInt$fSingleStorageClauseInt$fVecFamilyClauseInt $fShowClause $fEqClause WatcherListClauseExtManager ClauseManager newManagergetClauseVector markClause getKeyVectorpushClauseWithKeynewWatcherList getNthWatcher$fVecFamilyVectorClause!$fVecFamilyClauseExtManagerClause$fClauseManagerClauseExtManager#$fStackFamilyClauseExtManagerClause"$fSingleStorageClauseExtManagerIntVarHeap StatIndex NumOfBackjump NumOfRestartEndOfStatIndexSolvermodel conflictsclauseslearntswatchesassignsphasestrailtrailLimqHeadreasonlevel activitiesorderconfignVarsvarInc rootLevelokan'seen an'toClearan'stack an'lastDL litsLearntstats newSolvernAssignsnClausesnLearntsgetModel decisionLevelvalueVarvalueLitlockedgetStatsetStat incrementStatgetStats addClauseenqueueassume cancelUntilclaActivityThresholdvarBumpActivityvarDecayActivityclaBumpActivityclaRescaleActivityAfterRestart$fVarOrderSolver$fBoundedStatIndex$fEnumStatIndex $fEqStatIndex$fOrdStatIndex$fReadStatIndex$fShowStatIndex simplifyDBsolvevalidate versionIdexecuteSolverOn executeSolver runSolversolveSATsolveSATWithConfigurationexecuteValidatorOnexecuteValidatorvalidateAssignmentdumpAssigmentAsCNF clausesOf tseitinNumberL boolFormTrue boolFormFalseisTrueisFalsemaxRankrenumberpintint problemLine commentLines preambleCNFseqNums parseClausesparseCNFdrivernewlinedigitspacesnoneOfmint _commentLinesparseMinisatOutputghc-prim GHC.TypesInt _nActives_purged _clauseVector _keyVector purifyManager clauseNewvarRescaleActivityclaRescaleActivity getHeapRootheapidxsvarActivityThreshold newVarHeapnumElementsInHeapinHeap increaseHeap percolateUp percolateDown insertHeaprankOf removeWatchnewLearntClausesimplifyanalyzeRemovable analyzeFinal propagatereduceDB rankWidth unsafeEnqueue unsafeAssume sortClauses skipCommentsreportElapsedTime parseHeaderskipWhitespaceparseInt readClauseshowPath