Incorrect grounding of formula with two bi-implications.

What steps will reproduce the problem?

1. Using the attached MLN and evidence file, run:

     $ infer -i net.mln -e evidence.db -q R -outputNetwork -r ground.lcnf

What is the expected output? What do you see instead?

The input cnf has a formula of the form:

A <=> (B <=> C).

The grounded formula should give us constraints of the form:

!A v !B v C.
!A v B v !C.
A v !B v !C.
A v B v C.

Instead, it gives us an unsatisfiable formula consisting solely of unit clauses.

What version of the product are you using? On what operating system?

January 2013 release. Linux, Fedora 20, x86_64.

Please provide any additional information below.

Original issue reported on code.google.com by Kopp.Ti...@gmail.com on 10 Feb 2015 at 4:44

Attachments:

evidence.db
net.mln

iraycd / alchemy-2

Incorrect grounding of formula with two bi-implications. #12