TPTP and dimacs are syntax for describing SAT problems
This project converts TPTP syntax to dimacs when it is possible
TPTP BNF: http://www.tptp.org/TPTP/SyntaxBNF.html
TPTP detail description (technical document): http://www.tptp.org/TPTP/TR/TPTPTR.shtml
Dimacs syntax: http://www.domagoj-babic.com/uploads/ResearchProjects/Spear/dimacs-cnf.pdf
Dimacs tutorial: https://fairmut3x.wordpress.com/2011/07/29/cnf-conjunctive-normal-form-dimacs-format-explained/
Python 3.6 or higher required.
pip install -r requirements.txtDo not edit files in antrl_generated they are generated automatically. There is also defined grammar for dimacs but it was not used.
To generate grammar use command:
antlr4 -Dlanguage=Python3 -o antlr_generated tptp.g4 dimacs.g4python main.py -hExample command (converted file will be saved to out.dimacs)
python main.py -f examples/cnf/dimacs-convertable/roles000.p