Is there any tool that implements a non-CNF SAT solver?

Question

I need a SAT solver able to take as input not only CNF files but also normal txt files containing propositional clauses (written with only and or and not).

I couldn't find any. Could you please point out one?

Answer 1

After having searched carefully I have found limboole: http://fmv.jku.at/limboole/.

It's really useful because it accepts any propositional logic formula and it can either compute whether it's valid or satisfiable.

Answer 2

Have a look at bc2cnf, a commandline tool which translates Boolean "circuits" into CNF.

A circuit is a collection of Boolean expressions. The expressions can be used as input variables of other expressions.

Once you have the CNF, you can feed it into a SAT solver like cryptominisat or Z3 to find solutions which satisfy your expression(s).

See related posts: here and here

Another interesting innovation of Simon Felix is SATInterface. It allows to couple C# programs with SAT solvers CaDiCaL or cryptominisat.