how to convert boolean expression to cnf file? [closed]

Closed. This question does not meet Stack Overflow guidelines. It is not currently accepting answers.

---

We don’t allow questions seeking recommendations for books, tools, software libraries, and more. You can edit the ques开发者_运维知识库tion so it can be answered with facts and citations.

Closed 3 years ago.

Improve this question

i need to use sat solver for checking satisfiability of boolean expressions..

I have complex boolean expression like this

is there any automatic cnf file converter so that i can give it straight to sat solver?

I read the cnf format file.. but how to express this expression in .cnf file? i get confused when there is a conjunction inside the paranthesis and how to express --> and <-> ? please help me

---

There are a couple of solutions.

Limboole is an open source tool which I believe includes a separate 'propositional logic to CNF' converter.

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

---

SBSAT is a state based SAT solver that is able to accept a variety of input formats. You could take a simple expression and give it to SBSAT to convert to CNF. The manual, section 4.10, describes how to do this.