test_sat() - Code Metrics - conda/conda - Measure and Improve Code Quality continuously with Scrutinizer

test_sat() F
last analyzed 2018-07-03 17:04 UTC

↳ Parent: Project

Complexity

Conditions

Size

Total Lines

Duplication

Lines	0
Ratio	0 %

Importance

Changes

Metric	Value
cc	15
dl	0
loc	19
rs	2.9998
c	0
b	0
f	0

How to fix Complexity

from itertools import chain, combinations, permutations, product

import pytest

from conda.common.compat import iteritems, string_types
from conda.common.logic import (Clauses, evaluate_eq, minimal_unsatisfiable_subset)
from tests.helpers import raises


# These routines implement logical tests with short-circuiting
# and propogation of unknown values:
#    - positive integers are variables
#    - negative integers are negations of positive variables
#    - lowercase True and False are fixed values
#    - None reprents an indeterminate value
# If a fixed result is not determinable, the result is None, which
# propagates through the result.
#
# To ensure correctness, the only logic functions we have implemented
# directly are NOT and OR. The rest are implemented in terms of these.
# Peformance is not an issue.


def my_NOT(x):
    if isinstance(x, bool):
        return not x
    if isinstance(x, int):
        return -x
    if isinstance(x, string_types):
        return x[1:] if x[0] == '!' else '!' + x
    return None


def my_ABS(x):
    if isinstance(x, bool):
        return True
    if isinstance(x, int):
        return abs(x)
    if isinstance(x, string_types):
        return x[1:] if x[0] == '!' else x
    return None


def my_OR(*args):
    '''Implements a logical OR according to the logic:
            - positive integers are variables
            - negative integers are negations of positive variables
            - lowercase True and False are fixed values
            - None is an unknown value
       True  OR x -> True
       False OR x -> False
       None  OR x -> None
       x     OR y -> None'''
    if any(v is True for v in args):
        return True
    args = set([v for v in args if v is not False])
    if len(args) == 0:
        return False
    if len(args) == 1:
        return next(v for v in args)
    if len(set([v if v is None else my_ABS(v) for v in args])) < len(args):
        return True
    return None


def my_AND(*args):
    args = list(map(my_NOT,args))
    return my_NOT(my_OR(*args))


def my_XOR(i,j):
    return my_OR(my_AND(i,my_NOT(j)),my_AND(my_NOT(i),j))


def my_ITE(c,t,f):
    return my_OR(my_AND(c,t),my_AND(my_NOT(c),f))


def my_AMONE(*args):
    args = [my_NOT(v) for v in args]
    return my_AND(*[my_OR(v1,v2) for v1,v2 in combinations(args,2)])


def my_XONE(*args):
    return my_AND(my_OR(*args),my_AMONE(*args))


def my_SOL(ij, sol):
    return (v if type(v) is bool else (True if v in sol else False) for v in ij)


def my_EVAL(eq, sol):
    # evaluate_eq doesn't handle True/False entries
    return evaluate_eq(eq, sol) + sum(c for c, a in eq if a is True)

# Testing strategy: mechanically construct a all possible permutations of
# True, False, variables from 1 to m, and their negations, in order to exercise
# all logical branches of the function. Test negative, positive, and full
# polarities for each.


def my_TEST(Mfunc, Cfunc, mmin, mmax, is_iter):
    for m in range(mmin,mmax+1):
        if m == 0:
            ijprod = [()]
        else:
            ijprod = (True,False)+sum(((k,my_NOT(k)) for k in range(1,m+1)),())
            ijprod = product(ijprod, repeat=m)
        for ij in ijprod:
            C = Clauses()
            Cpos = Clauses()
            Cneg = Clauses()
            for k in range(1,m+1):
                nm = 'x%d' % k
                C.new_var(nm)
                Cpos.new_var(nm)
                Cneg.new_var(nm)
            ij2 = tuple(C.from_index(k) if type(k) is int else k for k in ij)
            if is_iter:
                x = Cfunc.__get__(C,Clauses)(ij2)
                Cpos.Require(Cfunc.__get__(Cpos,Clauses), ij)
                Cneg.Prevent(Cfunc.__get__(Cneg,Clauses), ij)
            else:
                x = Cfunc.__get__(C,Clauses)(*ij2)
                Cpos.Require(Cfunc.__get__(Cpos,Clauses), *ij)
                Cneg.Prevent(Cfunc.__get__(Cneg,Clauses), *ij)
            tsol = Mfunc(*ij)
            if type(tsol) is bool:
                assert x is tsol, (ij2, Cfunc.__name__, C.clauses)
                assert Cpos.unsat == (not tsol) and not Cpos.clauses, (ij, 'Require(%s)')
                assert Cneg.unsat == tsol and not Cneg.clauses, (ij, 'Prevent(%s)')
                continue
            for sol in C.itersolve([(x,)]):
                qsol = Mfunc(*my_SOL(ij,sol))
                assert qsol is True, (ij2, sol, Cfunc.__name__, C.clauses)
            for sol in Cpos.itersolve([]):
                qsol = Mfunc(*my_SOL(ij,sol))
                assert qsol is True, (ij, sol,'Require(%s)' % Cfunc.__name__, Cpos.clauses)
            for sol in C.itersolve([(C.Not(x),)]):
                qsol = Mfunc(*my_SOL(ij,sol))
                assert qsol is False, (ij2, sol, Cfunc.__name__, C.clauses)
            for sol in Cneg.itersolve([]):
                qsol = Mfunc(*my_SOL(ij,sol))
                assert qsol is False, (ij, sol,'Prevent(%s)' % Cfunc.__name__, Cneg.clauses)


def test_NOT():
    my_TEST(my_NOT, Clauses.Not, 1, 1, False)


def test_AND():
    my_TEST(my_AND, Clauses.And, 2,2, False)


@pytest.mark.integration  # only because this test is slow
def test_ALL():
    my_TEST(my_AND, Clauses.All, 0, 4, True)


def test_OR():
    my_TEST(my_OR,  Clauses.Or,  2,2, False)


@pytest.mark.integration  # only because this test is slow
def test_ANY():
    my_TEST(my_OR,  Clauses.Any, 0,4, True)


def test_XOR():
    my_TEST(my_XOR, Clauses.Xor, 2,2, False)


def test_ITE():
    my_TEST(my_ITE, Clauses.ITE, 3,3, False)


def test_AMONE():
    my_TEST(my_AMONE, Clauses.AtMostOne_NSQ, 0,3, True)
    my_TEST(my_AMONE, Clauses.AtMostOne_BDD, 0,3, True)
    my_TEST(my_AMONE, Clauses.AtMostOne, 0,3, True)
    C1 = Clauses(10)
    x1 = C1.AtMostOne_BDD((1,2,3,4,5,6,7,8,9,10))
    C2 = Clauses(10)
    x2 = C2.AtMostOne((1,2,3,4,5,6,7,8,9,10))
    assert x1 == x2 and C1.clauses == C2.clauses


@pytest.mark.integration  # only because this test is slow
def test_XONE():
    my_TEST(my_XONE, Clauses.ExactlyOne_NSQ, 0,3, True)
    my_TEST(my_XONE, Clauses.ExactlyOne_BDD, 0,3, True)
    my_TEST(my_XONE, Clauses.ExactlyOne, 0,3, True)


@pytest.mark.integration  # only because this test is slow
def test_LinearBound():
    L = [
        ([], [0, 1], 10),
        ([], [1, 2], 10),
        ({'x1':2, 'x2':2}, [3, 3], 10),
        ({'x1':2, 'x2':2}, [0, 1], 1000),
        ({'x1':1, 'x2':2}, [0, 2], 1000),
        ({'x1':2, '!x2':2}, [0, 2], 1000),
        ([(1, 1), (2, 2), (3, 3)], [3, 3], 1000),
        ([(0, 1), (1, 2), (2, 3), (0, 4), (1, 5), (0, 6), (1, 7)], [0, 2], 1000),
        ([(0, 1), (1, 2), (2, 3), (0, 4), (1, 5), (0, 6), (1, 7),
          (3, False), (2, True)], [2, 4], 1000),
        ([(1, 15), (2, 16), (3, 17), (4, 18), (5, 6), (5, 19), (6, 7),
          (6, 20), (7, 8), (7, 21), (7, 28), (8, 9), (8, 22), (8, 29), (8, 41), (9,
          10), (9, 23), (9, 30), (9, 42), (10, 1), (10, 11), (10, 24), (10, 31),
          (10, 34), (10, 37), (10, 43), (10, 46), (10, 50), (11, 2), (11, 12), (11,
          25), (11, 32), (11, 35), (11, 38), (11, 44), (11, 47), (11, 51), (12, 3),
          (12, 4), (12, 5), (12, 13), (12, 14), (12, 26), (12, 27), (12, 33), (12,
          36), (12, 39), (12, 40), (12, 45), (12, 48), (12, 49), (12, 52), (12, 53),
          (12, 54)], [192, 204], 100),
        ]
    for eq, rhs, max_iter in L:
        if isinstance(eq, dict):
            N = len(eq)
        else:
            N = max([0]+[a for c,a in eq if a is not True and a is not False])
        C = Clauses(N)
        Cpos = Clauses(N)
        Cneg = Clauses(N)
        if isinstance(eq, dict):
            for k in range(1,N+1):
                nm = 'x%d'%k
                C.name_var(k, nm)
                Cpos.name_var(k, nm)
                Cneg.name_var(k, nm)
            eq2 = [(v,C.from_name(c)) for c,v in iteritems(eq)]
        else:
            eq2 = eq
        x = C.LinearBound(eq, rhs[0], rhs[1])
        Cpos.Require(Cpos.LinearBound, eq, rhs[0], rhs[1])
        Cneg.Prevent(Cneg.LinearBound, eq, rhs[0], rhs[1])
        if x is not False:
            for _, sol in zip(range(max_iter), C.itersolve([] if x is True else [(x,)],N)):
                assert rhs[0] <= my_EVAL(eq2,sol) <= rhs[1], C.clauses
        if x is not True:
            for _, sol in zip(range(max_iter), C.itersolve([] if x is True else [(C.Not(x),)],N)):
                assert not(rhs[0] <= my_EVAL(eq2,sol) <= rhs[1]), C.clauses
        for _, sol in zip(range(max_iter), Cpos.itersolve([],N)):
            assert rhs[0] <= my_EVAL(eq2,sol) <= rhs[1], ('Cpos',Cpos.clauses)
        for _, sol in zip(range(max_iter), Cneg.itersolve([],N)):
            assert not(rhs[0] <= my_EVAL(eq2,sol) <= rhs[1]), ('Cneg',Cneg.clauses)


def test_sat():
    C = Clauses()
    C.new_var('x1')
    C.new_var('x2')
    assert C.sat() is not None
    assert C.sat([]) is not None
    assert C.sat([()]) is None
    assert C.sat([(False,)]) is None
    assert C.sat([(True,),()]) is None
    assert C.sat([(True,False,-1)]) is not None
    assert C.sat([(+1,False),(+2,),(True,)], names=True) == {'x1','x2'}
    assert C.sat([(-1,False),(True,),(+2,)], names=True) == {'x2'}
    assert C.sat([(True,),(-1,),(-2,False)], names=True) == set()
    assert C.sat([(+1,),(-1,False)], names=True) is None
    C.unsat = True
    assert C.sat() is None
    assert C.sat([]) is None
    assert C.sat([(True,)]) is None
    assert len(Clauses(10).sat([[1]])) == 10


def test_minimize():
    # minimize    x1 + 2 x2 + 3 x3 + 4 x4 + 5 x5
    # subject to  x1 + x2 + x3 + x4 + x5  == 1
    C = Clauses(15)
    C.Require(C.ExactlyOne, range(1,6))
    sol = C.sat()
    C.unsat = True
    # Unsatisfiable constraints
    assert C.minimize([(k,k) for k in range(1,6)], sol)[1] == 16
    C.unsat = False
    sol, sval = C.minimize([(k,k) for k in range(1,6)], sol)
    assert sval == 1
    C.Require(C.ExactlyOne, range(6,11))
    # Supply an initial vector that is too short, forcing recalculation
    sol, sval = C.minimize([(k,k) for k in range(6,11)], sol)
    assert sval == 6
    C.Require(C.ExactlyOne, range(11,16))
    # Don't supply an initial vector
    sol, sval = C.minimize([(k,k) for k in range(11,16)])
    assert sval == 11


def test_minimal_unsatisfiable_subset():
    def sat(val):
        return Clauses(max(abs(v) for v in chain(*val))).sat(val)
    assert raises(ValueError, lambda: minimal_unsatisfiable_subset([[1]], sat))

    clauses = [[-10], [1], [5], [2, 3], [3, 4], [5, 2], [-7], [2], [3],
        [-2, -3, 5], [7, 8, 9, 10], [-8], [-9]]
    res = minimal_unsatisfiable_subset(clauses, sat)
    assert sorted(res) == [[-10], [-9], [-8], [-7], [7, 8, 9, 10]]
    assert not sat(res)

    clauses = [[1, 3], [2, 3], [-1], [4], [3], [-3]]
    for perm in permutations(clauses):
        res = minimal_unsatisfiable_subset(clauses, sat)
        assert sorted(res) == [[-3], [3]]
        assert not sat(res)

    clauses = [[1], [-1], [2], [-2], [3, 4], [4]]
    for perm in permutations(clauses):
        res = minimal_unsatisfiable_subset(perm, sat)
        assert sorted(res) in [[[-1], [1]], [[-2], [2]]]
        assert not sat(res)


1			from itertools import chain, combinations, permutations, product
2
3			import pytest
4
5			from conda.common.compat import iteritems, string_types
6			from conda.common.logic import (Clauses, evaluate_eq, minimal_unsatisfiable_subset)
7			from tests.helpers import raises
8
9
10			# These routines implement logical tests with short-circuiting
11			# and propogation of unknown values:
12			# - positive integers are variables
13			# - negative integers are negations of positive variables
14			# - lowercase True and False are fixed values
15			# - None reprents an indeterminate value
16			# If a fixed result is not determinable, the result is None, which
17			# propagates through the result.
18			#
19			# To ensure correctness, the only logic functions we have implemented
20			# directly are NOT and OR. The rest are implemented in terms of these.
21			# Peformance is not an issue.
22
23
24			def my_NOT(x):
25			if isinstance(x, bool):
26			return not x
27			if isinstance(x, int):
28			return -x
29			if isinstance(x, string_types):
30			return x[1:] if x[0] == '!' else '!' + x
31			return None
32
33
34			def my_ABS(x):
35			if isinstance(x, bool):
36			return True
37			if isinstance(x, int):
38			return abs(x)
39			if isinstance(x, string_types):
40			return x[1:] if x[0] == '!' else x
41			return None
42
43
44			def my_OR(*args):
45			'''Implements a logical OR according to the logic:
46			- positive integers are variables
47			- negative integers are negations of positive variables
48			- lowercase True and False are fixed values
49			- None is an unknown value
50			True OR x -> True
51			False OR x -> False
52			None OR x -> None
53			x OR y -> None'''
54			if any(v is True for v in args):
55			return True
56			args = set([v for v in args if v is not False])
57			if len(args) == 0:
58			return False
59			if len(args) == 1:
60			return next(v for v in args)
61			if len(set([v if v is None else my_ABS(v) for v in args])) < len(args):
62			return True
63			return None
64
65
66			def my_AND(*args):
67			args = list(map(my_NOT,args))
68			return my_NOT(my_OR(*args))
69
70
71			def my_XOR(i,j):
72			return my_OR(my_AND(i,my_NOT(j)),my_AND(my_NOT(i),j))
73
74
75			def my_ITE(c,t,f):
76			return my_OR(my_AND(c,t),my_AND(my_NOT(c),f))
77
78
79			def my_AMONE(*args):
80			args = [my_NOT(v) for v in args]
81			return my_AND(*[my_OR(v1,v2) for v1,v2 in combinations(args,2)])
82
83
84			def my_XONE(*args):
85			return my_AND(my_OR(args),my_AMONE(args))
86
87
88			def my_SOL(ij, sol):
89			return (v if type(v) is bool else (True if v in sol else False) for v in ij)
90
91
92			def my_EVAL(eq, sol):
93			# evaluate_eq doesn't handle True/False entries
94			return evaluate_eq(eq, sol) + sum(c for c, a in eq if a is True)
95
96			# Testing strategy: mechanically construct a all possible permutations of
97			# True, False, variables from 1 to m, and their negations, in order to exercise
98			# all logical branches of the function. Test negative, positive, and full
99			# polarities for each.
100
101
102			def my_TEST(Mfunc, Cfunc, mmin, mmax, is_iter):
103			for m in range(mmin,mmax+1):
104			if m == 0:
105			ijprod = [()]
106			else:
107			ijprod = (True,False)+sum(((k,my_NOT(k)) for k in range(1,m+1)),())
108			ijprod = product(ijprod, repeat=m)
109			for ij in ijprod:
110			C = Clauses()
111			Cpos = Clauses()
112			Cneg = Clauses()
113			for k in range(1,m+1):
114			nm = 'x%d' % k
115			C.new_var(nm)
116			Cpos.new_var(nm)
117			Cneg.new_var(nm)
118			ij2 = tuple(C.from_index(k) if type(k) is int else k for k in ij)
119			if is_iter:
120			x = Cfunc.__get__(C,Clauses)(ij2)
121			Cpos.Require(Cfunc.__get__(Cpos,Clauses), ij)
122			Cneg.Prevent(Cfunc.__get__(Cneg,Clauses), ij)
123			else:
124			x = Cfunc.__get__(C,Clauses)(*ij2)
125			Cpos.Require(Cfunc.__get__(Cpos,Clauses), *ij)
126			Cneg.Prevent(Cfunc.__get__(Cneg,Clauses), *ij)
127			tsol = Mfunc(*ij)
128			if type(tsol) is bool:
129			assert x is tsol, (ij2, Cfunc.__name__, C.clauses)
130			assert Cpos.unsat == (not tsol) and not Cpos.clauses, (ij, 'Require(%s)')
131			assert Cneg.unsat == tsol and not Cneg.clauses, (ij, 'Prevent(%s)')
132			continue
133			for sol in C.itersolve([(x,)]):
134			qsol = Mfunc(*my_SOL(ij,sol))
135			assert qsol is True, (ij2, sol, Cfunc.__name__, C.clauses)
136			for sol in Cpos.itersolve([]):
137			qsol = Mfunc(*my_SOL(ij,sol))
138			assert qsol is True, (ij, sol,'Require(%s)' % Cfunc.__name__, Cpos.clauses)
139			for sol in C.itersolve([(C.Not(x),)]):
140			qsol = Mfunc(*my_SOL(ij,sol))
141			assert qsol is False, (ij2, sol, Cfunc.__name__, C.clauses)
142			for sol in Cneg.itersolve([]):
143			qsol = Mfunc(*my_SOL(ij,sol))
144			assert qsol is False, (ij, sol,'Prevent(%s)' % Cfunc.__name__, Cneg.clauses)
145
146
147			def test_NOT():
148			my_TEST(my_NOT, Clauses.Not, 1, 1, False)
149
150
151			def test_AND():
152			my_TEST(my_AND, Clauses.And, 2,2, False)
153
154
155			@pytest.mark.integration # only because this test is slow
156			def test_ALL():
157			my_TEST(my_AND, Clauses.All, 0, 4, True)
158
159
160			def test_OR():
161			my_TEST(my_OR, Clauses.Or, 2,2, False)
162
163
164			@pytest.mark.integration # only because this test is slow
165			def test_ANY():
166			my_TEST(my_OR, Clauses.Any, 0,4, True)
167
168
169			def test_XOR():
170			my_TEST(my_XOR, Clauses.Xor, 2,2, False)
171
172
173			def test_ITE():
174			my_TEST(my_ITE, Clauses.ITE, 3,3, False)
175
176
177			def test_AMONE():
178			my_TEST(my_AMONE, Clauses.AtMostOne_NSQ, 0,3, True)
179			my_TEST(my_AMONE, Clauses.AtMostOne_BDD, 0,3, True)
180			my_TEST(my_AMONE, Clauses.AtMostOne, 0,3, True)
181			C1 = Clauses(10)
182			x1 = C1.AtMostOne_BDD((1,2,3,4,5,6,7,8,9,10))
183			C2 = Clauses(10)
184			x2 = C2.AtMostOne((1,2,3,4,5,6,7,8,9,10))
185			assert x1 == x2 and C1.clauses == C2.clauses
186
187
188			@pytest.mark.integration # only because this test is slow
189			def test_XONE():
190			my_TEST(my_XONE, Clauses.ExactlyOne_NSQ, 0,3, True)
191			my_TEST(my_XONE, Clauses.ExactlyOne_BDD, 0,3, True)
192			my_TEST(my_XONE, Clauses.ExactlyOne, 0,3, True)
193
194
195			@pytest.mark.integration # only because this test is slow
196			def test_LinearBound():
197			L = [
198			([], [0, 1], 10),
199			([], [1, 2], 10),
200			({'x1':2, 'x2':2}, [3, 3], 10),
201			({'x1':2, 'x2':2}, [0, 1], 1000),
202			({'x1':1, 'x2':2}, [0, 2], 1000),
203			({'x1':2, '!x2':2}, [0, 2], 1000),
204			([(1, 1), (2, 2), (3, 3)], [3, 3], 1000),
205			([(0, 1), (1, 2), (2, 3), (0, 4), (1, 5), (0, 6), (1, 7)], [0, 2], 1000),
206			([(0, 1), (1, 2), (2, 3), (0, 4), (1, 5), (0, 6), (1, 7),
207			(3, False), (2, True)], [2, 4], 1000),
208			([(1, 15), (2, 16), (3, 17), (4, 18), (5, 6), (5, 19), (6, 7),
209			(6, 20), (7, 8), (7, 21), (7, 28), (8, 9), (8, 22), (8, 29), (8, 41), (9,
210			10), (9, 23), (9, 30), (9, 42), (10, 1), (10, 11), (10, 24), (10, 31),
211			(10, 34), (10, 37), (10, 43), (10, 46), (10, 50), (11, 2), (11, 12), (11,
212			25), (11, 32), (11, 35), (11, 38), (11, 44), (11, 47), (11, 51), (12, 3),
213			(12, 4), (12, 5), (12, 13), (12, 14), (12, 26), (12, 27), (12, 33), (12,
214			36), (12, 39), (12, 40), (12, 45), (12, 48), (12, 49), (12, 52), (12, 53),
215			(12, 54)], [192, 204], 100),
216			]
217			for eq, rhs, max_iter in L:
218			if isinstance(eq, dict):
219			N = len(eq)
220			else:
221			N = max([0]+[a for c,a in eq if a is not True and a is not False])
222			C = Clauses(N)
223			Cpos = Clauses(N)
224			Cneg = Clauses(N)
225			if isinstance(eq, dict):
226			for k in range(1,N+1):
227			nm = 'x%d'%k
228			C.name_var(k, nm)
229			Cpos.name_var(k, nm)
230			Cneg.name_var(k, nm)
231			eq2 = [(v,C.from_name(c)) for c,v in iteritems(eq)]
232			else:
233			eq2 = eq
234			x = C.LinearBound(eq, rhs[0], rhs[1])
235			Cpos.Require(Cpos.LinearBound, eq, rhs[0], rhs[1])
236			Cneg.Prevent(Cneg.LinearBound, eq, rhs[0], rhs[1])
237			if x is not False:
238			for _, sol in zip(range(max_iter), C.itersolve([] if x is True else [(x,)],N)):
239			assert rhs[0] <= my_EVAL(eq2,sol) <= rhs[1], C.clauses
240			if x is not True:
241			for _, sol in zip(range(max_iter), C.itersolve([] if x is True else [(C.Not(x),)],N)):
242			assert not(rhs[0] <= my_EVAL(eq2,sol) <= rhs[1]), C.clauses
243			for _, sol in zip(range(max_iter), Cpos.itersolve([],N)):
244			assert rhs[0] <= my_EVAL(eq2,sol) <= rhs[1], ('Cpos',Cpos.clauses)
245			for _, sol in zip(range(max_iter), Cneg.itersolve([],N)):
246			assert not(rhs[0] <= my_EVAL(eq2,sol) <= rhs[1]), ('Cneg',Cneg.clauses)
247
248
249			def test_sat():
250			C = Clauses()
251			C.new_var('x1')
252			C.new_var('x2')
253			assert C.sat() is not None
254			assert C.sat([]) is not None
255			assert C.sat([()]) is None
256			assert C.sat([(False,)]) is None
257			assert C.sat([(True,),()]) is None
258			assert C.sat([(True,False,-1)]) is not None
259			assert C.sat([(+1,False),(+2,),(True,)], names=True) == {'x1','x2'}
260			assert C.sat([(-1,False),(True,),(+2,)], names=True) == {'x2'}
261			assert C.sat([(True,),(-1,),(-2,False)], names=True) == set()
262			assert C.sat([(+1,),(-1,False)], names=True) is None
263			C.unsat = True
264			assert C.sat() is None
265			assert C.sat([]) is None
266			assert C.sat([(True,)]) is None
267			assert len(Clauses(10).sat([[1]])) == 10
268
269
270			def test_minimize():
271			# minimize x1 + 2 x2 + 3 x3 + 4 x4 + 5 x5
272			# subject to x1 + x2 + x3 + x4 + x5 == 1
273			C = Clauses(15)
274			C.Require(C.ExactlyOne, range(1,6))
275			sol = C.sat()
276			C.unsat = True
277			# Unsatisfiable constraints
278			assert C.minimize([(k,k) for k in range(1,6)], sol)[1] == 16
279			C.unsat = False
280			sol, sval = C.minimize([(k,k) for k in range(1,6)], sol)
281			assert sval == 1
282			C.Require(C.ExactlyOne, range(6,11))
283			# Supply an initial vector that is too short, forcing recalculation
284			sol, sval = C.minimize([(k,k) for k in range(6,11)], sol)
285			assert sval == 6
286			C.Require(C.ExactlyOne, range(11,16))
287			# Don't supply an initial vector
288			sol, sval = C.minimize([(k,k) for k in range(11,16)])
289			assert sval == 11
290
291
292			def test_minimal_unsatisfiable_subset():
293			def sat(val):
294			return Clauses(max(abs(v) for v in chain(*val))).sat(val)
295			assert raises(ValueError, lambda: minimal_unsatisfiable_subset([[1]], sat))
296
297			clauses = [[-10], [1], [5], [2, 3], [3, 4], [5, 2], [-7], [2], [3],
298			[-2, -3, 5], [7, 8, 9, 10], [-8], [-9]]
299			res = minimal_unsatisfiable_subset(clauses, sat)
300			assert sorted(res) == [[-10], [-9], [-8], [-7], [7, 8, 9, 10]]
301			assert not sat(res)
302
303			clauses = [[1, 3], [2, 3], [-1], [4], [3], [-3]]
304			for perm in permutations(clauses):
305			res = minimal_unsatisfiable_subset(clauses, sat)
306			assert sorted(res) == [[-3], [3]]
307			assert not sat(res)
308
309			clauses = [[1], [-1], [2], [-2], [3, 4], [4]]
310			for perm in permutations(clauses):
311			res = minimal_unsatisfiable_subset(perm, sat)
312			assert sorted(res) in [[[-1], [1]], [[-2], [2]]]
313			assert not sat(res)
314

conda / conda

test_sat() F last analyzed 2018-07-03 17:04 UTC

Complexity

Size

Duplication

Importance

How to fix Complexity

Complexity

Duplication Side-by-Side

Filter issues like

test_sat() F
last analyzed 2018-07-03 17:04 UTC