cspsat package
Submodules
- cspsat.csp module
SolverEncoderEncoder.defaultFunctionHooksEncoder.defaultConstraintHooksEncoder.delimEqEncoder.delimGeEncoder.delimBitEncoder.defInt()Encoder.variables()Encoder.intLb()Encoder.intUb()Encoder.intRange()Encoder.wsumBound()Encoder.getBound()Encoder.varEqK()Encoder.varToBool()Encoder.encodeInt()Encoder.isBoolLike()Encoder.encodeWsumEq0()Encoder.encodeWsumNe0()Encoder.encodeWsumLe0()Encoder.encode()Encoder.put()Encoder.decode()Encoder.toCNF()Encoder.getBlock()
DirectEncoderOrderEncoderLogEncoder
- cspsat.dpll module
DPLLDPLL.nVars()DPLL.nClauses()DPLL.toLit()DPLL.toVar()DPLL.value()DPLL.newVar()DPLL.decisionLevel()DPLL.enqueue()DPLL.assume()DPLL.propagateClause()DPLL.propagate()DPLL.cancel()DPLL.cancelUntil()DPLL.newDecision()DPLL.backtrack()DPLL.getModel()DPLL.search()DPLL.getStat()DPLL.solutions()DPLL.solve()DPLL.info()DPLL.var2repr()DPLL.lit2repr()DPLL.clause2repr()DPLL.assigns2repr()DPLL.decisions2repr()DPLL.watches2repr()DPLL.addInternalClause()DPLL.addDimacsClause()DPLL.toDimacsLit()DPLL.toDimacsLits()DPLL.addClause()DPLL.add()DPLL.load()
- cspsat.functions module
variables()assignments()value()truthTable()isValid()isSat()isEquiv()models()toNF()toNNF()toCNF()toDNF()ge1()le1()eq1()geK()leK()eqK()statDatastatus()defaultTimeoutgetTimeout()setTimeout()solutionsSAT()solveSAT()solutionsCSP()solveCSP()saveSAT()loadSAT()saveDimacs()saveCSP()loadCSP()
- cspsat.hooks module
- cspsat.sat module
SATSAT.variablesSAT.nclausesSAT.modelSAT.statsSAT.commitPositionSAT.bufferSAT.bufLimitSAT.defaultCommandSAT.defaultTempdirSAT.defaultLimitSAT.defaultMaxClausesSAT.nVars()SAT.nClauses()SAT.updateDimacsHeader()SAT.add()SAT.find()SAT.getStat()SAT.addBlock()SAT.commit()SAT.cancel()SAT.solutions()SAT.solve()
- cspsat.util module
CspsatExceptionCspsatTimeoutBoolTRUEFALSEVarWsumBinaryBinary.binsBinary.eqK()Binary.neK()Binary.geK()Binary.gtK()Binary.leK()Binary.ltK()Binary.eq()Binary.ne()Binary.ge()Binary.gt()Binary.le()Binary.lt()Binary.put()Binary.addNum()Binary.add()Binary.addMul()Binary.addPower()Binary.isSimpleSeq()Binary.toSimpleSeq()Binary.toBchain()Binary.toCNF()
BinaryEquationSeqCounterPreprocessor
Module contents
cspsatモジュール
注釈
本プログラムは学習用の目的で作成されている. 実用上の問題への適用は想定していない. Copyright (c) 2025-- Naoyuki Tamura Licensed under the MIT License