ToySolver.SAT.PBO

Contents

• The Optimizer type
• Solving
• Extract results
• Configulation

Description

Synopsis

• data Optimizer
• newOptimizer :: Solver -> PBLinSum -> IO Optimizer
• optimize :: Optimizer -> IO ()
• addSolution :: Optimizer -> Model -> IO ()
• getBestSolution :: Optimizer -> IO (Maybe (Model, Integer))
• getBestValue :: Optimizer -> IO (Maybe Integer)
• getBestModel :: Optimizer -> IO (Maybe Model)
• isUnsat :: Optimizer -> IO Bool
• isOptimum :: Optimizer -> IO Bool
• isFinished :: Optimizer -> IO Bool
• data SearchStrategy
  • = LinearSearch
  • | BinarySearch
  • | AdaptiveSearch
  • | UnsatBased
  • | MSU4
  • | BC
  • | BCD
  • | BCD2
• defaultSearchStrategy :: SearchStrategy
• getSearchStrategy :: Optimizer -> IO SearchStrategy
• setSearchStrategy :: Optimizer -> SearchStrategy -> IO ()
• defaultEnableObjFunVarsHeuristics :: Bool
• getEnableObjFunVarsHeuristics :: Optimizer -> IO Bool
• setEnableObjFunVarsHeuristics :: Optimizer -> Bool -> IO ()
• defaultTrialLimitConf :: Int
• getTrialLimitConf :: Optimizer -> IO Int
• setTrialLimitConf :: Optimizer -> Int -> IO ()
• setOnUpdateBestSolution :: Optimizer -> (Model -> Integer -> IO ()) -> IO ()
• setOnUpdateLowerBound :: Optimizer -> (Integer -> IO ()) -> IO ()
• setLogger :: Optimizer -> (String -> IO ()) -> IO ()

The Optimizer type

Solving

Extract results

Configulation