{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_HADDOCK show-extensions #-}
module ToySolver.SAT.Solver.SLS.ProbSAT
( Solver
, newSolver
, newSolverWeighted
, getNumVars
, getRandomGen
, setRandomGen
, getBestSolution
, getStatistics
, Options (..)
, Callbacks (..)
, Statistics (..)
, generateUniformRandomSolution
, probsat
, walksat
) where
import Prelude hiding (break)
import Control.Exception
import Control.Loop
import Control.Monad
import Control.Monad.Primitive
import Control.Monad.Trans
import Control.Monad.Trans.Except
import Data.Array.Base (unsafeRead, unsafeWrite, unsafeAt)
import Data.Array.IArray
import Data.Array.IO
import Data.Array.Unboxed
import Data.Array.Unsafe
import Data.Bits
import Data.Default.Class
import qualified Data.Foldable as F
import Data.Int
import Data.IORef
import Data.Maybe
import Data.Sequence ((|>))
import qualified Data.Sequence as Seq
import Data.Typeable
import Data.Word
import System.Clock
import qualified System.Random.MWC as Rand
import qualified System.Random.MWC.Distributions as Rand
import qualified ToySolver.FileFormat.CNF as CNF
import ToySolver.Internal.Data.IOURef
import qualified ToySolver.Internal.Data.Vec as Vec
import qualified ToySolver.SAT.Types as SAT
data Solver
= Solver
{ Solver -> Array Var PackedClause
svClauses :: !(Array ClauseId PackedClause)
, Solver -> Array Var Weight
svClauseWeights :: !(Array ClauseId CNF.Weight)
, Solver -> UArray Var Double
svClauseWeightsF :: !(UArray ClauseId Double)
, Solver -> IOUArray Var Int32
svClauseNumTrueLits :: !(IOUArray ClauseId Int32)
, Solver -> IOUArray Var Var
svClauseUnsatClauseIndex :: !(IOUArray ClauseId Int)
, Solver -> UVec Var
svUnsatClauses :: !(Vec.UVec ClauseId)
, Solver -> Array Var (UArray Var Var)
svVarOccurs :: !(Array SAT.Var (UArray Int ClauseId))
, :: !(Array SAT.Var (IOUArray Int Bool))
, Solver -> IOUArray Var Bool
svSolution :: !(IOUArray SAT.Var Bool)
, Solver -> IORef Weight
svObj :: !(IORef CNF.Weight)
, Solver -> IORef GenIO
svRandomGen :: !(IORef Rand.GenIO)
, Solver -> IORef (Weight, Model)
svBestSolution :: !(IORef (CNF.Weight, SAT.Model))
, Solver -> IORef Statistics
svStatistics :: !(IORef Statistics)
}
type ClauseId = Int
type PackedClause = Array Int SAT.Lit
newSolver :: CNF.CNF -> IO Solver
newSolver :: CNF -> IO Solver
newSolver CNF
cnf = do
let wcnf :: WCNF
wcnf =
CNF.WCNF
{ wcnfNumVars :: Var
CNF.wcnfNumVars = CNF -> Var
CNF.cnfNumVars CNF
cnf
, wcnfNumClauses :: Var
CNF.wcnfNumClauses = CNF -> Var
CNF.cnfNumClauses CNF
cnf
, wcnfTopCost :: Weight
CNF.wcnfTopCost = forall a b. (Integral a, Num b) => a -> b
fromIntegral (CNF -> Var
CNF.cnfNumClauses CNF
cnf) forall a. Num a => a -> a -> a
+ Weight
1
, wcnfClauses :: [WeightedClause]
CNF.wcnfClauses = [(Weight
1,PackedClause
c) | PackedClause
c <- CNF -> [PackedClause]
CNF.cnfClauses CNF
cnf]
}
WCNF -> IO Solver
newSolverWeighted WCNF
wcnf
newSolverWeighted :: CNF.WCNF -> IO Solver
newSolverWeighted :: WCNF -> IO Solver
newSolverWeighted WCNF
wcnf = do
let m :: SAT.Var -> Bool
m :: Var -> Bool
m Var
_ = Bool
False
nv :: Var
nv = WCNF -> Var
CNF.wcnfNumVars WCNF
wcnf
IORef Weight
objRef <- forall a. a -> IO (IORef a)
newIORef (Weight
0::Integer)
[(Weight, PackedClause)]
cs <- forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. [Maybe a] -> [a]
catMaybes forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (WCNF -> [WeightedClause]
CNF.wcnfClauses WCNF
wcnf) forall a b. (a -> b) -> a -> b
$ \(Weight
w,PackedClause
pc) -> do
case Clause -> Maybe Clause
SAT.normalizeClause (PackedClause -> Clause
SAT.unpackClause PackedClause
pc) of
Maybe Clause
Nothing -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just [] -> forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' IORef Weight
objRef (Weight
wforall a. Num a => a -> a -> a
+) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return forall a. Maybe a
Nothing
Just Clause
c -> do
let c' :: PackedClause
c' = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, forall (t :: * -> *) a. Foldable t => t a -> Var
length Clause
c forall a. Num a => a -> a -> a
- Var
1) Clause
c
seq :: forall a b. a -> b -> b
seq PackedClause
c' forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return (forall a. a -> Maybe a
Just (Weight
w,PackedClause
c'))
let len :: Var
len = forall (t :: * -> *) a. Foldable t => t a -> Var
length [(Weight, PackedClause)]
cs
clauses :: Array Var PackedClause
clauses = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Weight, PackedClause)]
cs)
weights :: Array ClauseId CNF.Weight
weights :: Array Var Weight
weights = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Weight, PackedClause)]
cs)
weightsF :: UArray ClauseId Double
weightsF :: UArray Var Double
weightsF = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, Var
len forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (Integral a, Num b) => a -> b
fromIntegral forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Weight, PackedClause)]
cs)
(IOArray Var (Seq (Var, Bool))
varOccurs' :: IOArray SAT.Var (Seq.Seq (Int, Bool))) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (Var
1, Var
nv) forall a. Seq a
Seq.empty
IOUArray Var Int32
clauseNumTrueLits <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array Var PackedClause
clauses) Int32
0
IOUArray Var Var
clauseUnsatClauseIndex <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> e -> m (a i e)
newArray (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds Array Var PackedClause
clauses) (-Var
1)
UVec Var
unsatClauses <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ Array Var PackedClause
clauses forall a b. (a -> b) -> a -> b
$ \(Var
c,PackedClause
clause) -> do
let n :: Int32
n = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum [Int32
1 | Var
lit <- forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause, forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit]
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Int32
clauseNumTrueLits Var
c Int32
n
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
n forall a. Eq a => a -> a -> Bool
== Int32
0) forall a b. (a -> b) -> a -> b
$ do
Var
i <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
unsatClauses
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Var
clauseUnsatClauseIndex Var
c Var
i
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
unsatClauses Var
c
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef IORef Weight
objRef ((Array Var Weight
weights forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c) forall a. Num a => a -> a -> a
+)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems PackedClause
clause) forall a b. (a -> b) -> a -> b
$ \Var
lit -> do
let v :: Var
v = Var -> Var
SAT.litVar Var
lit
let b :: Bool
b = forall m. IModel m => m -> Var -> Bool
SAT.evalLit Var -> Bool
m Var
lit
seq :: forall a b. a -> b -> b
seq Bool
b forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v (forall a. Seq a -> a -> Seq a
|> (Var
c,Bool
b))
Array Var (UArray Var Var)
varOccurs <- do
(IOArray Var (UArray Var Var)
arr::IOArray SAT.Var (UArray Int ClauseId)) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
Seq (Var, Bool)
s <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray Var (UArray Var Var)
arr Var
v forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
(i, i) -> [e] -> a i e
listArray (Var
0, forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s forall a. Num a => a -> a -> a
- Var
1) (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s))
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray Var (UArray Var Var)
arr
Array Var (IOUArray Var Bool)
varOccursState <- do
(IOArray Var (IOUArray Var Bool)
arr::IOArray SAT.Var (IOUArray Int Bool)) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1, Var
nv)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1 .. Var
nv] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
Seq (Var, Bool)
s <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOArray Var (Seq (Var, Bool))
varOccurs' Var
v
IOUArray Var Bool
ss <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, forall a. Seq a -> Var
Seq.length Seq (Var, Bool)
s forall a. Num a => a -> a -> a
- Var
1)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a b. [a] -> [b] -> [(a, b)]
zip [Var
0..] (forall (t :: * -> *) a. Foldable t => t a -> [a]
F.toList Seq (Var, Bool)
s)) forall a b. (a -> b) -> a -> b
$ \(Var
j,(Var, Bool)
a) -> forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Bool
ss Var
j (forall a b. (a, b) -> b
snd (Var, Bool)
a)
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOArray Var (IOUArray Var Bool)
arr Var
v IOUArray Var Bool
ss
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOArray Var (IOUArray Var Bool)
arr
IOUArray Var Bool
solution <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> [e] -> m (a i e)
newListArray (Var
1, Var
nv) forall a b. (a -> b) -> a -> b
$ [forall m. IModel m => m -> Var -> Bool
SAT.evalVar Var -> Bool
m Var
v | Var
v <- [Var
1..Var
nv]]
Weight
bestObj <- forall a. IORef a -> IO a
readIORef IORef Weight
objRef
Model
bestSol <- forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze IOUArray Var Bool
solution
IORef (Weight, Model)
bestSolution <- forall a. a -> IO (IORef a)
newIORef (Weight
bestObj, Model
bestSol)
IORef (Gen RealWorld)
randGen <- forall a. a -> IO (IORef a)
newIORef forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall (m :: * -> *). PrimMonad m => m (Gen (PrimState m))
Rand.create
IORef Statistics
stat <- forall a. a -> IO (IORef a)
newIORef forall a. Default a => a
def
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$
Solver
{ svClauses :: Array Var PackedClause
svClauses = Array Var PackedClause
clauses
, svClauseWeights :: Array Var Weight
svClauseWeights = Array Var Weight
weights
, svClauseWeightsF :: UArray Var Double
svClauseWeightsF = UArray Var Double
weightsF
, svClauseNumTrueLits :: IOUArray Var Int32
svClauseNumTrueLits = IOUArray Var Int32
clauseNumTrueLits
, svClauseUnsatClauseIndex :: IOUArray Var Var
svClauseUnsatClauseIndex = IOUArray Var Var
clauseUnsatClauseIndex
, svUnsatClauses :: UVec Var
svUnsatClauses = UVec Var
unsatClauses
, svVarOccurs :: Array Var (UArray Var Var)
svVarOccurs = Array Var (UArray Var Var)
varOccurs
, svVarOccursState :: Array Var (IOUArray Var Bool)
svVarOccursState = Array Var (IOUArray Var Bool)
varOccursState
, svSolution :: IOUArray Var Bool
svSolution = IOUArray Var Bool
solution
, svObj :: IORef Weight
svObj = IORef Weight
objRef
, svRandomGen :: IORef GenIO
svRandomGen = IORef (Gen RealWorld)
randGen
, svBestSolution :: IORef (Weight, Model)
svBestSolution = IORef (Weight, Model)
bestSolution
, svStatistics :: IORef Statistics
svStatistics = IORef Statistics
stat
}
flipVar :: Solver -> SAT.Var -> IO ()
flipVar :: Solver -> Var -> IO ()
flipVar Solver
solver Var
v = forall a. IO a -> IO a
mask_ forall a b. (a -> b) -> a -> b
$ do
let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
occursState :: IOUArray Var Bool
occursState = Solver -> Array Var (IOUArray Var Bool)
svVarOccursState Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq IOUArray Var Bool
occursState forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *) a. Monad m => a -> m a
return ()
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray (Solver -> IOUArray Var Bool
svSolution Solver
solver) Var
v Bool -> Bool
not
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ \(Var
j,!Var
c) -> do
Bool
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead IOUArray Var Bool
occursState Var
j
Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite IOUArray Var Bool
occursState Var
j (Bool -> Bool
not Bool
b)
if Bool
b then do
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c (Int32
nforall a. Num a => a -> a -> a
-Int32
1)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nforall a. Eq a => a -> a -> Bool
==Int32
1) forall a b. (a -> b) -> a -> b
$ do
Var
i <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
c
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c Var
i
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> Array Var Weight
svClauseWeights Solver
solver) Var
c)
else do
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c (Int32
nforall a. Num a => a -> a -> a
+Int32
1)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int32
nforall a. Eq a => a -> a -> Bool
==Int32
0) forall a b. (a -> b) -> a -> b
$ do
Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
Var
i <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Var
i forall a. Eq a => a -> a -> Bool
== Var
sforall a. Num a => a -> a -> a
-Var
1) forall a b. (a -> b) -> a -> b
$ do
let i2 :: Var
i2 = Var
sforall a. Num a => a -> a -> a
-Var
1
Var
c2 <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i2
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i2 Var
c
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> e -> IO ()
Vec.unsafeWrite (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
i Var
c2
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> e -> m ()
unsafeWrite (Solver -> IOUArray Var Var
svClauseUnsatClauseIndex Solver
solver) Var
c2 Var
i
Var
_ <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO e
Vec.unsafePop (Solver -> UVec Var
svUnsatClauses Solver
solver)
forall a. IORef a -> (a -> a) -> IO ()
modifyIORef' (Solver -> IORef Weight
svObj Solver
solver) (forall a. Num a => a -> a -> a
subtract (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> Array Var Weight
svClauseWeights Solver
solver) Var
c))
forall (m :: * -> *) a. Monad m => a -> m a
return ()
setSolution :: SAT.IModel m => Solver -> m -> IO ()
setSolution :: forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver m
m = do
(Var, Var)
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> m (i, i)
getBounds (Solver -> IOUArray Var Bool
svSolution Solver
solver)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ (forall a. Ix a => (a, a) -> [a]
range (Var, Var)
b) forall a b. (a -> b) -> a -> b
$ \Var
v -> do
Bool
val <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray (Solver -> IOUArray Var Bool
svSolution Solver
solver) Var
v
let val' :: Bool
val' = forall m. IModel m => m -> Var -> Bool
SAT.evalVar m
m Var
v
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Bool
val forall a. Eq a => a -> a -> Bool
== Bool
val') forall a b. (a -> b) -> a -> b
$ do
Solver -> Var -> IO ()
flipVar Solver
solver Var
v
getNumVars :: Solver -> IO Int
getNumVars :: Solver -> IO Var
getNumVars Solver
solver = forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. Ix a => (a, a) -> Var
rangeSize forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver)
getRandomGen :: Solver -> IO Rand.GenIO
getRandomGen :: Solver -> IO GenIO
getRandomGen Solver
solver = forall a. IORef a -> IO a
readIORef (Solver -> IORef GenIO
svRandomGen Solver
solver)
setRandomGen :: Solver -> Rand.GenIO -> IO ()
setRandomGen :: Solver -> GenIO -> IO ()
setRandomGen Solver
solver GenIO
gen = forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef GenIO
svRandomGen Solver
solver) GenIO
gen
getBestSolution :: Solver -> IO (CNF.Weight, SAT.Model)
getBestSolution :: Solver -> IO (Weight, Model)
getBestSolution Solver
solver = forall a. IORef a -> IO a
readIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver)
getStatistics :: Solver -> IO Statistics
getStatistics :: Solver -> IO Statistics
getStatistics Solver
solver = forall a. IORef a -> IO a
readIORef (Solver -> IORef Statistics
svStatistics Solver
solver)
{-# INLINE getMakeValue #-}
getMakeValue :: Solver -> SAT.Var -> IO Double
getMakeValue :: Solver -> Var -> IO Double
getMakeValue Solver
solver Var
v = do
let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
(Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
lb forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
ub forall a b. (a -> b) -> a -> b
$
forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub Double
0 forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
let c :: Var
c = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Int32
n forall a. Eq a => a -> a -> Bool
== Int32
0 then (Double
r forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> UArray Var Double
svClauseWeightsF Solver
solver) Var
c) else Double
r
{-# INLINE getBreakValue #-}
getBreakValue :: Solver -> SAT.Var -> IO Double
getBreakValue :: Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v = do
let occurs :: UArray Var Var
occurs = Solver -> Array Var (UArray Var Var)
svVarOccurs Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
occursState :: IOUArray Var Bool
occursState = Solver -> Array Var (IOUArray Var Bool)
svVarOccursState Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
v
(Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds UArray Var Var
occurs
seq :: forall a b. a -> b -> b
seq UArray Var Var
occurs forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq IOUArray Var Bool
occursState forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
lb forall a b. (a -> b) -> a -> b
$ seq :: forall a b. a -> b -> b
seq Var
ub forall a b. (a -> b) -> a -> b
$
forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub Double
0 forall a b. (a -> b) -> a -> b
$ \ !Double
r !Var
i -> do
Bool
b <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead IOUArray Var Bool
occursState Var
i
if Bool
b then do
let c :: Var
c = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt UArray Var Var
occurs Var
i
Int32
n <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> Var -> m e
unsafeRead (Solver -> IOUArray Var Int32
svClauseNumTrueLits Solver
solver) Var
c
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! if Int32
nforall a. Eq a => a -> a -> Bool
==Int32
1 then (Double
r forall a. Num a => a -> a -> a
+ forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt (Solver -> UArray Var Double
svClauseWeightsF Solver
solver) Var
c) else Double
r
else
forall (m :: * -> *) a. Monad m => a -> m a
return Double
r
data Options
= Options
{ Options -> Weight
optTarget :: !CNF.Weight
, Options -> Var
optMaxTries :: !Int
, Options -> Var
optMaxFlips :: !Int
, Options -> Bool
optPickClauseWeighted :: Bool
}
deriving (Options -> Options -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Options -> Options -> Bool
$c/= :: Options -> Options -> Bool
== :: Options -> Options -> Bool
$c== :: Options -> Options -> Bool
Eq, Var -> Options -> ShowS
[Options] -> ShowS
Options -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Options] -> ShowS
$cshowList :: [Options] -> ShowS
show :: Options -> String
$cshow :: Options -> String
showsPrec :: Var -> Options -> ShowS
$cshowsPrec :: Var -> Options -> ShowS
Show)
instance Default Options where
def :: Options
def =
Options
{ optTarget :: Weight
optTarget = Weight
0
, optMaxTries :: Var
optMaxTries = Var
1
, optMaxFlips :: Var
optMaxFlips = Var
100000
, optPickClauseWeighted :: Bool
optPickClauseWeighted = Bool
False
}
data Callbacks
= Callbacks
{ Callbacks -> Solver -> IO Model
cbGenerateInitialSolution :: Solver -> IO SAT.Model
, Callbacks -> Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution :: Solver -> CNF.Weight -> SAT.Model -> IO ()
}
instance Default Callbacks where
def :: Callbacks
def =
Callbacks
{ cbGenerateInitialSolution :: Solver -> IO Model
cbGenerateInitialSolution = Solver -> IO Model
generateUniformRandomSolution
, cbOnUpdateBestSolution :: Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution = \Solver
_ Weight
_ Model
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return ()
}
data Statistics
= Statistics
{ Statistics -> TimeSpec
statTotalCPUTime :: !TimeSpec
, Statistics -> Var
statFlips :: !Int
, Statistics -> Double
statFlipsPerSecond :: !Double
}
deriving (Statistics -> Statistics -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Statistics -> Statistics -> Bool
$c/= :: Statistics -> Statistics -> Bool
== :: Statistics -> Statistics -> Bool
$c== :: Statistics -> Statistics -> Bool
Eq, Var -> Statistics -> ShowS
[Statistics] -> ShowS
Statistics -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Statistics] -> ShowS
$cshowList :: [Statistics] -> ShowS
show :: Statistics -> String
$cshow :: Statistics -> String
showsPrec :: Var -> Statistics -> ShowS
$cshowsPrec :: Var -> Statistics -> ShowS
Show)
instance Default Statistics where
def :: Statistics
def =
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
0
, statFlips :: Var
statFlips = Var
0
, statFlipsPerSecond :: Double
statFlipsPerSecond = Double
0
}
generateUniformRandomSolution :: Solver -> IO SAT.Model
generateUniformRandomSolution :: Solver -> IO Model
generateUniformRandomSolution Solver
solver = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
Var
n <- Solver -> IO Var
getNumVars Solver
solver
(IOUArray Var Bool
a :: IOUArray Int Bool) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
1,Var
n)
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Var
1..Var
n] forall a b. (a -> b) -> a -> b
$ \Var
v -> do
Bool
b <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen RealWorld
gen
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Bool
a Var
v Bool
b
forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
unsafeFreeze IOUArray Var Bool
a
checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution :: Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb = do
(Weight, Model)
best <- forall a. IORef a -> IO a
readIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver)
Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
< forall a b. (a, b) -> a
fst (Weight, Model)
best) forall a b. (a -> b) -> a -> b
$ do
Model
sol <- forall i (a :: * -> * -> *) e (m :: * -> *) (b :: * -> * -> *).
(Ix i, MArray a e m, IArray b e) =>
a i e -> m (b i e)
freeze (Solver -> IOUArray Var Bool
svSolution Solver
solver)
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef (Weight, Model)
svBestSolution Solver
solver) (Weight
obj, Model
sol)
Callbacks -> Solver -> Weight -> Model -> IO ()
cbOnUpdateBestSolution Callbacks
cb Solver
solver Weight
obj Model
sol
pickClause :: Solver -> Options -> IO PackedClause
pickClause :: Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
if Options -> Bool
optPickClauseWeighted Options
opt then do
Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
let f :: Var -> Weight -> IO Var
f !Var
j !Weight
x = do
Var
c <- forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.read (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
j
let w :: Weight
w = Solver -> Array Var Weight
svClauseWeights Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c
if Weight
x forall a. Ord a => a -> a -> Bool
< Weight
w then
forall (m :: * -> *) a. Monad m => a -> m a
return Var
c
else
Var -> Weight -> IO Var
f (Var
j forall a. Num a => a -> a -> a
+ Var
1) (Weight
x forall a. Num a => a -> a -> a
- Weight
w)
Weight
x <- forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand Weight
obj Gen RealWorld
gen
Var
c <- Var -> Weight -> IO Var
f Var
0 Weight
x
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Solver -> Array Var PackedClause
svClauses Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
c)
else do
Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
Var
j <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
0, Var
s forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
gen
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM (Solver -> Array Var PackedClause
svClauses Solver
solver forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
!) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.read (Solver -> UVec Var
svUnsatClauses Solver
solver) Var
j
rand :: PrimMonad m => Integer -> Rand.Gen (PrimState m) -> m Integer
rand :: forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand Weight
n Gen (PrimState m)
gen
| Weight
n forall a. Ord a => a -> a -> Bool
<= forall a. Integral a => a -> Weight
toInteger (forall a. Bounded a => a
maxBound :: Word32) = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM forall a. Integral a => a -> Weight
toInteger forall a b. (a -> b) -> a -> b
$ forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Word32
0, forall a b. (Integral a, Num b) => a -> b
fromIntegral Weight
n forall a. Num a => a -> a -> a
- Word32
1 :: Word32) Gen (PrimState m)
gen
| Bool
otherwise = do
Weight
a <- forall (m :: * -> *).
PrimMonad m =>
Weight -> Gen (PrimState m) -> m Weight
rand (Weight
n forall a. Bits a => a -> Var -> a
`shiftR` Var
32) Gen (PrimState m)
gen
(Word32
b::Word32) <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
Gen (PrimState m) -> m a
Rand.uniform Gen (PrimState m)
gen
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ (Weight
a forall a. Bits a => a -> Var -> a
`shiftL` Var
32) forall a. Bits a => a -> a -> a
.|. forall a. Integral a => a -> Weight
toInteger Word32
b
data Finished = Finished
deriving (Var -> Finished -> ShowS
[Finished] -> ShowS
Finished -> String
forall a.
(Var -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Finished] -> ShowS
$cshowList :: [Finished] -> ShowS
show :: Finished -> String
$cshow :: Finished -> String
showsPrec :: Var -> Finished -> ShowS
$cshowsPrec :: Var -> Finished -> ShowS
Show, Typeable)
instance Exception Finished
probsat :: Solver -> Options -> Callbacks -> (Double -> Double -> Double) -> IO ()
probsat :: Solver
-> Options -> Callbacks -> (Double -> Double -> Double) -> IO ()
probsat Solver
solver Options
opt Callbacks
cb Double -> Double -> Double
f = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
let maxClauseLen :: Var
maxClauseLen =
if forall a. Ix a => (a, a) -> Var
rangeSize (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds (Solver -> Array Var PackedClause
svClauses Solver
solver)) forall a. Eq a => a -> a -> Bool
== Var
0
then Var
0
else forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (forall a. Ix a => (a, a) -> Var
rangeSize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds) forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e i. (IArray a e, Ix i) => a i e -> [e]
elems (Solver -> Array Var PackedClause
svClauses Solver
solver)
(IOUArray Var Double
wbuf :: IOUArray Int Double) <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
(i, i) -> m (a i e)
newArray_ (Var
0, Var
maxClauseLenforall a. Num a => a -> a -> a
-Var
1)
IOURef Double
wsumRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Double
0 :: Double)
let pickVar :: PackedClause -> IO SAT.Var
pickVar :: PackedClause -> IO Var
pickVar PackedClause
c = do
forall a. MArray IOUArray a IO => IOURef a -> a -> IO ()
writeIOURef IOURef Double
wsumRef Double
0
forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ PackedClause
c forall a b. (a -> b) -> a -> b
$ \(Var
k,Var
lit) -> do
let v :: Var
v = Var -> Var
SAT.litVar Var
lit
Double
m <- Solver -> Var -> IO Double
getMakeValue Solver
solver Var
v
Double
b <- Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v
let w :: Double
w = Double -> Double -> Double
f Double
m Double
b
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray IOUArray Var Double
wbuf Var
k Double
w
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Double
wsumRef (forall a. Num a => a -> a -> a
+Double
w)
Double
wsum <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Double
wsumRef
let go :: Int -> Double -> IO Int
go :: Var -> Double -> IO Var
go !Var
k !Double
a = do
if Bool -> Bool
not (forall a. Ix a => (a, a) -> a -> Bool
inRange (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c) Var
k) then do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall a b. (a, b) -> b
snd (forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c)
else do
Double
w <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray IOUArray Var Double
wbuf Var
k
if Double
a forall a. Ord a => a -> a -> Bool
<= Double
w then
forall (m :: * -> *) a. Monad m => a -> m a
return Var
k
else
Var -> Double -> IO Var
go (Var
k forall a. Num a => a -> a -> a
+ Var
1) (Double
a forall a. Num a => a -> a -> a
- Double
w)
Var
k <- Var -> Double -> IO Var
go Var
0 forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Double
0, Double
wsum) Gen RealWorld
gen
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
k)
TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
IOURef Var
flipsRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Var
0::Int)
let body :: IO ()
body = do
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxTries Options
opt) forall a b. (a -> b) -> a -> b
$ do
Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) forall a b. (a -> b) -> a -> b
$ do
Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s forall a. Eq a => a -> a -> Bool
== Var
0) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
Solver -> Var -> IO ()
flipVar Solver
solver Var
v
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef forall a. Integral a => a -> a
inc
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
IO ()
body forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> forall (m :: * -> *) a. Monad m => a -> m a
return ())
TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
Var
flips <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Var
flipsRef
let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
totalCPUTimeSec :: Double
totalCPUTimeSec = forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) forall a. Fractional a => a -> a -> a
/ Double
10forall a b. (Num a, Integral b) => a -> b -> a
^(Var
9::Int)
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) forall a b. (a -> b) -> a -> b
$
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
, statFlips :: Var
statFlips = Var
flips
, statFlipsPerSecond :: Double
statFlipsPerSecond = forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
}
forall (m :: * -> *) a. Monad m => a -> m a
return ()
walksat :: Solver -> Options -> Callbacks -> Double -> IO ()
walksat :: Solver -> Options -> Callbacks -> Double -> IO ()
walksat Solver
solver Options
opt Callbacks
cb Double
p = do
Gen RealWorld
gen <- Solver -> IO GenIO
getRandomGen Solver
solver
(UVec Var
buf :: Vec.UVec SAT.Var) <- forall (a :: * -> * -> *) e. MArray a e IO => IO (GenericVec a e)
Vec.new
let pickVar :: PackedClause -> IO SAT.Var
pickVar :: PackedClause -> IO Var
pickVar PackedClause
c = do
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf
let (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds PackedClause
c
Either Var ()
r <- forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT forall a b. (a -> b) -> a -> b
$ do
Double
_ <- forall a (m :: * -> *) b.
(Num a, Eq a, Monad m) =>
a -> a -> b -> (b -> a -> m b) -> m b
numLoopState Var
lb Var
ub (Double
1.0forall a. Fractional a => a -> a -> a
/Double
0.0) forall a b. (a -> b) -> a -> b
$ \ !Double
b0 !Var
i -> do
let v :: Var
v = Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
Double
b <- forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ Solver -> Var -> IO Double
getBreakValue Solver
solver Var
v
if Double
b forall a. Ord a => a -> a -> Bool
<= Double
0 then
forall (m :: * -> *) e a. Monad m => e -> ExceptT e m a
throwE Var
v
else if Double
b forall a. Ord a => a -> a -> Bool
< Double
b0 then do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> IO ()
Vec.clear UVec Var
buf forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b
else if Double
b forall a. Eq a => a -> a -> Bool
== Double
b0 then do
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift forall a b. (a -> b) -> a -> b
$ forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> e -> IO ()
Vec.push UVec Var
buf Var
v
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
else do
forall (m :: * -> *) a. Monad m => a -> m a
return Double
b0
forall (m :: * -> *) a. Monad m => a -> m a
return ()
case Either Var ()
r of
Left Var
v -> forall (m :: * -> *) a. Monad m => a -> m a
return Var
v
Right ()
_ -> do
Bool
flag <- forall g (m :: * -> *). StatefulGen g m => Double -> g -> m Bool
Rand.bernoulli Double
p Gen RealWorld
gen
if Bool
flag then do
Var
i <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
lb,Var
ub) Gen RealWorld
gen
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! Var -> Var
SAT.litVar (PackedClause
c forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> i -> e
! Var
i)
else do
Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize UVec Var
buf
if Var
s forall a. Eq a => a -> a -> Bool
== Var
1 then
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead UVec Var
buf Var
0
else do
Var
i <- forall a (m :: * -> *).
(Variate a, PrimMonad m) =>
(a, a) -> Gen (PrimState m) -> m a
Rand.uniformR (Var
0, Var
s forall a. Num a => a -> a -> a
- Var
1) Gen RealWorld
gen
forall (a :: * -> * -> *) e.
MArray a e IO =>
GenericVec a e -> Var -> IO e
Vec.unsafeRead UVec Var
buf Var
i
TimeSpec
startCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
IOURef Var
flipsRef <- forall a. MArray IOUArray a IO => a -> IO (IOURef a)
newIOURef (Var
0::Int)
let body :: IO ()
body = do
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxTries Options
opt) forall a b. (a -> b) -> a -> b
$ do
Model
sol <- Callbacks -> Solver -> IO Model
cbGenerateInitialSolution Callbacks
cb Solver
solver
forall m. IModel m => Solver -> m -> IO ()
setSolution Solver
solver Model
sol
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
forall (m :: * -> *) a. Applicative m => Var -> m a -> m ()
replicateM_ (Options -> Var
optMaxFlips Options
opt) forall a b. (a -> b) -> a -> b
$ do
Var
s <- forall (a :: * -> * -> *) e. GenericVec a e -> IO Var
Vec.getSize (Solver -> UVec Var
svUnsatClauses Solver
solver)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var
s forall a. Eq a => a -> a -> Bool
== Var
0) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
Weight
obj <- forall a. IORef a -> IO a
readIORef (Solver -> IORef Weight
svObj Solver
solver)
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Weight
obj forall a. Ord a => a -> a -> Bool
<= Options -> Weight
optTarget Options
opt) forall a b. (a -> b) -> a -> b
$ forall a e. Exception e => e -> a
throw Finished
Finished
PackedClause
c <- Solver -> Options -> IO PackedClause
pickClause Solver
solver Options
opt
Var
v <- PackedClause -> IO Var
pickVar PackedClause
c
Solver -> Var -> IO ()
flipVar Solver
solver Var
v
forall a. MArray IOUArray a IO => IOURef a -> (a -> a) -> IO ()
modifyIOURef IOURef Var
flipsRef forall a. Integral a => a -> a
inc
Solver -> Callbacks -> IO ()
checkCurrentSolution Solver
solver Callbacks
cb
IO ()
body forall e a. Exception e => IO a -> (e -> IO a) -> IO a
`catch` (\(Finished
_::Finished) -> forall (m :: * -> *) a. Monad m => a -> m a
return ())
TimeSpec
endCPUTime <- Clock -> IO TimeSpec
getTime Clock
ProcessCPUTime
Var
flips <- forall a. MArray IOUArray a IO => IOURef a -> IO a
readIOURef IOURef Var
flipsRef
let totalCPUTime :: TimeSpec
totalCPUTime = TimeSpec
endCPUTime TimeSpec -> TimeSpec -> TimeSpec
`diffTimeSpec` TimeSpec
startCPUTime
totalCPUTimeSec :: Double
totalCPUTimeSec = forall a b. (Integral a, Num b) => a -> b
fromIntegral (TimeSpec -> Weight
toNanoSecs TimeSpec
totalCPUTime) forall a. Fractional a => a -> a -> a
/ Double
10forall a b. (Num a, Integral b) => a -> b -> a
^(Var
9::Int)
forall a. IORef a -> a -> IO ()
writeIORef (Solver -> IORef Statistics
svStatistics Solver
solver) forall a b. (a -> b) -> a -> b
$
Statistics
{ statTotalCPUTime :: TimeSpec
statTotalCPUTime = TimeSpec
totalCPUTime
, statFlips :: Var
statFlips = Var
flips
, statFlipsPerSecond :: Double
statFlipsPerSecond = forall a b. (Integral a, Num b) => a -> b
fromIntegral Var
flips forall a. Fractional a => a -> a -> a
/ Double
totalCPUTimeSec
}
forall (m :: * -> *) a. Monad m => a -> m a
return ()
{-# INLINE modifyArray #-}
modifyArray :: (MArray a e m, Ix i) => a i e -> i -> (e -> e) -> m ()
modifyArray :: forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> (e -> e) -> m ()
modifyArray a i e
a i
i e -> e
f = do
e
e <- forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> m e
readArray a i e
a i
i
forall (a :: * -> * -> *) e (m :: * -> *) i.
(MArray a e m, Ix i) =>
a i e -> i -> e -> m ()
writeArray a i e
a i
i (e -> e
f e
e)
{-# INLINE forAssocsM_ #-}
forAssocsM_ :: (IArray a e, Monad m) => a Int e -> ((Int,e) -> m ()) -> m ()
forAssocsM_ :: forall (a :: * -> * -> *) e (m :: * -> *).
(IArray a e, Monad m) =>
a Var e -> ((Var, e) -> m ()) -> m ()
forAssocsM_ a Var e
a (Var, e) -> m ()
f = do
let (Var
lb,Var
ub) = forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> (i, i)
bounds a Var e
a
forall a (m :: * -> *).
(Num a, Ord a, Monad m) =>
a -> a -> (a -> m ()) -> m ()
numLoop Var
lb Var
ub forall a b. (a -> b) -> a -> b
$ \Var
i ->
(Var, e) -> m ()
f (Var
i, forall (a :: * -> * -> *) e i.
(IArray a e, Ix i) =>
a i e -> Var -> e
unsafeAt a Var e
a Var
i)
{-# INLINE inc #-}
inc :: Integral a => a -> a
inc :: forall a. Integral a => a -> a
inc a
a = a
aforall a. Num a => a -> a -> a
+a
1