Add Case Study: Satisfiability

[grantjenks]

"""Satisfiability and Propositional Logic

Consider the following constraints:

– Alice can only meet either on Monday, Wednesday or Thursday
– Bob cannot meet on Wednesday
– Carol cannot meet on Friday
– Dave cannot meet neither on Tuesday nor on Thursday
– Question: When can the meeting take place?

- Encode then into the following Boolean formula:

    (Mon ∨ Wed ∨ Thu) ∧ (¬Wed) ∧ (¬Fri) ∧ (¬Tue ∧ ¬Thu)

The meeting must take place on Monday

"""

import logging
from patternmatching import *

logging.basicConfig(format='%(message)s', level=logging.DEBUG)

options = [
    'monday', 'wednesday', 'thursday', 'X',
    'monday', 'tuesday', 'thursday', 'friday', 'X',
    'monday', 'tuesday', 'wednesday', 'thursday', 'X',
    'monday', 'wednesday', 'friday', 'X',
    True,
]

constraints = (
    padding + anyone * group('alice') + padding + 'X'
    + padding + anyone * group('bob') + padding + 'X'
    + padding + anyone * group('carol') + padding + 'X'
    + padding + anyone * group('dave') + padding + 'X'
    + like(lambda _: bound.alice == bound.bob == bound.carol == bound.dave)
)

assert match(options, constraints)  # <-- FAILS! and I don't know why :(

[grantjenks]

Idea: make a reduced repro for the bug, duhh!

[grantjenks]

This is a fine test case but lousy example. It is little more than combinatorial brute force for something that is easily solved in your head. It’s also embarrassingly slow. This may be possible but it’s not worth advertising.

[grantjenks]

Note that real SAT solvers have optimizers that make them far faster.