Email Gateway (Aug 19 2022 at 16:55): Email Gateway (Aug 19 2022 at 16:55):From: "W. Douglas Maurer" <maurer@gwu.edu>
When I used to use try0 in Isabelle 2013, it tried nine methods. In
Isabelle 2014, it tries 12, and the three additional ones are
"algebra", "meson", and "satx". In the new Isabelle/Isar Reference
Manual for 2014, I have found descriptions of "algebra" and "meson",
but not of "satx". Using Google on satx method Isabelle, I find a
statement from Makarius that "It looks like the proof methods 'sat'
and 'satx' and the command 'refute' have seen a renaissance," but
nothing about what these actually do. Is there a description of
"satx" anywhere that I can download? Thanks!
Email Gateway (Aug 19 2022 at 16:56):From: boehmes@in.tum.de
The “satx” method is based on work by Tjark Weber described here:
http://user.it.uu.se/~tjawe125/publications/weber09efficiently.html
In essence, a SAT solver is invoked on the definitional conjunctive normal form of the goal. By default, the applied SAT solver is an ML implementation of a simplified version of the conflict-driven clause learning approach used by modern SAT solvers. Alternatively, external SAT solvers such as Minisat or zChaff can be invoked for better performance.
Regards,
Sascha
Last updated: Apr 26 2024 at 04:17 UTC