Inconsistent result on assertless program.

[Xwtek]

I discovered a bug on Ersatz when dealing with a program without assert.

main :: IO ()
main = do
    (_, out) <- solveWith @_ @Maybe @_ @[Bit] minisat $ do
        b1 <- exists @Bit
        b2 <- exists
        return [b1, b2, b1 || b2, b1 && b2]
    print out

Currently, this outputs [False, False, True, False], which contradicts the fact that the third bool can only be True if the first or the second bool is also True. The problem disappears when using cryptominisat5. The problem might be caused bu the fact minisat does not give any value on an unconstrained bit, but cryptominisat5 does, as the litMap (i.e. the second output of the solver function) of minisat is fromList [], but the litMap of cryptominisat5 is fromList [(1, True), (2, False), (3, False)]

[Xwtek]

I actually know how to fix it... but it results in breaking change as it would change the type signature of decode, so I'm not sure if I should proceed or not

[RyanGlScott]

What is the solution that you have in mind, @Xwtek?

I did some investigation into the code, and I suspect that this code in the Codec Literal instance is the culprit:

https://github.com/ekmett/ersatz/blob/49edb43a8d64f2caecd056fb8f63e91962edf468/src/Ersatz/Codec.hs#L39

In this code, if solutionLiteral fails to map a Literal to Just b (for some Bool b), then it will fall back on pure False <|> pure True. When dealing with Maybe's MonadPlus instance, this means that every unconstrained Literal will map to Just False. This is almost surely not what we want, since that would mean that both Literal 2 and Literal (-2) would map to Just False, even though one of these should map to Just True. (See also #60, which is in similar territory.)

One possible solution would be to make the default aware of the signedness of the Literal. That is, do something like this:

diff --git a/src/Ersatz/Codec.hs b/src/Ersatz/Codec.hs
index 1ea7b52..097ab43 100644
--- a/src/Ersatz/Codec.hs
+++ b/src/Ersatz/Codec.hs
@@ -36,7 +36,7 @@ class Codec a where

 instance Codec Literal where
   type Decoded Literal = Bool
-  decode s a = maybe (pure False <|> pure True) pure (solutionLiteral s a)
+  decode s a = maybe (if literalId a >= 0 then pure True <|> pure False else pure False <|> pure True) pure (solutionLiteral s a)
   encode True  = literalTrue
   encode False = literalFalse

That suffices to fix both #60 and this issue, although I'm unclear if there would be any unintended consequences of doing this.

[Xwtek]

There seems to be a related problem (and I believe is the cause) on Codec instance on a tuple (or any cartesian product), as it assumes that each item tuple is independent, while it's not the case.

main :: IO ()
main = do
    print =<< solveWith @_ @[] minisat mainBody

mainBody :: (MonadSAT s m) => m (Literal, Literal)
mainBody = do
    b <- exists
    bLit <- runBit b
    return (bLit, bLit)

This fact is hidden by #61, where the Codec instance of Bit only uses Maybe as the MonadPlus parameter, essentially only picking the first result.

[Xwtek]

So, what I have in mind is a choice between three options:

1. Give up on MonadPlus thing. It's not like minisat are exhausting the possible solutions anyway.
2. Change the type of decode to a -> StateT Solution f a, so that an evaluation of a literal "updates" the Solution.
3. Change the type of decode to a -> Solution -> a and "pregenerate" the Solution by making solutionFrom return a f Solution

Changing the Codec Literal solution might work, but unless the Codec Bit is also changed, it will probably be equivalent to assuming that an unassigned literal is False because in Codec Bit, the MonadPlus used when using Codec Literal is Maybe

[jwaldmann]

(for each of the three) what would change for users of the library (that have Codec instances for their data types)?

[Xwtek]

For the first solution, I think this option is the most principled way because it reflects the fact that SAT doesn't exhaustively list all the possible solutions to the problem, but it's also the most breaking change, as pretty much any program would break and must be changed as even solveWith now just returns Maybe (Decoded a) The second and third solution only affects the user when the user manually interacts with Codec like implementing it in a way other than using generics. The third seems to be simpler and more intuitive to write a Codec instance for. The second option requires a monadic interface to get the value of a Literal and to decode generally. I think that we should forget the second option.

[jwaldmann]

concrete example for solveWith:

  (status, result) <- liftIO $ solveWith minisat $  ...
  case (status, result) of     (Satisfied, Just p) -> do ...

https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/src/Kachinuki/SAT.hs#L67

the pattern match fixes the MonadPlus instance, and would still work? while the more modern solveWith @_ @Maybe @_ @[Bit] would not?

concrete example for decode:

instance KnownNat w => Codec (N w) where  
 ...
   decode s (N xs) =   
     ( fromIntegral . length . takeWhile id )   <$> mapM (decode s) xs

https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/blob/master/src/Ersatz/Order.hs#L44

if you "just" change the monad, then that code would still be fine (since it does not mention the type)?

whatever you do .. do it before the teaching term starts, so I can adapt .. I was just checking that the example (at start of my lecture) uses old-style implicit types https://www.imn.htwk-leipzig.de/~waldmann/edu/ws22/cp/folien/#(22)

[RyanGlScott]

I am also skeptical of how useful it is to make decode work in an arbitrary MonadPlus f, considering that instantiating f to [] doesn't produce the expected results most of the time. For that matter, I'm not sure if it always produces the expected results when f is instantiated to Maybe. If you write:

main :: IO ()
main = do
    r <- solveWith @_ @Maybe @_ @[Bit] minisat $ do
        b <- exists
        assert $ (true :: Bit) === false -- Contradiction
        pure [b]
    print r

Then you'll get:

(Unsatisfied,Just [False])

It seems a bit strange for the assignment to return Just when the program is unsatisfiable... but in any case, I'll ignore that technical detail for now. For the rest of this comment, let's assume that we are only dealing with Satisfiable programs with f := Maybe.

---

Another way that we could approach this problem is by changing the implementation of solutionFrom to map all unconstrained literals to a constant. Something like this:

diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs
index 68eb3de..42023e2 100644
--- a/src/Ersatz/Problem.hs
+++ b/src/Ersatz/Problem.hs
@@ -28,6 +28,7 @@ module Ersatz.Problem
   , literalExists
   , assertFormula
   , generateLiteral
+  , satClauses
   -- * QSAT
   , QSAT(QSAT)
   , HasQSAT(..)
diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs
index 5bce748..810327f 100644
--- a/src/Ersatz/Solution.hs
+++ b/src/Ersatz/Solution.hs
@@ -17,6 +17,7 @@ import Control.Lens
 import qualified Data.HashMap.Lazy as HashMap
 import Data.IntMap (IntMap)
 import qualified Data.IntMap.Strict as IntMap
+import qualified Data.IntSet as IntSet
 import Data.Ix
 import Ersatz.Internal.Literal
 import Ersatz.Problem
@@ -30,14 +31,21 @@ data Solution = Solution
 solutionFrom :: HasSAT s => IntMap Bool -> s -> Solution
 solutionFrom litMap qbf = Solution lookupLit lookupSN
   where
-    lookupLit l | i >= 0    = IntMap.lookup i litMap
-                | otherwise = not <$> IntMap.lookup (-i) litMap
+    lookupLit l
+      | IntSet.member i constrainedSet
+      = if i >= 0
+        then IntMap.lookup i litMap
+        else not <$> IntMap.lookup (-i) litMap
+      | otherwise -- Unconstrained literal, use an arbitrary assignment
+      = Just False
       where i = literalId l

     lookupSN sn = lookupLit =<< HashMap.lookup sn snMap

     snMap = qbf^.stableMap

+    constrainedSet = IntSet.unions $ satClauses qbf
+
 data Result
   = Unsolved
   | Unsatisfied

This wouldn't require any breaking changes to the API to accomplish. (Separately from this, we could consider making decodeWith always use Maybe instead of an arbitrary MonadPlus, but it's not strictly required.) What do you think of this idea?

[Xwtek]

If we change solutionFrom into that, won't the lookupLit always return Just? We might be as well as making lookupLit return the value directly without Maybe wrapping. Also, this will essentially renders MonadPlus unnecessary, as it's used as if it's Maybe. If we don't want interface change. maybe we should document it that using a MonadPlus without Maybe is deprecated.

[RyanGlScott]

If we change solutionFrom into that, won't the lookupLit always return Just? We might be as well as making lookupLit return the value directly without Maybe wrapping.

Indeed, lookupLit would always return True. I suppose we could bundle some additional information that indicates whether the Literal was constrained by the solution or not, but I'm not sure if this information would be used anywhere in ersatz.

Either way, we should probably just change the type of lookupLit. It's technically part of the public API, but I doubt it's used that much by code in the wild.

Also, this will essentially renders MonadPlus unnecessary, as it's used as if it's Maybe. If we don't want interface change. maybe we should document it that using a MonadPlus without Maybe is deprecated.

Indeed. But as noted above, I'm not sure if using Maybe makes sense either, as I don't think you can ever get solveWith to return Nothing.

The more I think about it, the interface for solveWith seems imprecise. I think a better type for solveWith would be:

data Result a
  = Unsolved
  | Unsatisfied
  | Satisfied a

type Solver s m = s -> m (Result (IntMap Bool))

solveWith ::
  (Monad m, HasSAT s, Default s, Codec a) =>
  Solver s m -> StateT s m a -> m (Result (Decoded a))

That is, make the Satisfied constructor carry a payload. In the case of Solver, this payload would be the satisfying assignment, and in the case of solveWith, this payload would be the decoded result. This way, there is no confusion about what the relationship between the Result and Maybe values is.

Of course, this would be a pretty substantial change to the ersatz API, and if we chose this plan, we'd want to think about a migration path. In the meantime, perhaps we should simply document the best practices for using solveWith. That is:

1. solveWith's results only make sense when picking Maybe as the particular MonadPlus type.
2. The decoded results are only meaningful when the Result value is Satisfied.

[RyanGlScott]

One thing that I forgot is that user-written Codec instances are free to return mzero (i.e., Nothing), and indeed, this is something that likely happens in the wild. As such, I don't think my idea for completely revamping the type of solveWith in https://github.com/ekmett/ersatz/issues/76#issuecomment-1719212158 is fully baked.

For now, I propose that we:

1. Specialize the type of solveWith to work over Maybe instead of any MonadPlus instance (thereby fixing #61),
2. Changing the type of solutionLit from Literal -> Maybe Bool to Literal -> Bool and making it always return False for unconstrainted literals (thereby fixing this issue, #76), and
3. Documenting that the Maybe (Decoded a) value that solveWith returns is only meaningful if the Result value is Satisfied.

Does that sound reasonable?

[RyanGlScott]

I've submitted #77 with a fix. While implementing this, I discovered that I actually don't need to change the type of solutionLiteral at all, as it's more natural to change the behavior of the Codec Literal instead. I've made sure to carefully document this, of course.

[RyanGlScott]

I've released ersatz-0.5 to Hackage, which includes these changes.