boolean-expressionsatboolean-algebrasatisfiabilityconjunctive-normal-form

Generating DIMACS CNF file using bc2cnf is missing AND

I tried using the bc2cnf tool to generate the DIMACS CNF file of a boolean equation.

The input file contains the equation of an AND gate as shown below :

BC1.1
f := A & B;
ASSIGN f;

Command used: ./bc2cnf -v inp.txt opt.txt

Content in the output file:

c The instance was satisfiable
c A <-> T
c B <-> T
c f <-> T
p cnf 1 1
1 0

Here, it can be observed that the correct DIMACS CNF format of the AND gate is not generated.

Please let me know how this problem can be rectified.

Solution

  • Use commandline parameter -nosimplify to suppress bc2cnf optimization.

    Result is

    c f <-> 1
c B <-> 2
c A <-> 3
p cnf 3 4
-1 2 0
-1 3 0
1 -3 -2 0
1 0

    bc2cnf has a number of useful parameters. Try bc2cnf -? to get help.