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?

score 2 · Accepted Answer · answered Jun 03 '18 at 08:02

2

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.

answered Jun 03 '18 at 08:02

elena

889
2
11
19

Axel Kemper · Answer 2 · 2020-04-27T21:28:09.633

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.

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

2 Answers2