S52SAT 2.0

Binaries: Linux v2 Mac OS X v2 View source

 It is still use as: ./bin/S52SAT $formula [upperbound] [options] [optis] 
 where $formula is an InToHyLo formula

[optis] can now be: 
   -simplification to realize some S5 simplification on the input formula

   -minimal [N] try to find the minimal model (if it exists)
      [N] can be 0 for 1 world to W worlds
                 1 for W worlds to 1 world
                 2 for a dichotomic search.
          by default, the W worlds to 1 world is activated.

[options] can now be: 

   -ToWCnf to display the MaxSAT equivalent of the min modal logic S5 problem
   -bound N to use N as the upper-bound on the SAT translation of the formula

For any additional information about this tool, please feel free to contact montmirail@cril.fr.

    Valentin Montmirail                               
    Université d'Artois                           
    CRIL - CNRS UMR 8188
    Rue Jean Souvraz SP 18 62307 Lens FRANCE