Skip to content

sat.py

sat.py

Functions for sat-checking Cnfs, Graphs, and MHGraphs.

Satisfiability of Cnfs

A Cnf is satisfiable if there exists a truth assignment for each variable in the Cnf such that on applying the assignment, the Cnf evaluates to True.

This module implements three different sat-solvers

  1. cnf_bruteforce_satcheck: a brute-force solver. This solver is easy to understand and reason about. It does not have other external dependencies. However, it is quite slow.

  2. cnf_pysat_satcheck: using the pysat library's Minisat22 solver. This solver calls Minisat v2.2 via the pysat library. It is the fast solver in this list but has many external dependencies (because pysat has many dependencies).

  3. cnf_minisat_satcheck: using Minisat v2.2 as a subprocess. This calls minisat.c directly as a subprocess. minisat.c is easy to obtain and install. However, creating subprocesses is not a very fast process.

TODO: Add a function for equisatisfiability of Cnfs

cnf_bruteforce_satcheck(cnf_instance)

Use brute force to check satisfiability of Cnf.

.. note:: Brute-forcing is the most sub-optimal strategy possible. Do not use this function on large Cnfs. (Anything more than 6 Variables or 6 Clauses is large.)

Parameters:

Name Type Description Default
cnf_instance

obj:Cnf)

 required
Return

First, tautologically reduce the Cnf. Then. if the Cnf is Satisfiable return True else return False.

Source code in normal_form/sat.py 
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
def cnf_bruteforce_satcheck(cnf_instance: Cnf) -> bool:
    """Use brute force to check satisfiability of Cnf.

    .. note::
       Brute-forcing is the most sub-optimal strategy possible. Do not use this function
       on large Cnfs. (Anything more than 6 Variables or 6 Clauses is large.)

    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       First, tautologically reduce the Cnf. Then. if the Cnf is Satisfiable return
       ``True`` else return ``False``.

    """
    cnf_reduced: Cnf = tauto_reduce(cnf_instance)

    if cnf_reduced == TRUE_CNF:
        return True
    if cnf_reduced == FALSE_CNF:
        return False

    def assigns_cnf_to_true(assignment: Assignment) -> bool:
        return assign(cnf_reduced, assignment) == TRUE_CNF

    # Note: cnf_reduced cannot be TRUE/FALSE, hence all_assignments != ({})
    head: list[Assignment]
    all_assignments: Iterator[Assignment] = generate_assignments(cnf_reduced)
    head, all_assignments = mit.spy(all_assignments)
    assert head != [{}], "Empty assignment generated."

    satisfying_assignments: Iterator[Assignment]
    satisfying_assignments = filter(assigns_cnf_to_true, all_assignments)

    return any(satisfying_assignments)

cnf_minisat_satcheck(cnf_instance)

Use the subprocess library to call minisat.c solver to sat-check a Cnf.

minisat.c should be correctly installed for this to work.

Parameters:

Name Type Description Default
cnf_instance

obj:Cnf)

 required
Return

If the Cnf is Satisfiable return True else return False.

Source code in normal_form/sat.py 
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
def cnf_minisat_satcheck(cnf_instance: Cnf) -> bool:
    """Use the `subprocess` library to call minisat.c solver to sat-check a Cnf.

    minisat.c should be correctly installed for this to work.

    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       If the Cnf is Satisfiable return ``True`` else return ``False``.

    """
    cnf_dimacs: str
    cnf_dimacs = cnf_to_dimacs(cnf_instance)

    output: str = subprocess.run(['minisat', '-rnd-init', '-verb=0'],
                                 input=cnf_dimacs,
                                 text=True,
                                 capture_output=True,
                                 shell=True,
                                 check=False).stdout
    assert output, "Empty output. Check if minisat is installed on your system."
    result: str = output.split()[-1]
    if result == 'SATISFIABLE':
        return True
    if result == 'UNSATISFIABLE':
        return False
    raise RuntimeError('Unexpected output from minisat.', output)   # pragma: no cover

cnf_pysat_satcheck(cnf_instance)

Use the pysat library's Minisat22 solver to sat-check a Cnf.

Parameters:

Name Type Description Default
cnf_instance

obj:Cnf)

 required
Return

If the Cnf is Satisfiable return True else return False.

Source code in normal_form/sat.py 
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
def cnf_pysat_satcheck(cnf_instance: Cnf) -> bool:
    """Use the `pysat` library's Minisat22 solver to sat-check a Cnf.

    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       If the Cnf is Satisfiable return ``True`` else return ``False``.

    """
    if cnf_instance == TRUE_CNF:
        return True
    if cnf_instance == FALSE_CNF:
        return False

    try:
        if (result := Minisat22(int_repr(cnf_instance)).solve()) is None:
            raise RuntimeError("Minisat22 returned None as result.")  # pragma: nocover
        return result
    except (TypeError, RuntimeError) as exc:
        # The Cnf was probably not in reduced form. Reduce and try again
        cnf_reduced: Cnf = tauto_reduce(cnf_instance)
        if cnf_reduced == cnf_instance:
            raise RuntimeError(
                "Irreducible Cnf not getting solved by Minisat22") from exc  # pragma: nocover
        return cnf_pysat_satcheck(cnf_instance=cnf_reduced)

cnf_to_dimacs(cnf_instance)

Convert a Cnf to DIMACS format.

The Cnf is tautologically reduced first so as to not contain TRUE or FALSE lits.

Parameters:

Name Type Description Default
cnf_instance

obj:Cnf)

 required
Return

A string which consists of lines. Each line is a Clause of the Cnf ending with zero. Each lit in the Clause is written with a space delimiter.

After tautological reduction, if the Cnf reduced to TRUE or FALSE then return a string that will be correctly interpreted as such.

Source code in normal_form/sat.py 
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
def cnf_to_dimacs(cnf_instance: Cnf) -> str:
    """Convert a Cnf to DIMACS format.

    The Cnf is tautologically reduced first so as to not contain TRUE or FALSE lits.
    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       A string which consists of lines. Each line is a Clause of the Cnf ending with
       zero. Each lit in the Clause is written with a space delimiter.

       After tautological reduction, if the Cnf reduced to TRUE or FALSE then return a
       string that will be correctly interpreted as such.

    """
    cnf_reduced: Cnf
    cnf_reduced = tauto_reduce(cnf_instance)

    if cnf_reduced == TRUE_CNF:
        return ''  # A Clause that is always satisfied
    if cnf_reduced == FALSE_CNF:
        return '0'  # A Clause that can never be satisfied

    clause_strs: map[map[str]]
    clause_strs = map(lambda clause: map(str, clause), int_repr(cnf_reduced))

    clause_strs_with_tails: map[str]
    clause_strs_with_tails = map(lambda clause_str: ' '.join(clause_str) + ' 0',
                                 clause_strs)

    return '\n'.join(clause_strs_with_tails)

generate_assignments(cnf_instance)

Generate all :math:2^n truth-assignments for a Cnf with :math:n Variables.

A Cnf's truth-assignment will be represented as a dictionary with keys being all the Variables that appear in the Cnf and values being Bools.

Edge cases

  • TRUE/FALSE Cnfs are treated as having :math:0 Variables and therefore their only corresponding truth-assignment is the empty dictionary. In other words, the function returns ({}).

  • Any Cnf that can be tautologically reduced to TRUE/FALSE also returns ({}).

  • This function cannot distinguish between sat/unsat Cnfs.

Parameters:

Name Type Description Default
cnf_instance

obj:Cnf)

 required
Return

First, tautologically reduce the Cnf. Then, return an Iterator of truth-assignment dictionaries with keys being Variables and values being Bools.

Source code in normal_form/sat.py 
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
def generate_assignments(cnf_instance: Cnf) -> Iterator[Assignment]:
    """Generate all :math:`2^n` truth-assignments for a Cnf with :math:`n` Variables.

    A Cnf's `truth-assignment` will be represented as a dictionary with keys being
    all the Variables that appear in the Cnf and values being Bools.

    Edge cases:

       * ``TRUE``/``FALSE`` Cnfs are treated as having :math:`0` Variables and
         therefore their only corresponding truth-assignment is the empty dictionary.
         In other words, the function returns ``({})``.

       * Any Cnf that can be tautologically reduced to TRUE/FALSE also returns ``({})``.

       * This function cannot distinguish between sat/unsat Cnfs.

    Args:
       cnf_instance (:obj:`Cnf`)

    Return:
       First, tautologically reduce the Cnf. Then, return an Iterator of
       truth-assignment dictionaries with keys being Variables and values being
       Bools.

    """
    cnf_reduced: Cnf
    cnf_reduced = tauto_reduce(cnf_instance)

    lit_set: frozenset[Lit]
    lit_set = lits(cnf_reduced) - {lit(Bool.TRUE), lit(Bool.FALSE)}

    lit_value_set: set[int | Bool] = {absolute_value(literal).value for literal in lit_set}
    assert all(isinstance(value, int) for value in lit_value_set)

    variable_set: set[Variable]
    variable_set = {variable(cast(int, value)) for value in lit_value_set}

    assignment_values: Iterator[tuple[Bool, ...]]
    assignment_values = it.product([Bool.TRUE, Bool.FALSE], repeat=len(variable_set))

    for boolean_tuple in assignment_values:
        yield dict(zip(variable_set, boolean_tuple))
Last update: September 11, 2022