back to root

back to Zipperposition

Msat_tseitin

• Petar Vukmirovic

  2020-04-27 10:23:44 (GMT)

  @Simon Cruanes @Guillaume Bury:

  @Visa created a cool new rule for checking semantic tautology in Zip modulo booleans:
  Clause $\neg \textsf{p} (\textsf{a} \land \textsf{b}) \lor \textsf{p} (\textsf{a}) \lor \textsf{p} (\textsf{b})$ is a tautology

• Petar Vukmirovic

  2020-04-27 10:25:32 (GMT)

  This is easy to see if you write the clause as $\textsf{p} (\textsf{a} \land \textsf{b}) \Rightarrow \textsf{p} (\textsf{a}) \lor \textsf{p} (\textsf{b})$

• Petar Vukmirovic

  2020-04-27 10:28:54 (GMT)

  which can be falsified only if $\neg (\textsf{a} \land \textsf{b} \Leftrightarrow \textsf{a})$ and $\neg (\textsf{a} \land \textsf{b} \Leftrightarrow \textsf{b})$

• Petar Vukmirovic

  2020-04-27 10:29:21 (GMT)

  Which can be checked using SAT solvers

• Petar Vukmirovic

  2020-04-27 10:32:36 (GMT)

  To avoid Tseitin encoding myself I wanted to use the Tseitin encoder of Msat,
  but it is not available in the normal installation of Msat, and MSat_tseitin is not available as well

• Petar Vukmirovic

  2020-04-27 10:34:39 (GMT)

  Is it removed or can just hidden from the public interface?

• Guillaume Bury

  2020-04-27 11:2:43 (GMT)

  It should be available, i'll check.

• Guillaume Bury

  2020-04-27 11:6:24 (GMT)

  @Petar Vukmirovic So, in the last version of msat, the tseitin transformation was made into a separate ocamlfind sub-package, so you need to add msat.tseitin to your list of dependencies, and then the Msat_tseitin module should become available.

• Petar Vukmirovic

  2020-04-27 12:32:23 (GMT)

  Thanks a lot!