-- | Simple state transition system:
-- a state is a list of Booleans,
-- a transition is the flip of exactly one bit.
-- Calling the main program with "./State w::Int d::Int"
-- produces the qbf for 'there is a path of length <= 2^d
-- from state False^w to state True^w'.
-- The formula size is linear in w*d.
-- Test cases: "./State 4 2" (satisfiable), "./State 5 2" (unsatisfiable).
-- Output is an element near the middle of the path.
-- You may check the about half the bits are flipped (if the depth bound is tight).
import Prelude hiding ( not, and, or )
import Data.List ( tails )
import Data.Set ( Set )
import qualified Data.Set as S
import Control.Monad ( guard, forM )
import Data.Ix ( range )
main = do
argv <- getArgs
let [ w, d ] = map read argv
result <- Satchmo.Solver.Quantor.solve $ form w d
form :: Int -> Int -> SAT ( Decoder [ Bool ] )
form width depth = do
start <- forM [ 1 .. width ] $ \ n -> constant False
goal <- forM [ 1 .. width ] $ \ n -> constant True
( p, mid ) <- path depth start goal
assert [ p ]
return $ decode mid
-- | is there a path of length <= 2^depth ?
-- If so, the second component is a state from the middle of the path
path :: Int -> [ Boolean ] -> [ Boolean ] -> SAT ( Boolean, [ Boolean ] )
path depth from to =
if depth > 0
mid <- forM [ 1 .. length from ] $ \ _ -> exists
p <- forM [ 1 .. length from ] $ \ _ -> forall
q <- forM [ 1 .. length from ] $ \ _ -> forall
pre <- monadic or [ monadic and [ equals from p , equals mid q ]
, monadic and [ equals mid p , equals to q ]
( post, _ ) <- path (depth - 1) p q
ok <- or [ not pre, post ]
return ( ok, mid )
ok <- monadic or [ onestep from to, equals from to ]
return ( ok, from )
equals :: [ Boolean ] -> [ Boolean ] -> SAT Boolean
equals xs ys = monadic and
$ for ( zip xs ys ) $ \ (x,y) -> fmap not $ xor [x,y]
onestep :: [ Boolean ] -> [ Boolean ] -> SAT Boolean
onestep xs ys = do
changes <- forM ( zip xs ys ) $ \ (x,y) -> xor [x,y]
exactly 1 changes
for = flip map