The Davis-Putnam-Logemann-Loveland (DPLL) Algorithm.

dpll.py

#!/usr/bin/env python3
# -- coding: utf-8 -*-

"""Module for the Davis-Putnam-Logemann-Loveland (DPLL) Algorithm."""

from __future__ import print_function
from __future__ import unicode_literals

import re
import sys

# chr was unichr in Python2
if sys.version_info[0] < 3:
	chr = unichr

class ParseError(SyntaxError):
	"""Exception-class for parse-failures."""
	ERROR = '\033[91mError\033[0m: '
	def __init__(self, what):
		"""Initializes the parent exception-class."""
		super(ParseError, self).__init__(self.ERROR + what)

def simplify(expression):
	"""
	Simplifies a logical expression.

	Simplifies:
	!true		->	false
	!false		->	true
	true & F	->	F
	true | F	->	true
	false & F	->	false
	false | F	->	False

	Arguments:
		expression (str): A logical expression.

	Returns:
		The simplified expression.
	"""

	# Keep for reference if we changed something
	original = expression

	# !true -> false
	expression = re.sub(r'!\s*true', r'false', expression)

	# !false -> true
	expression = re.sub(r'!\s*false', r'true', expression)

	# true & F -> F
	expression = re.sub(
		r'\(?(?<!!)true\s*&\s*(\([^)]+\)|[^(&|)\s]+)\)?|'
		r'\(?(\([^)]+\)|[^(&|)\s]+)\s*&\s*(?<!!)true\)?',
		lambda m: m.group(1) or m.group(2),
		expression
	)

	# true | F -> true
	expression = re.sub(
		r'\(?(?<!!)true\s*\|\s*(\([^)]+\)|[^(&|)\s]+)\)?|'
		r'\(?(\([^)]+\)|[^(&|)\s]+)\s*\|\s*(?<!!)true\)?',
		'true',
		expression
	)

	# false & F -> false
	expression = re.sub(
		r'\(?(?<!!)false\s*&\s*(\([^)]+\)|[^(&|)\s]+)\)?|'
		r'\(?(\([^)]+\)|[^(&|)\s]+)\s*&\s*(?<!!)false\)?',
		'false',
		expression
	)

	# false | F -> F
	expression = re.sub(
		r'\(?(?<!!)false\s*\|\s*(\([^)]+\)|[^(&|)\s]+)\)?|'
		r'\(?(\([^)]+\)|[^(&|)\s]+)\s*\|\s*(?<!!)false\)?',
		lambda m: m.group(1) or m.group(2),
		expression
	)

	# (F) -> F
	expression = re.sub(
		r'\((\s*!?\s*\w+\s*|\s*\(.*\))\s*\)',
		r'\1',
		expression
	)

	# If we didn't do anything, we're done
	if expression == original:
		return expression
	return simplify(expression)


def dpll(expression):
	"""
	Applies the Davis-Putnam-Logemann-Loveland (DPLL) Algorithm.

	Arguments:
		expression (str): A logical expression.

	Returns:
		True if the expression is satisfiable, else False.
	"""

	if expression == 'true':
		return True
	if expression == 'false':
		return False

	# Grab next variable, assuming single-character variable
	match = re.search(r'\b\w\b', expression)
	if not match:
		raise ParseError('The expression you entered is not valid.')
	variable = match.group()

	# Replace the variable with 'true' and simplify
	e_1 = simplify(expression.replace(variable, 'true'))

	# Replace the variable with 'false' and simplify
	e_2 = simplify(expression.replace(variable, 'false'))

	# Cheap shortcut before recursing for e_1
	if e_2 == 'true':
		return True

	# See if returns True for e_1 or e_2
	return dpll(e_1) or dpll(e_2)


def parse(expression):
	"""
	Parses an expression.

	Replaces unicode and/or textual logical operators
	with their equivalent for the syntax used here.

	Arguments:
		expression (str): User input for an expression.

	Returns:
		The parsed expression.
	"""

	original = expression

	expression = re.sub(r'AND|{0}'.format(chr(0x2227)), '&', expression)
	expression = re.sub(r'OR|{0}'.format(chr(0x2228)), '|', expression)
	expression = re.sub(r'NOT\s*|{0}\s*'.format(chr(0x172)), '!', expression)

	expression = expression.replace('TRUE', 'true')
	expression = expression.replace('FALSE', 'false')

	return expression

def main():
	"""Main entry point"""
	if len(sys.argv) < 2:
		raise ParseError('Expected logical expression.')

	result = dpll(parse(sys.argv[1]))

	print('Satifiable: {0}.'.format('Yes' if result else 'No'))

if __name__ == '__main__':
	main()