0

I am automatically generating clauses like this with a C++ program: 

((((((condition1#0 and not action1#0 and not action2#0 and TRUE) and (action1#1 and not action2#1 and not condition1#1 and TRUE) and TRUE)) or (not action1#0 and not action2#0 and not condition1#0 and action2#1 and not action1#1 and not condition1#1 and TRUE) or FALSE)))

I need then to check their satisfiability with some tool (something like MiniSat), but before inputing them in such a tool I need to convert them in DIMACS CNF, do you know any tool that can do it automatically for me?

Thank you!

Edit:

Also a non-CNF sat solver would work fine!

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
elena
  • 889
  • 2
  • 11
  • 19

1 Answers1

1

In pysmt there is a parser called human readable parser (hrparser) that should be able to parse those expressions. [1] .

Pysmt is integrated with both picosat and the cudd bdd package,so that you can check for satisfiability easily. In general, smt solvers are more flexible in the structure of the input (non cnf) . If you can change the output of the c++ code, it might be easy enough to create an smtlib file and use an smt silver (eg yices, z3, or cvc4).

Note: I am one of the developers of pysmt [1] http://pysmt.readthedocs.io/en/latest/_modules/pysmt/parsing.html#HRParser

Marco
  • 326
  • 1
  • 3
  • thank you! Since I can change the output of my program, do you think I can easily perform the following steps? 1) give the txt file as input to the smtlib 2) check if it is satisfiable 3) find at least one model – elena Jun 01 '18 at 13:52
  • That would be reasonably easy. Notice that most smt solvers have a c api, you could use directly, if you want. Many tools to work with smtlib are linked on the smtlib website http://smtlib.cs.uiowa.edu/utilities.shtml – Marco Jun 02 '18 at 00:23