better-sat-solver

Checks whether a given well-formed formula of Propositional Logic in Clausal Normal Form is satisfiable, and if so, produces a satisfying interpretation.

Getting Started

These instructions will get you a copy of the project up and running on your local machine for development and testing purposes. See deployment for notes on how to deploy the project on a live system.

Prerequisites

• Java Development Kit

Compile and Run

• Clone project into your own folder.
• Compile with javac Main.java
• Run using java Main and follow instructions.

Features

• Create maximum invalid clause-set, given a number of literals.
• Create maximum satisfiable clause-set, given a number of literals.
• Create clause-set given a String-representation of a propositional formula in CNF.
  • String-representation has to have every literal in every clause.
    • "A and B" has to be written "(A or -B) and (-A or B) and (A or B)".
• Brute-force a satisfiable interpretation (if one exist) for a given clause-set.

TODO

• Remove requirement that string-representation has to have every literal in every clause.
• Check if a formula is in CNF.
• Convert an arbitrary propositional formula to CNF.
• Add a better algorithm for satisfiability checking (e.g. CDCL).
• Add support for Modal operators.
• Add support for First-Order quantifiers.
• Extend size of maximal clause set.

Built With

• Java SE 8

Contributing

Please read CONTRIBUTING.md for details on our code of conduct, and the process for submitting pull requests to us.

Authors

• Henrik Torland Klev - Initial work - torland-klev

License

This project is licensed under the MIT License - see the LICENSE file for details

Acknowledgments

• M. Giese for teaching me Propositional Logic.