ToySolver.SAT.Solver.SLS.ProbSAT

Documentation

data Solver

newSolver :: CNF -> IO Solver

newSolverWeighted :: WCNF -> IO Solver

getNumVars :: Solver -> IO Int

getRandomGen :: Solver -> IO GenIO

setRandomGen :: Solver -> GenIO -> IO ()

getBestSolution :: Solver -> IO (Weight, Model)

getStatistics :: Solver -> IO Statistics

data Options

Constructors

Options

Fields

• optTarget :: !Weight
• optMaxTries :: !Int
• optMaxFlips :: !Int
• optPickClauseWeighted :: Bool

Instances

Eq Options

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

(==) :: Options -> Options -> Bool

(/=) :: Options -> Options -> Bool

Show Options

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

showsPrec :: Int -> Options -> ShowS

show :: Options -> String

showList :: [Options] -> ShowS

Default Options

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

def :: Options

data Callbacks

Constructors

Callbacks

Fields

• cbGenerateInitialSolution :: Solver -> IO Model
• cbOnUpdateBestSolution :: Solver -> Weight -> Model -> IO ()

Instances

Default Callbacks

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

def :: Callbacks

data Statistics

Constructors

Statistics

Fields

• statTotalCPUTime :: !TimeSpec
• statFlips :: !Int
• statFlipsPerSecond :: !Double

Instances

Eq Statistics

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

(==) :: Statistics -> Statistics -> Bool

(/=) :: Statistics -> Statistics -> Bool

Show Statistics

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

showsPrec :: Int -> Statistics -> ShowS

show :: Statistics -> String

showList :: [Statistics] -> ShowS

Default Statistics

Defined in ToySolver.SAT.Solver.SLS.ProbSAT

Methods

def :: Statistics

generateUniformRandomSolution :: Solver -> IO Model

probsat :: Solver -> Options -> Callbacks -> (Double -> Double -> Double) -> IO ()

walksat :: Solver -> Options -> Callbacks -> Double -> IO ()