wanted: assertClause :: [Bit] -> m ()

[jwaldmann]

(Note: I will investigate, but I welcome comments. See also #33)

Currently, there seems to be no way to assert a clause. I want this:

assertClause :: (HasSAT s, MonadState s m) => [Bit] -> m ()
assertClause bs = do
  ls <- forM bs runBit
  assertFormula $ formulaFromList [ map literalId ls ]

but this is using runBit which is not exported.

I can assertClause bs = assert $ or bs which is equivalent semantically but produces useless extra clauses: or bs gets Tseitin-transformed in to a fresh literal l. The useless clauses are b ==> l for each b in bs. These will be removed by minisat's simplifier, but we waste time generating them.

Some time ago, I wrote this (see https://hackage.haskell.org/package/ersatz-0.4.7/docs/src/Ersatz.Bit.html#assert)

assert (Not (And bs)) = do
  ls <- Traversable.for bs runBit
  assertFormula $ fromClause $ foldMap (fromLiteral . negateLiteral) ls

but there's a comment in the code that suggests that it's not working. The idea was that or bs will be converted to its AIG form Not(And(map Not bs)) (see #12 )

While we're at it, should also investigate

assertImplies :: (HasSAT s, MonadState s m) => [Bit] -> [Bit] -> m ()
assertImplies xs ys = assertClause (map not xs <> ys)

but perhaps with a better implementation (that avoids <> on lists)

[jwaldmann]

Meanwhile I have seen more instances where assert wastes clauses, and the time to print them.

but there's a comment in the code that suggests that it's not working:

assert (Not (And bs)) = do
ls <- Traversable.for bs runBit
assertFormula $ fromClause $ foldMap (fromLiteral . negateLiteral) ls

I think the underlying reason is

• when we don't use runBit, we lose sharing, and duplicate work
• runBit b produces a literal l that is equivalent to b (Tseitin transform)
• when we use l in the translation of assert $ or [ ... b ... ] (we emit the clause [ ... l .. ]), an implication l => b would be enough.

There is a name for this "half Tseitin" that escapes me at the moment. The idea is: runBit should get context information: the polarity of the usage of the result (positive, negative, both). For "both", use what we have, but for the others, just emit clauses for the one implication that we need.

Then, there should be no need for assertClause.

[jwaldmann]

But ... generateLiteral is used for sharing, so it must give us the information on the polarity that was used when the literal was created. This seems to require the storage of some extra information. Where?

[jwaldmann]

There is a name for this "half Tseitin"

PlaistedGreenbaum’86 https://doi.org/10.1016/S0747-7171(86)80028-1

cited by Armin Biere in http://fmv.jku.at/biere/talks/Biere-SATSMTAR18-talk.pdf (slide 21)