search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

small change in orderHelper for better at-most-one #56

Open jwaldmann opened 3 years ago

jwaldmann commented 3 years ago

We implement atmost 1 bs as (essentially) sumBits bs <=? encode 1 with overflow-checked one-bit numbers. The comparison checks that there is no overflow, and that the contents is <=? 1 - but this is trivially true, since its bit-width is one! Currently, that's not detected, so we produce clauses that turn out to be useless. A small change improves the situtaiton.

We get this formula

runSAT' (do xs <- replicateM 2 exists ; assert $ atmost 1 xs; return xs )
([Var 2,Var 3],SAT 4 ((1) & (-4 | -2) & (-4 | -3) & (2 | 3 | 4) & (-3 | -2)) mempty)
                            ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

where variable 4 and its clauses are redundant

The reason is the implementation of <=? for Bits

instance Orderable Bits where
  Bits xs <=? Bits ys = orderHelper true  xs ys
orderHelper :: Bit -> [Bit] -> [Bit] -> Bit
orderHelper c0 xs ys = foldl aux c0 (zipWithBits (,) xs ys)
    where   aux c (x,y) = c && x === y || x <? y

Function aux is called with c=true and y=true. Simplification gives not x || x, but we want true.

We can get this when we change to

      aux c (x,y) = c && (x <=? y) || (x <? y)

Then indeed 

runSAT' (do xs <- replicateM 2 exists ; assert $ atmost 1 xs; return xs )
([Var 2,Var 3],SAT 3 ((1) & (-3 | -2)) mempty)

NB. this atmost 1 looks reasonable also for larger argument lengths

runSAT' (do xs <- replicateM 4 exists ; assert $ atmost 1 xs; return xs )
([Var 2,Var 3,Var 4,Var 5],SAT 7 ((1) 
& (-3 | -2) & (-5 | -4)   
& (-6 | -2) & (-6 | -3) 
& (-7 | -4) & (-7 | -5)
& (6 | 7)) mempty)

runSAT' (do xs <- replicateM 8 exists ; assert $ atmost 1 xs; return xs )
([Var 2,Var 3,Var 4,Var 5,Var 6,Var 7,Var 8,Var 9],SAT 15 ((1) 
& (-3 | -2) & (-5 | -4) 
& (-10 | -2) & (-10 | -3) & (-11 | -4) & (-11 | -5) & (10 | 11) 
& (-7 | -6) & (-9 | -8) 
& (-12 | -6) & (-12 | -7) & (-13 | -8) & (-13 | -9) & (12 | 13) 
& (-14 | -2) & (-14 | -3) & (-14 | -4) & (-14 | -5) 
& (-15 | -6) & (-15 | -7) & (-15 | -8) & (-15 | -9)
 & (14 | 15)) mempty)

This looks good for propagation: assume, e.g., that 4 = true gets assigned. Then we unit-propagate *

For input width n, total number of clauses is n log n.

We are still missing some sharing here? E.g., -15 occurs in 4 clauses but these two should be enough: (-15 | 12) & (-15 | 13).