\nF@      !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTUVWXYZ[\]^_`abcdefghijklmnopqrstuvwxyz{|}~                                  ! " # $ % & ' ( ) * +,-./0123456789:;<=>?Safe%;=ij&CNF 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)Areturns 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   BCSafeij,Dparse a non-signed integerEparse a (signed) integerF+return integer list that terminates at zeroG#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]Safeij6 Hparse a non-signed integerIparse a (signed) integerJ0Parse something like: p FORMAT VARIABLES CLAUSESK=Parse something like: c This in an example of a comment line.LParse the preamble partM+return integer list that terminates at zeroN%Parse something like: 1 -2 0 4 0 -3 0O#top level interface for parsing CNFP(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]] ! !Safeij?AFTijPY(Stack of Int, an alias of Vec Int)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 Double0 Mutable Int Note: Int' is identical to (1 Mutable Bool25Interface for single (one-length vector) mutable data3"allocates and returns an new data.4gets the value.5sets the value.6calls an update function on it.Q0A thin abstract layer for mutable unboxed Vector7Another abstraction layer on Vector0 which reserves zero element for internal use. Note+: If you want to use the 0-th element, use  UVector Int.8The interface on vectors.9 returns the n -th value.: sets the n -th value.;erases all elements in it.< returns the nF-th value (index starts from zero in any case). | swaps two elements.=calls the update function.>returns a new vector.?sets all elements.@extends the size of stack by n8; note: values in new elements aren't initialized maybe.Aconverts to a list.Breturns a new ( from [Int].C%returns the number of allocated slotsD5sort the content of a stack, in small-to-large order. ()*+,-./01263457RST8;A9:<=>?@BCD89:;<=>?@A7234561/0)*+,-.(BCD)*+,-.234568 9:;<=>?@AUTVSWRSafedij.Mformats of state dumpR stat indexSthe number of backjumpTthe number of restartUthe number of blacking startVthe number of classic restartWthe number of propagationXthe number of reductionYthe number of alive given clausesZthe number of alive learnt clauses[the number of alive variables\ the number of assigned variables]Don't use this dummy.^6Solver's parameters; random decision rate was dropped.` decay rate for variable activityadecay rate for clause activitybdump stats data during solvingcMisc information on a CNFethe number of variablesfthe number of clausesggiven filenamehAssisting 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 k@ will return the unassigned variable with the highest activity.i;should be called when a variable has increased in activity.jIshould be called when a variable becomes unbound (may be selected again).k3returns a new, unassigned var as the next decision.l)Lifted Boolean domain (p.7) that extends X with """ means  undefinedb design note: _|_ should be null = 0; True literals are coded to even numbers. So it should be 2.mThe 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).n represents Var.othe type that Mios returns This captures the following three cases: * solved with a satisfiable assigment, * proved that it's an unsatisfiable problem, and * aborted due to Mios specification or an internal errorpabnormal termination flagsw&terminate and find an SAT/UNSAT answerzCONFLICT on the Lifted Bool domain{ UNDEFINED on the Lifted Bool domain|TRUE on the Lifted Bool domain}FALSE on the Lifted Bool domain~Special constant in n (p.7)/converts a usual Int as literal to an internal n 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 2Special constant in m (p.7)returns True if the literal is positivenegates literal negateLit 23 negateLit 32 negateLit 45 negateLit 54 converts m into n. lit2var 21 lit2var 31 lit2var 42 lit2var 52 converts a n to the corresponing literal.var2lit 1 True2var2lit 1 False3var2lit 2 True4var2lit 2 False5 converts  into m as lit2int . int2lit == id. int2lit 12 int2lit (-1)3 int2lit 24 int2lit (-2)5 converts m into  as int2lit . lit2int == id. lit2int 21 lit2int 3-1 lit2int 42 lit2int 5-2$returns the value of a literal as a ldafault 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).]}|{z()*+,-./01263457RST8;A9:<=>?@BCDMNOPQRSTUVWXYZ[\]^_`abcdefghikjlmnopqrstuvwxy~=owxypqrstuvcdefg^_`abn~ml}|{zhijkRSTUVWXYZ[\]MNOPQ YZ[\]^_`abcdefghMNOPQR STUVWXYZ[\]^_`abcdefghijkpqrstuvwxy}|{zSafeijaconfiguration swithcesdefault option settingsdefinition of mios optiongenerates help messagebuilds MiosProgramOption$ from string given as command optionbuilds MiosProgramOption from a String converts MiosProgramOption into SIHConfiguration^_`ab^_`ab  Trustworthy "#%;=>?Dij Mutable  Vector Fig. 7.(p.11): normal, null (and binary) clause. This matches both of Clause and GClause in MiniSat.goodness like LBD; computed in RankingZactivity of this clause , protected :: !Bool' -- ^ protected 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  StackfamilyLon literals since literals in it will be discared if satisifed at level = 0. is a 2! on the number of literals in it. is a 8 of m.The equality on  is defined with reallyUnsafePtrEquality. is a vector of .   Trustworthy "#%;=>?ijImmutable Vector of Clause + Blocking LiteralClause + 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 n, m. is default size of each watcher list. | For n2 vars, we need [0 .. 2 + 2 * n - 1] slots, namely  2 * (n + 1)'-length vector FIXME: sometimes n > 1Mreturns the watcher List for Literal l. is a  is a ) on clauses. is a 2 on the number of clauses in it. is a collection of  is a  is a ) on clauses. is a 2 on the number of clauses in it. is an m-indexed collection of . ijklmnop  Trustworthy%ijan immutable Vector of ClauseSimpleManagerq@biclause should be stored into index:0, so the real limit is 64.returns a new rreturns ' for caluses which have suitable sizes.nIf a nice candidate as a learnt is stored, return it. Otherwise allocate a new clause in heap then return it.9Note: only not-too-large and learnt clauses are recycled. Safe "#%NV^ij:sA heap tree built from two 7]. 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. Fig. 2.(p.9) Internal State of the solverList 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 assigned(Set of literals in the case of conflicts3Heuristic measurement of the activity of a variable*Keeps track of the dynamic variable order.search paramertersnumber of variables.Clause activity increment amount to bump with.0Variable activity increment amount to bump with.-Separates incremental and search assumptions.used in used in used in  internal flag used in  used in  used in  last decision level used in  clause recyclerused in  and  to create a learnt clausestatistics information holderused in lbd computationused in lbd computationfast ema value of LBDslow ema value of LBDfast ema value of assignmentslow ema value of assignment"next restart in number of conflictmode of restart?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 current decision level.returns the assignment (:: l =  [-1, 0, -1]) from n.returns the assignment (:: l =  [-1, 0, -1]) from m.Fig. 7. (p.11) returns True- if the clause is locked (used as a reason). Learnt clauses only returns the value of R.!sets to R."(increments a stat data corresponding to R.#!returns the statistics as a list.$assigns a value to the n -th variable% 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 empty'E#M22: Revert to the states at given level (keeping all assignment at  but not beyond).t,returns the value on the root (renamed from getmin).(Jprint statatistic data to stdio. This should be called after each restart.)>Interfate to select a decision var based on variable activity.DRSTUVWXYZ[\]      !"#$%&'(D     $%&'RSTUVWXYZ[\] !"#(suvw&      Safe"#%ij*7validates the assignment even if the implementation of / is wrong; we re-implement some functions here.xchecks uniqueness of learnts**Safe"#%^ij +Fig. 14 (p.19) Bumping of clause activity,Fig. 14 (p.19)yFig. 14 (p.19)z$value for rescaling clause activity.-Fig. 14 (p.19).Fig. 14 (p.19){Fig. 14 (p.19)|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/returns Falseq if a conflict has occured. This function is called only before the solving phase to register the given clauses.0returns a POSIVITE value1#62+,-./01-.+,/01Safe "#%V^ij(D}#114:  RemoveWatch~Fig. 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 learnt-). 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 3#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.;applies a (good to bad) quick semi-sort to the vector in a  and returns the number of privileged clauses. This function uses the same criteria as reduceDB_lt in glucose 4.0: 1. binary clause 2. smaller LBD 3. larger activity defined as MiniSatthey are encoded into two Int64%s as the following (10+52+32 layout):10 bits for rank (LBD):  50 bits for converted activity:  32 bits for clauseVector index: 2#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: *  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. * : if the clause set is unsatisfiable or some error occured.3Fig. 16. (p.20) Main solve method.Pre-condition: If assumptions are used, 2 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.$(/23$/(23Safe%]ijET4 version name5vexecutes a solver on the given CNF file. This is the simplest entry to standalone programs; not for Haskell programs.6pexecutes a solver on the given 'arg :: MiosConfiguration'. This is another entry point for standalone programs.print messages on solver's result Note: the last field of benchmark CSV is: * 0 if UNSAT * 1 if satisfiable (by finding an assignment) * other bigger values are used for aborted cases.7%new top-level interface that returns:%conflicting literal set :: Left [Int]%satisfiable assignment :: Right [Int]8EThe 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.9vsolves 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 notJdo y <- solve s ... ; dumpAssigmentAsCNF (Just "result.cnf") y <$> model s>parses the header of a CNF file?>parses ByteString then injects the clauses in it into a solverskip comment lines Pre-condition:# we are on the benngining of a line4^_`abcdefgowxy*3456789:;<=>?4cdefg7893owxy<*56:;>?= !"#$%&'()*+,-./0123456789:;<=>?@ABCDEFGHIJKLMNOPQRSTU(VWXYZ[\]^_`abcdefghijklmnopqrrstuvvwxyz{|}~                                            ! " # $ % & ' ( ) * + , - . / 0 1 2 3 4 5 6 7 8 9:;<=>?@ABCDEFGHIJKLMNOPQQRSTURSVWXTYMZ[L\]^_`abbcdeffghijklmno  p q r s  t u v w x y x z { |}~ mios-1.5.4-HIMwis6IHA6SkvhS5HKVmSAT.Mios.TypesSAT.Mios.Util.BoolExp"SAT.Mios.Util.DIMACS.MinisatReaderSAT.Mios.Util.DIMACS.ReaderSAT.Mios.Util.DIMACS.WriterSAT.Mios.Util.DIMACS SAT.Mios.VecSAT.Mios.OptionParserSAT.Mios.ClauseSAT.Mios.ClauseManagerSAT.Mios.ClausePoolSAT.Mios.SolverSAT.Mios.ValidatorSAT.Mios.Criteria SAT.Mios.MainSAT.Miossearchanalyzeghc-prim GHC.TypesIntBoolFormCnf BoolComponenttoBF tseitinBasenumberOfVariablesnumberOfClauses-|--&-neg-=--!-->- disjunctionOf-|||- conjunctionOf-&&&-asList_asListasLatex_asLatex $fOrdBoolForm$fBoolComponentBool$fBoolComponentBoolForm$fBoolComponent[]$fBoolComponentL$fBoolComponentInt $fEqBoolForm$fShowBoolFormfromMinisatOutputclauseListFromMinisatOutputfromFileclauseListFromFiletoFiletoDIMACSStringtoString toLatexStringasDIMACSStringasDIMACSString_Stack StackFamilynewStackpushTopopFromlastOfshrinkByDouble'Int'Bool' SingleStoragenew'get'set'modify'Vec VecFamilygetNthsetNthreset swapBetween modifyNthnewVecsetAllgrowBynewStackFromListrealLengthOfStack sortStack$fVecFamilyVecInt$fVecFamilyMVectorInt$fVecFamilyVecInt0$fVecFamilyVecDouble$fSingleStorageVecDouble$fSingleStorageVecInt$fSingleStorageMVectorBool$fStackFamilyVecIntDumpModeNoDump DumpCSVHeaderDumpCSVDumpJSON StatIndex NumOfBackjump NumOfRestartNumOfBlockRestartNumOfGeometricRestartNumOfPropagationNumOfReduction NumOfClause NumOfLearnt NumOfVariable NumOfAssignedEndOfStatIndexMiosConfigurationvariableDecayRateclauseDecayRatedumpStatCNFDescription_numberOfVariables_numberOfClauses _pathnameVarOrderupdateundoselect LiftedBoolLitVar SolverResultSolverException StateUNSATStateSAT OutOfMemoryTimeOutInternalInconsistentUndescribedError CertificateSATUNSATConflictLBottomLiftedTLiftedF bottomVarint2var bottomLit positiveLit negateLitlit2varvar2litint2litlit2int lit2lbooldefaultConfiguration$fEqCertificate$fOrdCertificate$fReadCertificate$fShowCertificate$fBoundedSolverException$fEnumSolverException$fEqSolverException$fOrdSolverException$fShowSolverException$fEqCNFDescription$fOrdCNFDescription$fReadCNFDescription$fShowCNFDescription$fEqMiosConfiguration$fOrdMiosConfiguration$fReadMiosConfiguration$fShowMiosConfiguration$fBoundedStatIndex$fEnumStatIndex $fEqStatIndex$fOrdStatIndex$fReadStatIndex$fShowStatIndex$fBoundedDumpMode$fEnumDumpMode $fEqDumpMode $fOrdDumpMode$fReadDumpMode$fShowDumpMode$fBoundedDumpTag $fEnumDumpTag $fEqDumpTag $fOrdDumpTag $fReadDumpTag $fShowDumpTag $fEqMiosStats$fOrdMiosStats$fReadMiosStats$fShowMiosStats $fEqMiosDump $fOrdMiosDump$fReadMiosDump$fShowMiosDumpMiosProgramOption _targetFile_targets _outputFile_confVariableDecayRate_confClauseDecayRate _confMaxSize_confCheckAnswer _confVerbose_confBenchmark _confBenchSeq _confNoAnswer _confDumpStat_validateAssignment _displayHelp_displayVersionmiosDefaultOption miosOptions miosUsagemiosParseOptionsmiosParseOptionsFromArgs toMiosConf ClauseVectorClause NullClauserankactivitylitsnewClauseFromStacknewClauseVector$fStackFamilyClauseInt$fSingleStorageClauseInt$fVecFamilyClauseInt $fShowClause $fEqClause$fVecFamilyMVectorClause WatcherListClauseExtManagerClauseSimpleManager ClauseManager newManagergetClauseVector markClause getKeyVectorpushClauseWithKeynewWatcherList getNthWatcher"$fClauseManagerClauseSimpleManager&$fStackFamilyClauseSimpleManagerClause%$fSingleStorageClauseSimpleManagerInt!$fVecFamilyClauseExtManagerClause$fClauseManagerClauseExtManager#$fStackFamilyClauseExtManagerClause"$fSingleStorageClauseExtManagerInt$fVecFamilyVectorClause ClausePool newClausePoolmakeClauseFromStack putBackToPoolSolverclauseslearntswatchesassignsphasestrailtrailLimqHeadreasonlevel conflicts activitiesorderconfignVarsclaIncvarInc rootLevel learntSAdj learntSCnt maxLearntsokan'seen an'toClearan'stack an'lastDLclsPool litsLearntstatslbd'seenlbd'keyemaDFastemaDSlowemaAFastemaASlow nextRestart restartMode newSolvernAssignsnClausesnLearnts decisionLevelvalueVarvalueLitlockedgetStatsetStat incrementStatgetStats setAssignenqueueassume cancelUntil dumpSolver$fVarOrderSolvervalidatevarBumpActivityvarDecayActivityclaBumpActivityclaDecayActivity addClauselbdOfcheckRestartCondition simplifyDBsolve versionIdexecuteSolverOn executeSolver runSolversolveSATsolveSATWithConfigurationexecuteValidatorOnexecuteValidatorvalidateAssignmentdumpAssigmentAsCNFparseCNFinjectClausesFromCNF clausesOf tseitinNumberLpintintseqNumsparseMinisatOutput problemLine commentLines preambleCNF parseClausesdriverUVector ByteArrayIntByteArrayDoubleD:R:VecDouble0 D:R:VecInt0 D:R:Vec[]0BoolMiosDump _dumpedConf_dupmedCNFDesc _dumpedStat MiosStatsDumpTag TerminateS PropagationS ConflictSLearntS BackjumpSRestartS LearningRateSExtraS _nActives_purged _clauseVector _keyVector _numActives _clsVector storeLimit getManagerVarHeap getHeapRootheapidxscheckUniquenessvarRescaleActivityclaActivityThresholdclaRescaleActivity clauseNew removeWatchnewLearntClausesimplifyanalyzeRemovable analyzeFinal propagatereduceDB sortClauses rankWidth activityWidth indexWidthTrueFalse unsafeEnqueue unsafeAssume reportResult skipComments