Python - SAT Solver

Original Sources:

• Youtube by ‘PyCon 2019’

  • Slides of the Video

• Github ‘pysat’ (Python 2, Python 3.6+)

• Github ‘pycosat’ (Python $\le$ 3.6)

• Youtube - A Peek Inside SAT Solvers - Jon Smock

---

Used in this file:

• Python - sys.intern

---

Essential Utilities for Humanization

Youtube by ‘PyCon 2019’ @ 27:07

'Utility functions to humanize interaction with pycosat'
 
__author__ = 'Raymond Hettinger'
 
import pycosat                  # https://pypi.python.org/pypi/pycosat
from itertools import combinations
from functools import lru_cache
from sys import intern
 
def make_translate(cnf):
    """Make translator from symbolic CNF to PycoSat's numbered clauses.
 Return a literal to number dictionary and reverse lookup dict
 
 >>> make_translate([['~a', 'b', '~c'], ['a', '~c']])
 ({'a': 1, 'c': 3, 'b': 2, '~a': -1, '~b': -2, '~c': -3},
 {1: 'a', 2: 'b', 3: 'c', -1: '~a', -3: '~c', -2: '~b'})
 """
    lit2num = {}
    for clause in cnf:
        for literal in clause:
            if literal not in lit2num:
                var = literal[1:] if literal[0] == '~' else literal
                num = len(lit2num) // 2 + 1
                lit2num[intern(var)] = num
                lit2num[intern('~' + var)] = -num
    num2var = {num:lit for lit, num in lit2num.items()}
    return lit2num, num2var
 
def translate(cnf, uniquify=False):
    'Translate a symbolic cnf to a numbered cnf and return a reverse mapping'
    # DIMACS CNF file format:
    # http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html
    if uniquify:
        cnf = list(dict.fromkeys(cnf))
    lit2num, num2var = make_translate(cnf)
    numbered_cnf = [tuple([lit2num[lit] for lit in clause]) for clause in cnf]
    return numbered_cnf, num2var
 
def itersolve(symbolic_cnf, include_neg=False):
    numbered_cnf, num2var = translate(symbolic_cnf)
    for solution in pycosat.itersolve(numbered_cnf):
        yield [num2var[n] for n in solution if include_neg or n > 0]
 
def solve_all(symcnf, include_neg=False):
    return list(itersolve(symcnf, include_neg))
 
def solve_one(symcnf, include_neg=False):
    return next(itersolve(symcnf, include_neg))
 
############### Support for Building CNFs ##########################
 
@lru_cache(maxsize=None)
def neg(element) -> 'element':
    'Negate a single element'
    return intern(element[1:] if element.startswith('~') else '~' + element)
 
def from_dnf(groups) -> 'cnf':
    'Convert from or-of-ands to and-of-ors'
    cnf = {frozenset()}
    for group in groups:
        nl = {frozenset([literal]) : neg(literal) for literal in group}
        # The "clause | literal" prevents dup lits: {x, x, y} -> {x, y}
        # The nl check skips over identities: {x, ~x, y} -> True
        cnf = {clause | literal for literal in nl for clause in cnf
              if nl[literal] not in clause}
        # The sc check removes clauses with superfluous terms:
        #     {{x}, {x, z}, {y, z}} -> {{x}, {y, z}}
        # Should this be left until the end?
        sc = min(cnf, key=len)          # XXX not deterministic
        cnf -= {clause for clause in cnf if clause > sc}
    return list(map(tuple, cnf))
 
class Q:
    'Quantifier for the number of elements that are true'
    def __init__(self, elements):
        self.elements = tuple(elements)
    def __lt__(self, n: int) -> 'cnf':
        return list(combinations(map(neg, self.elements), n))
    def __le__(self, n: int) -> 'cnf':
        return self < n + 1
    def __gt__(self, n: int) -> 'cnf':
        return list(combinations(self.elements, len(self.elements)-n))
    def __ge__(self, n: int) -> 'cnf':
        return self > n - 1
    def __eq__(self, n: int) -> 'cnf':
        return (self <= n) + (self >= n)
    def __ne__(self, n) -> 'cnf':
        raise NotImplementedError
    def __repr__(self) -> str:
        return f'{self.__class__.__name__}(elements={self.elements!r})'
 
def all_of(elements) -> 'cnf':
    'Forces inclusion of matching rows on a truth table'
    return Q(elements) == len(elements)
 
def some_of(elements) -> 'cnf':
    'At least one of the elements must be true'
    return Q(elements) >= 1
 
def one_of(elements) -> 'cnf':
    'Exactly one of the elements is true'
    return Q(elements) == 1
 
def basic_fact(element) -> 'cnf':
    'Assert that this one element always matches'
    return Q([element]) == 1
 
def none_of(elements) -> 'cnf':
    'Forces exclusion of matching rows on a truth table'
    return Q(elements) == 0
 
[Next](https://rhettinger.github.io/rock_paper.html "Pattern Recognition and Reinforcement Learning")  [Previous](https://rhettinger.github.io/puzzle.html "Depth First and Breath First Search")

---

Title

Other Stuff