import sys
import copy
import random
from os.path import basename
import unittest
import pycosat
from pycosat import solve, itersolve
# -------------------------- utility functions ---------------------------
def read_cnf(path):
"""
read a DIMACS cnf formatted file from `path`, and return the clauses
and number of variables
"""
clauses = []
for line in open(path):
parts = line.split()
if not parts or parts[0] == 'c':
continue
if parts[0] == 'p':
assert len(parts) == 4
assert parts[1] == 'cnf'
n_vars, n_clauses = [int(n) for n in parts[2:4]]
continue
if parts[0] == '%':
break
assert parts[-1] == '0'
clauses.append([int(lit) for lit in parts[:-1]])
assert len(clauses) == n_clauses
return clauses, n_vars
def evaluate(clauses, sol):
"""
evaluate the clauses with the solution
"""
sol_vars = {} # variable number -> bool
for i in sol:
sol_vars[abs(i)] = bool(i > 0)
return all(any(sol_vars[abs(i)] ^ bool(i < 0) for i in clause)
for clause in clauses)
def py_itersolve(clauses):
while True:
sol = pycosat.solve(clauses)
if isinstance(sol, list):
yield sol
clauses.append([-x for x in sol])
else: # no more solutions -- stop iteration
return
def process_cnf_file(path):
sys.stdout.write('%30s: ' % basename(path))
sys.stdout.flush()
clauses, n_vars = read_cnf(path)
sys.stdout.write('vars: %6d cls: %6d ' % (n_vars, len(clauses)))
sys.stdout.flush()
n_sol = 0
for sol in itersolve(clauses, n_vars):
sys.stdout.write('.')
sys.stdout.flush()
assert evaluate(clauses, sol)
n_sol += 1
sys.stdout.write("%d\n" % n_sol)
sys.stdout.flush()
return n_sol
# -------------------------- test clauses --------------------------------
# p cnf 5 3
# 1 -5 4 0
# -1 5 3 4 0
# -3 -4 0
nvars1, clauses1 = 5, [[1, -5, 4], [-1, 5, 3, 4], [-3, -4]]
# p cnf 2 2
# -1 0
# 1 0
nvars2, clauses2 = 2, [[-1], [1]]
# p cnf 2 3
# -1 2 0
# -1 -2 0
# 1 -2 0
nvars3, clauses3 = 2, [[-1, 2], [-1, -2], [1, -2]]
# -------------------------- actual unit tests ---------------------------
tests = []
class TestSolve(unittest.TestCase):
def test_wrong_args(self):
self.assertRaises(TypeError, solve, [[1, 2], [-3]], 'A')
self.assertRaises(TypeError, solve, 1)
self.assertRaises(TypeError, solve, 1.0)
self.assertRaises(TypeError, solve, object())
self.assertRaises(TypeError, solve, ['a'])
self.assertRaises(TypeError, solve, [[1, 2], [3, None]], 5)
self.assertRaises(ValueError, solve, [[1, 2], [3, 0]])
def test_no_clauses(self):
for n in range(7):
self.assertEqual(solve([], n), [-i for i in range(1, n + 1)])
def test_cnf1(self):
self.assertEqual(solve(clauses1), [1, -2, -3, -4, 5])
if sys.version_info[0] == 2:
cls = [[long(lit) for lit in clause] for clause in clauses1]
self.assertEqual(solve(cls), [1, -2, -3, -4, 5])
def test_iter_clauses(self):
self.assertEqual(solve(iter(clauses1)), [1, -2, -3, -4, 5])
def test_each_clause_iter(self):
self.assertEqual(solve([iter(clause) for clause in clauses1]),
[1, -2, -3, -4, 5])
def test_tuple_caluses(self):
self.assertEqual(solve(tuple(clauses1)), [1, -2, -3, -4, 5])
def test_each_clause_tuples(self):
self.assertEqual(solve([tuple(clause) for clause in clauses1]),
[1, -2, -3, -4, 5])
def test_gen_clauses(self):
def gen_clauses():
for clause in clauses1:
yield clause
self.assertEqual(solve(gen_clauses()), [1, -2, -3, -4, 5])
def test_each_clause_gen(self):
self.assertEqual(solve([(x for x in clause) for clause in clauses1]),
[1, -2, -3, -4, 5])
def test_bad_iter(self):
class Liar:
def __iter__(self): return None
self.assertRaises(TypeError, solve, Liar())
def test_cnf2(self):
self.assertEqual(solve(clauses2), "UNSAT")
def test_cnf3(self):
self.assertEqual(solve(clauses3), [-1, -2])
def test_cnf3_3vars(self):
self.assertEqual(solve(clauses3, vars=3), [-1, -2, -3])
def test_cnf1_prop_limit(self):
for lim in range(1, 20):
self.assertEqual(solve(clauses1, prop_limit=lim),
"UNKNOWN" if lim < 8 else [1, -2, -3, -4, 5])
def test_cnf1_vars(self):
self.assertEqual(solve(clauses1, vars=7),
[1, -2, -3, -4, 5, -6, -7])
tests.append(TestSolve)
# -----
class TestIterSolve(unittest.TestCase):
def test_wrong_args(self):
self.assertRaises(TypeError, itersolve, [[1, 2], [-3]], 'A')
self.assertRaises(TypeError, itersolve, 1)
self.assertRaises(TypeError, itersolve, 1.0)
self.assertRaises(TypeError, itersolve, object())
self.assertRaises(TypeError, itersolve, ['a'])
self.assertRaises(TypeError, itersolve, [[1, 2], [3, None]], 5)
self.assertRaises(ValueError, itersolve, [[1, 2], [3, 0]])
def test_no_clauses(self):
for n in range(7):
self.assertEqual(len(list(itersolve([], vars=n))), 2 ** n)
def test_iter_clauses(self):
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve(iter(clauses1))))
def test_each_clause_iter(self):
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve([iter(clause) for clause in clauses1])))
def test_tuple_caluses(self):
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve(tuple(clauses1))))
def test_each_clause_tuples(self):
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve([tuple(clause) for clause in clauses1])))
def test_gen_clauses(self):
def gen_clauses():
for clause in clauses1:
yield clause
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve(gen_clauses())))
def test_each_clause_gen(self):
self.assertTrue(all(evaluate(clauses1, sol) for sol in
itersolve([(x for x in clause) for clause in
clauses1])))
def test_bad_iter(self):
class Liar:
def __iter__(self): return None
self.assertRaises(TypeError, itersolve, Liar())
def test_cnf1(self):
for sol in itersolve(clauses1, nvars1):
#sys.stderr.write('%r\n' % repr(sol))
self.assertTrue(evaluate(clauses1, sol))
sols = list(itersolve(clauses1, vars=nvars1))
self.assertEqual(len(sols), 18)
# ensure solutions are unique
self.assertEqual(len(set(tuple(sol) for sol in sols)), 18)
def test_shuffle_clauses(self):
ref_sols = set(tuple(sol) for sol in itersolve(clauses1))
for _ in range(10):
cnf = copy.deepcopy(clauses1)
# shuffling the clauses does not change the solutions
random.shuffle(cnf)
self.assertEqual(set(tuple(sol) for sol in itersolve(cnf)),
ref_sols)
def test_many_clauses(self):
ref_sols = set(tuple(sol) for sol in itersolve(clauses1))
# repeating the clauses many times does not change the solutions
cnf = 100 * copy.deepcopy(clauses1)
self.assertEqual(set(tuple(sol) for sol in itersolve(cnf)),
ref_sols)
def test_cnf2(self):
self.assertEqual(list(itersolve(clauses2, nvars2)), [])
def test_cnf3_3vars(self):
self.assertEqual(list(itersolve(clauses3, 3)),
[[-1, -2, -3], [-1, -2, 3]])
def test_cnf1_prop_limit(self):
self.assertEqual(list(itersolve(clauses1, prop_limit=2)), [])
tests.append(TestIterSolve)
# ------------------------------------------------------------------------
def run(verbosity=1, repeat=1):
print("sys.prefix: %s" % sys.prefix)
print("sys.version: %s" % sys.version)
print("pycosat version: %r" % pycosat.__version__)
suite = unittest.TestSuite()
for cls in tests:
for _ in range(repeat):
suite.addTest(unittest.makeSuite(cls))
runner = unittest.TextTestRunner(verbosity=verbosity)
return runner.run(suite)
if __name__ == '__main__':
if len(sys.argv) == 1:
run()
else:
for path in sys.argv[1:]:
process_cnf_file(path)