Exception with (!a && !b) || !b

[liskin]

With funsat 0.6.2 (compiled with ghc 7.0.3 after relaxing the base constraint to <5), I get an exception with this formula:

> solve1 (CNF 6 11 $ Data.Set.fromList  [[-6,-5],[-5,-3,2],[-5,1],[-4,-3],[-2,1],[-2,3],[-2,5],[-1,2,5],[1],[3,4],[5,6]])
*** Exception: getUnit: not unit: []
> solve1 . problemCnf . toCNF . runShared $ foldl1 or [ foldl1 and [ not (input 1), not (input 2) ], not (input 2) ]
*** Exception: getUnit: not unit: []

Otherwise it works quite well — after seeing this error I used the CNF form of the circuit and fed that to picosat and got the same results for hundreds of formulas, and it was actually much slower than funsat, so thanks very much for funsat, just please fix this one little issue. :-))

[dbueno]

On Apr 14, 2011, at 5:43 PM, liskin wrote:

With funsat 0.6.2 (compiled with ghc 7.0.3 after relaxing the base constraint to <5), I get an exception with this formula:

solve1 (CNF 6 1 $ Data.Set.fromList [[-6,-5],[-5,-3,2],[-5,1],[-4,-3],[-2,1],[-2,3],[-2,5],[-1,2,5],[1],[3,4],[5,6]])

Does this same problem fail if you write a dimacs cnf file? It looks like you passed the wrong number of clauses in the CNF data structure.

p cnf 6 11
-6 -5 0
-5 -3 2 0
-5 1 0
-4 -3 0
-2 1 0
-2 3 0
-2 5 0
-1 2 5 0
1 0
3 4 0
5 6 0

(The .cnf works fine for me, but YMMV.)

-Denis

[dbueno]

On Apr 14, 2011, at 5:43 PM, liskin wrote:

solve1 (CNF 6 1 $ Data.Set.fromList [[-6,-5],[-5,-3,2],[-5,1],[-4,-3],[-2,1],[-2,3],[-2,5],[-1,2,5],[1],[3,4],[5,6]])
*** Exception: getUnit: not unit: []
solve1 . problemCnf . toCNF . runShared $ foldl1 or [ foldl1 and [ not (input 1), not (input 2) ], not (input 2) ]
*** Exception: getUnit: not unit: []

So I've tried this now (compiled with 6.10.4) and I get an assertion error, even if I use CNF 6 11. I'll have to look into it. Thanks for reporting it. But for what it's worth, the same code works when I pass the cnf file. So it must be something stupid.

-Denis

[liskin]

On Thu, Apr 14, 2011 at 09:20:25PM -0700, dbueno wrote:

It looks like you passed the wrong number of clauses in the CNF data structure.

That was a typo which I fixed by editing the comment, but it remained wrong in
your e-mail, I guess. Sorry :-)