cspsat package

Submodules

• cspsat.csp module
  • Solver
    • Solver.model
    • Solver.stats
    • Solver.minimize
    • Solver.maximize
    • Solver.add()
    • Solver.find()
    • Solver.getStat()
    • Solver.solutions()
    • Solver.solve()
  • Encoder
    • Encoder.defaultFunctionHooks
    • Encoder.defaultConstraintHooks
    • Encoder.delimEq
    • Encoder.delimGe
    • Encoder.delimBit
    • Encoder.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()
  • DirectEncoder
    • DirectEncoder.varToBool()
    • DirectEncoder.encodeInt()
    • DirectEncoder.encodeWsumEq0()
    • DirectEncoder.encodeWsumNe0()
    • DirectEncoder.encodeWsumLe0()
    • DirectEncoder.decode()
    • DirectEncoder.getBlock()
  • OrderEncoder
    • OrderEncoder.varGeK()
    • OrderEncoder.varToBool()
    • OrderEncoder.encodeInt()
    • OrderEncoder.encodeWsumEq0()
    • OrderEncoder.encodeWsumNe0()
    • OrderEncoder.encodeWsumLe0()
    • OrderEncoder.decode()
    • OrderEncoder.getBlock()
  • LogEncoder
    • LogEncoder.varEqK()
    • LogEncoder.varBitK()
    • LogEncoder.getBools()
    • LogEncoder.varToBool()
    • LogEncoder.encodeInt()
    • LogEncoder.encodeWsumEq0()
    • LogEncoder.encodeWsumNe0()
    • LogEncoder.encodeWsumLe0()
    • LogEncoder.decode()
    • LogEncoder.getBlock()
• cspsat.dpll module
  • DPLL
    • DPLL.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()
  • statData
  • status()
  • defaultTimeout
  • getTimeout()
  • setTimeout()
  • solutionsSAT()
  • solveSAT()
  • solutionsCSP()
  • solveCSP()
  • saveSAT()
  • loadSAT()
  • saveDimacs()
  • saveCSP()
  • loadCSP()
• cspsat.hooks module
  • defaultFunctionHook()
  • defaultConstraintHook()
• cspsat.sat module
  • SAT
    • SAT.variables
    • SAT.nclauses
    • SAT.model
    • SAT.stats
    • SAT.commitPosition
    • SAT.buffer
    • SAT.bufLimit
    • SAT.defaultCommand
    • SAT.defaultTempdir
    • SAT.defaultLimit
    • SAT.defaultMaxClauses
    • SAT.nVars()
    • SAT.nClauses()
    • SAT.updateDimacsHeader()
    • SAT.add()
    • SAT.find()
    • SAT.getStat()
    • SAT.addBlock()
    • SAT.commit()
    • SAT.cancel()
    • SAT.solutions()
    • SAT.solve()
• cspsat.util module
  • CspsatException
  • CspsatTimeout
  • Bool
    • Bool.isAux()
  • TRUE
  • FALSE
  • Var
    • Var.isAux()
  • Wsum
    • Wsum.wsum
    • Wsum.c
    • Wsum.variables()
    • Wsum.coef()
    • Wsum.isConstant()
    • Wsum.where()
    • Wsum.mul()
    • Wsum.neg()
    • Wsum.add()
    • Wsum.sub()
    • Wsum.value()
    • Wsum.toExpr()
  • Binary
    • Binary.bins
    • Binary.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()
  • BinaryEquation
    • BinaryEquation.addNum()
    • BinaryEquation.add()
    • BinaryEquation.addMul()
    • BinaryEquation.addPower()
    • BinaryEquation.cmp0()
  • SeqCounter
    • SeqCounter.eqK()
    • SeqCounter.neK()
    • SeqCounter.geK()
    • SeqCounter.gtK()
    • SeqCounter.leK()
    • SeqCounter.ltK()
  • Preprocessor
    • Preprocessor.toWsum()
    • Preprocessor.isBC()
    • Preprocessor.toBC()
    • Preprocessor.toXCNF()

Module contents

cspsatモジュール

注釈

本プログラムは学習用の目的で作成されている． 実用上の問題への適用は想定していない． Copyright (c) 2025-- Naoyuki Tamura Licensed under the MIT License