A Python package for working with Conjunctive Normal Form (CNFs) and Boolean Satisfiability
Project description
A Python package for working with Conjunctive Normal Form (CNFs) and Boolean Satisfiability (SAT)
This Python package is brought to you by Vaibhav Karve and Anil N. Hirani, Department of Mathematics, University of Illinois at Urbana-Champaign.
normal-form
recognizes variables, literals, clauses, and CNFs. The
package implements an interface to easily construct CNFs and SAT-check
them via third-part libraries MINISAT and PySAT.
This package is written in Python v3.10, and is publicly available under the GNU-GPL-v3.0 license. It is set to be released on the Python Packaging Index as an open-source scientific package written in the literate programming style. We specifically chose to write this package as a literate program, despite the verbosity of this style, with the goal to create reproducible computational research.
Installation and usage
To get started on using this package,
-
Istall Python 3.10 or higher.
-
python3.10 -m pip install normal-form
-
Use it in a python script (or interactive REPL) as –
from normal_form import cnf from normal_form import sat # This is the CNF (a ∨ b ∨ ¬c) ∧ (¬b ∨ c ∨ ¬d) ∧ (¬a ∨ d). x1: cnf.Cnf = cnf.cnf([[1, 2, -3], [-2, 3, -4], [-1, 4]]) sat_x1: bool = sat.cnf_bruteforce_satcheck(x1) print(sat_x1) # prints: True because x1 is satisfiable.
Overview of modules
The package consists of the following modules.
Modules that act on Cnfs | |
cnf.py |
Constructors and functions for sentences in conjunctive normal form |
cnf_simplify.py |
Functions for simplifying Cnfs, for example (a∨b∨c) ∧ (a∨b∨¬ c) ⇝ (a ∨ b) |
prop.py |
Functions for propositional calculus – conjunction, disjunction and negation |
Modules concerning SAT | |
sat.py |
Functions for sat-checking Cnfs |
sxpr.py |
Functions for working with s-expressions |
Test suite | |
tests/* |
Unit- and property-based tests for each module |
Algorithms
Currently, normal-form
implements the following algorithms –
-
For formulae in conjunctive normal forms (CNFs), it implements variables, literals, clauses, Boolean formulae, and truth-assignments. It includes an API for reading, parsing and defining new instances.
-
For satisfiability of CNFs, it contains a bruteforce algorithm, an implementation that uses the open-source sat-solver PySAT, and an implementation using the MiniSAT solver.
Principles
normal-form
has been written in the functional-programming style
with the following principles in mind –
-
Avoid classes as much as possible. Prefer defining functions instead.
-
Write small functions and then compose/map/filter them to create more complex functions.
-
Use lazy evaluation strategy whenever possible (using the itertools library).
-
Add type hints wherever possible (checked using the mypy static type-checker).
-
Add unit-tests for each function (checked using the pytest framework). Further, add property-based testing wherever possible (using the hypothesis framework).
Project details
Download files
Download the file for your platform. If you're not sure which to choose, learn more about installing packages.
Source Distribution
Built Distribution
Hashes for normal_form-0.1.1-py3-none-any.whl
Algorithm | Hash digest | |
---|---|---|
SHA256 | a3c5bf53d1bd661ba3fadd094e5abea257907a900ab415a135380e37d70501af |
|
MD5 | ea54720344bfb2b04f95e90e689e70fd |
|
BLAKE2b-256 | 666cae6b23014c7fb458ef9ad2fc8abfa76b25a2fd90bafb4482f8d844c99d2b |