This is a program to answer the question of whether a boolean satisfiability problem in conjunctive normal form with 3 variables per clause (3SAT) is true or false in linear time.

solve-3sat.py

#!/usr/bin/python
# ***************************
# * solve-3sat.py
# *  by Graham Neubig
# *  4/1/2013
# ***************************
#
# This is a Python program to provide an answer for satisfiability problems
# in conjunctive normal form with 3 variables per clause (3SAT) in LINEAR time.
#
# Given a particular expression such as the following:
#  (a or b or c) and (a or !b or !c)
#
# The input to the program is one clause per line with the ! indicating false:
# a b c
# a !b !c
#
# Given an input in this format, this program will provide an answer indicating
# whether the satisfiability problem is solvable or not.

# First, read in the input
import sys
clauses = []
# Read in every line of the file
for line in sys.stdin:
    line = line.strip()
    # Split it into three clauses
    (a, b, c) = line.split(' ')
    # Add the clause to the end of the list
    clauses.append( (a, b, c) )

# Provide an answer
print "Maybe!"