 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

MQBF instances available here
3CNF_KSP instances available here
LWB K,KT and S4 generator available here
PDDL instances available here generated thanks to http://www.cril.univ-artois.fr/~montmirail/planning-to-s5/

MaxHS-b : http://www.maxhs.org/
MSCG-2015b: https://core.di.fc.ul.pt/~aign/soft/mscg15b-linux-x86-64
MSUNCORE: http://logos.ucd.ie/wiki/doku.php?id=msuncore

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
    http://www.cril.fr/~montmirail

S52SAT 2.0

What's new in 2.0 ?

Benchmarks used

MaxSAT solvers tested to minimize models

Contact