How to convert boolean expression to cnf file?

Question

I need to use a satellite solver to test the feasibility of boolean expressions.

I have a complex boolean expression like this

Is there any automatic cnf file converter so that I can give it to direct satellite?

I am reading a cnf format file .. but how to express this expression in a .cnf file? I am confused when there is a conjunction inside paranthesis and how to express → and ↔? Please help me

Answer 1

There are several solutions.

Limboole is an open source tool that I believe includes a separate conversion of propositional logic for CNF.

More generally, you can also use a tool that supports the propositional logic initially; some examples include Z3 , CVC3, and Yices .

Answer 2

SBSAT is a state-based SAT solver capable of accepting various input formats. You can make a simple expression and pass it to SBSAT for conversion to CNF. manual , section 4.10, describes how to do this.