Graph Satisfiability
Home

Pick a countable set and call it our set of variables. A boolean literal is a variable or its negation such that we can assign boolean values to it each variable.

A boolean formula is said to be in Conjunctive Normal Form (CNF) if it is the conjunction of disjunctions of boolean literals. A CNF is satisfiable if there exists a truth assignment that satisfies it. Otherwise it is unsatisfiable.

For every CNF we define a multi-hypergraph by erasing all negations and then treating clauses as hyperedges and conjunctions as the graph-join operation. We denote this projection map by \(\pi\).

Example: \[(a\vee \neg b) \wedge (b \vee \neg c) \wedge (\neg a \vee \neg c)\wedge d \longmapsto (ab),(bc),(ac),(d)\]

Here, \((d)\) should be interpreted as a loop at the vertex \(d\).

Table summarizing the effect of \(\pi\):

A multi-hypergraph \(G\) is satisfiable if the set \(\pi^{-1}(G)\) is nonempty and every element of \(\pi^{-1}(G)\) is satisfiable. Otherwise it is unsatisfiable.

We let GraphSAT itself denote both the decision problem as well as the set of all satisfiable multi-hypergraphs.

Currently, graphsat 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 graph theory, the package includes graphs with self-loops, edge-multiplicities, hyperedges, and multi-hyperedges. It includes an API for reading, parsing and defining new instances.
• For satisfiability of CNFs and graphs, it contains a bruteforce algorithm, an implementation that uses the open-source sat-solver PySAT, and an implementation using the MiniSAT solver.
• Additionally, for graph theory, the library also implements vertex maps, vertex degree, homeomorphisms, homomorphisms, subgraphs, and isomorphisms. This allows us to encode local rewriting rules as well as parallelized grid-based searching for forbidden structures.
• Finally, graphsat has a tree-based recursive reduction algorithm that uses known local-rewrite rules as well as algorithms for checking satisfiability invariance of proposed reduction rules.

graphsat 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 (using the functools library).
• 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).

The package consists of several different modules.

1. Modules that act only on Cnfs –

   cnf.py	Constructors and functions for sentences in conjunctive normal form (Cnf).
   cnf_simplify.py	Functions for simplifying Cnfs, particularly (a∨b∨c) ∧ (a∨b∨¬ c) ⇝ (a ∨ b).
   prop.py	Functions for propositional calculus – conjunction, disjunction and negation.

2. Modules that act only on graphs –

   graph.py	Constructors and functions for simple graphs.
   mhgraph.py	Constructors and functions for Loopless-Multi-Hyper-Graphs
   morphism.py	Constructors and functions for Graph and MHGraph morphisms.

3. Modules concerning SAT and GraphSAT –

   sat.py	Functions for sat-checking Cnfs, Graphs, MHGraphs.
   sxpr.py	Functions for working with s-expressions.
   operations.py	Functions for working with graph-satisfiability and various graph parts.

4. Modules that implement and compute local graph rewriting, rule reduction etc.

   graph_collapse.py	Functions for collapsing a set of Cnfs into compact graphs representation.
   graph_rewrite.py	An implementation of the Local graph rewriting algorithm.

5. Finally, the test suite for each module is located in the test/ folder.