Add Case Study: Satisfiability

grantjenks commented 5 years ago

"""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 commented 5 years ago

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

grantjenks commented 5 years ago

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 commented 5 years ago

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

grantjenks / python-pattern-matching

Add Case Study: Satisfiability #7