def solve_SAT(expr, num_solutions=None):
    """
    Returns a iterator of {var: truth value} assignments which satisfy the given
    expression.

    Expressions should not include a variable named ``TRUE_``, since those
    are used in the internals of this function as stand-ins for truth literals.
    """
    expr = convert_to_conjunctive_normal_form(expr)
    Assignment = get_assignment_class(expr)

    # Hack to include a True literal (not directly supported by pycosat API).
    # We add a trivial constraint to the list of constraints, forcing this
    # variables to be True in any solutions. Note that this is still conjunctive
    # normal form, since T and F are literals.
    T = Var('TRUE_')
    expr = expr & T

    vars = list(get_free_variables(expr))

    # 1-index, since pycosat expects nonzero integers.
    var2pycosat_index = {v: i + 1 for i, v in enumerate(vars)}

    def get_pycosat_index(literal):
        # pycosat accepts input as a list of CNF subclauses (disjunctions of variables
        # or negated variables).
        if isinstance(literal, Not):
            return -get_pycosat_index(literal.children[0])
        elif isinstance(literal, Var):
            return var2pycosat_index[literal]
        elif isinstance(literal, ExpressionNode):  # pragma: no cover
            raise TypeError('Unhandled literal type %r' % literal)
        else:
            # Here we assume this is some other python object, so we consider it
            # a boolean.
            return var2pycosat_index[T] if literal else -var2pycosat_index[T]

    constraints = [
        map(get_pycosat_index,
            # Child is one of a literal or a disjunction of literals.
            (child.children if isinstance(child, Or) else [child]))
        for child in expr.children
    ]

    solutions = (
        pycosat.itersolve(constraints)
        if num_solutions is None else pycosat.itersolve(constraints, num_solutions))
    for solution in solutions:
        namespace = {}
        for i, var_assignment in enumerate(solution):
            # pycosat returns the solution as a list of positive or negative
            # 1-indexed variable numbers. Positive indices correspond to assignments
            # to True, and negative corresponds to False.
            as_bool = var_assignment > 0
            var = vars[i]
            if var == T:
                assert as_bool, 'Bug: Solution has an invalid solution to the T literal.'
            else:
                namespace[var.name] = as_bool
        yield Assignment(**namespace)

def main():
    # A requires B
    r1 = [-1, 2]

    # A requires C
    r2 = [-1, 3]

    # B conflicts C
    r3 = [-2, -3]

    # A conflicts B
    r4 = [-1, -2]

    # (-A|B) & (-A|C) & (-B|-C)
    cnf1 = [r1, r2, r3]

    # (-A|B) & (-A|-B)
    cnf2 = [r1, r4]

    print("Case 1:")
    for sol in pycosat.itersolve(cnf1):
        interpret(sol)
        print("\t----")

    print("Case 2:")
    for sol in pycosat.itersolve(cnf2):
        interpret(sol)
        print("\t----")

def sat(clauses):
    """
    Calculate a SAT solution for `clauses`.

    Returned is the list of those solutions.  When the clauses are
    unsatisfiable, an empty list is returned.

    """
    try:
        import pycosat
    except ImportError:
        sys.exit('Error: could not import pycosat (required for dependency '
                 'resolving)')

    try:
        pycosat.itersolve({(1,)})
    except TypeError:
        # Old versions of pycosat require lists. This conversion can be very
        # slow, though, so only do it if we need to.
        clauses = list(map(list, clauses))

    solution = pycosat.solve(clauses)
    if solution == "UNSAT" or solution == "UNKNOWN": # wtf https://github.com/ContinuumIO/pycosat/issues/14
        return []
    # XXX: If solution == [] (i.e., clauses == []), the result will have
    # boolean value of False even though the clauses are not unsatisfiable)
    return solution

 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_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 min_sat(clauses, max_n=1000, N=None, alg='iterate'):
    """
    Calculate the SAT solutions for the `clauses` for which the number of true
    literals from 1 to N is minimal.  Returned is the list of those solutions.
    When the clauses are unsatisfiable, an empty list is returned.

    alg can be any algorithm supported by generate_constraints, or 'iterate",
    which iterates all solutions and finds the smallest.

    """
    log.debug("min_sat using alg: %s" % alg)
    try:
        import pycosat
    except ImportError:
        sys.exit('Error: could not import pycosat (required for dependency '
                 'resolving)')

    if not clauses:
        return []
    m = max(map(abs, chain(*clauses)))
    if not N:
        N = m
    if alg == 'iterate':
        min_tl, solutions = sys.maxsize, []
        try:
            pycosat.itersolve({(1,)})
        except TypeError:
            # Old versions of pycosat require lists. This conversion can be
            # very slow, though, so only do it if we need to.
            clauses = list(map(list, clauses))
        for sol in islice(pycosat.itersolve(clauses), max_n):
            tl = sum(lit > 0 for lit in sol[:N]) # number of true literals
            if tl < min_tl:
                min_tl, solutions = tl, [sol]
            elif tl == min_tl:
                solutions.append(sol)
        return solutions
    else:
        solution = sat(clauses)
        if not solution:
            return []
        eq = [(1, i) for i in range(1, N+1)]
        def func(lo, hi):
            return list(generate_constraints(eq, m,
                [lo, hi], alg=alg))
        evaluate_func = partial(evaluate_eq, eq)
        # Since we have a solution, might as well make use of that fact
        max_val = evaluate_func(solution)
        log.debug("Using max_val %s. N=%s" % (max_val, N))
        constraints = bisect_constraints(0, min(max_val, N), clauses, func,
            evaluate_func=evaluate_func, increment=1000)
        return min_sat(list(chain(clauses, constraints)), max_n=max_n, N=N, alg='iterate')

def solve(n):
	y =[]
	#rows
	for i in range (1,(n*n)+1,n):
		y += vertical(range(i,i+n,1),True)

	#columns
	for i in range (1,n+1):
		y+= vertical(range(i,(n*n)-n+1+i,n),True)
		
	#diagonals 
	y+=diagonal(1,n)
	
	#results
	result = []
	for sol in pycosat.itersolve(y):
		result.append(sol)

	#replace numbers with something more meaningful
	result = changeFormat(result,n)
	#return a boolean list indicating which solutions are unique 
	isValid = returnWithoutRotations(result)
	#figure out how many unique solutions there are
	NValidSol = 0
	for i in range(0,len(result)): 
		if isValid[i] :
			NValidSol += 1
	#print out all the unique solutions
	for i in range(0,len(result)):
		if(isValid[i]):
			printSol(result[i])

	print("There are " , NValidSol ,  " unique solutions with rotations and reflections")

 def solve(self):
     """
     Produces an iterator for schedule possibilities that have no conflicts.
     
     Solves the constraints using a SAT solving algorithm and processes the results.
     """
     return ([self.index_mapping[y] for y in x if y > 0] for x in pycosat.itersolve(self.constraints))

def min_sat(clauses, max_n=1000):
    """
    Calculate the SAT solutions for the `clauses` for which the number of
    true literals is minimal.  Returned is the list of those solutions.
    When the clauses are unsatisfiable, an empty list is returned.

    This function could be implemented using a Pseudo-Boolean SAT solver,
    which would avoid looping over the SAT solutions, and would therefore
    be much more efficient.  However, for our purpose the current
    implementation is good enough.
    """
    try:
        import pycosat
    except ImportError:
        sys.exit('Error: could not import pycosat (required for dependency '
                 'resolving)')

    min_tl, solutions = sys.maxsize, []
    for sol in islice(pycosat.itersolve(clauses), max_n):
        tl = sum(lit > 0 for lit in sol) # number of true literals
        if tl < min_tl:
            min_tl, solutions = tl, [sol]
        elif tl == min_tl:
            solutions.append(sol)

    return solutions

def solve():
    clauses = queens_clauses()
    # solve the SAT problem
    for sol in pycosat.itersolve(clauses):
        sol = set(sol)
        for i in range(N):
            print(''.join('Q' if v(i, j) in sol else '.' for j in range(N)))
        print('')

    def solutions(self):
        """
        Yield each solution to the current set of constraints.
        """
        solution_found = False
        for solution in pycosat.itersolve(self.clauses):
            yield self.remap_solution(solution)
            solution_found = True

        if not solution_found:
            # Only present to raise a descriptive exception.
            self.solution

    def minimal_solutions(self):
        # this is a bit of a strawman.  the idea is, we need to enumerate all of the SAT
        # solutions to know which is the smallest!  the containment thing in the old version (below)
        # seems sketchy to me, due to nonmonotonicity.  return to this later.
        solns = []
        for soln in pycosat.itersolve(self.satformula):
            solns.append(frozenset(map(self.vars.lookupNum, filter(lambda x: x > 0, soln))))

        def getKey(item):
            return len(item)

        for soln in sorted(solns, key=getKey):
            yield soln

    def Nminimal_solutions(self):
        solns = []        
        done = []
        for soln in pycosat.itersolve(self.satformula):
            solns.append(frozenset(map(self.vars.lookupNum, filter(lambda x: x > 0, soln))))
        
        def getKey(item):
            return len(item)

        for soln in sorted(solns, key=getKey):
            #if not done.has_key(soln):
            #    yield soln
            if self.contained_in_none(done, soln):
                yield soln
            done.append(soln)

def main(req_use):
    if req_use.strip() == '':
        return [[]]
    # REQUIRED_USE variable value for which the combinations
    # are being generated

    # If flags aren't provided, match words from REQUIRED_USE
    flags = re.findall(r'\w+', req_use)

    # Remove duplicates
    flags = list(set(flags))
    # sort reverse to length (so that they can be replaced in
    # this order by numbers later)
    flags = sorted(flags, key=len)
    flags.reverse()

    i = 1
    dict = {}
    rev_dict = {}
    # Assign a number to each keyword (to send to pycosat as
    # it accepts cnf in form of numbers )
    for k in flags:
        dict[k] = i
        rev_dict[i] = k
        i += 1

    # Generate the needed boolean expression
    cnf_out = solve(req_use)

    # str(object) gives a string in CNF form
    cnf_str = str(cnf_out)

    # Replace all flags with numerical equivalent
    for key in flags:
        cnf_str = cnf_str.replace(key, str(dict[key]))

    # Convert to form needed by pycosat
    cnf_str = cnf_str[1:-1]
    cnf_lst = cnf_str.split(') & (')
    for i in range(len(cnf_lst)):
        cnf_lst[i] = [int(k) for k in cnf_lst[i].split(' | ')]

    # Generate all possible solutions to the equation
    k = (list(pycosat.itersolve(cnf_lst)))
    for soln in k:
        for i in range(0, len(soln)):
            soln[i] = ( "-" if soln[i] < 0 else "" ) + rev_dict[abs(soln[i])]
    return k

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

def sat(clauses, iterator=False):
    """
    Calculate a SAT solution for `clauses`.

    Returned is the list of those solutions.  When the clauses are
    unsatisfiable, an empty list is returned.

    """
    if pycosat_prep:
        clauses = list(map(list,clauses))
    if iterator:
        return pycosat.itersolve(clauses)
    solution = pycosat.solve(clauses)
    if solution == "UNSAT" or solution == "UNKNOWN":
        return None
    return solution

def mate(ind1, ind2, groups, model):
    # g = deepcopy(groups)
    # random.shuffle(g)
    # g = g[:int(len(g)*0.1)]
    # g = [item for i in g for item in i]
    # s1 = list(ind1)
    # s2 = list(ind2)
    # for i in range(len(s1)):
    #     if i in g:
    #         s1[i], s2[i] = s2[i], s1[i]
    # split_point = random.randint(0, len(s1))
    # ind1 = model.Individual(''.join(s1[:split_point]+s2[split_point:]))
    # ind2 = model.Individual(''.join(s2[:split_point]+s1[split_point:]))
    # pdb.set_trace()
    # return ind1, ind2

    diff = [i for i, (x, y) in enumerate(zip(ind1, ind2)) if x != y]
    # lock the irrelevant parts
    cnfs = []
    for i in range(len(ind1)):
        if random.random() < 0.1: continue
        if i not in diff:
            if ind1[i] == '1':
                cnfs += [[i+1]]
            else:
                cnfs += [[-i-1]]
    sat_engine = pycosat.itersolve(model.cnfs + cnfs)
    l = list(islice(sat_engine, 2))
    if len(l) == 0:
        return ind1, ind2
    if len(l) == 1:
        return model.Individual(pycosatSol2binstr(l[0])), ind2
    else:
        ind1 = model.Individual(pycosatSol2binstr(l[0]))
        ind2 = model.Individual(pycosatSol2binstr(l[1]))
        # pdb.set_trace()
        return ind1, ind2

def _generate_schedules_sat_from_sections(sections, busy_times, preferences):
    clauses = []

    # Map from input domain to SAT domain
    # - input domain: course sections
    # - SAT domain: integers
    from_index, from_string, to_index = _build_section_index(sections)

    # Constraint: Must schedule one section for each core component
    core_clauses = collections.defaultdict(list)
    for core_section in sections:
        index = to_index[core_section.get('asString')]
        core_clauses[core_section.get('course') + core_section.get('component')].append(index)
    clauses += [v for k, v in core_clauses.iteritems()]

    # Constraint: Must not schedule conflicting sections together
    # Note: sections in the same component conflict
    # Note: recall (A' + B') == (AB)'
    conflict_clauses = []
    for a, b in _get_conflicts(sections, busy_times):
        if a.get('asString') != b.get('asString'):
            conflict_clauses.append([-1 * to_index[a.get('asString')],
                                     -1 * to_index[b.get('asString')]])
        else:
            conflict_clauses.append([-1 * to_index[a.get('asString')]])
    clauses += conflict_clauses

    # Solve the SAT problem and map back to input domain from SAT domain
    schedules = []
    for solution in pycosat.itersolve(clauses):
        sections = [from_index[i] for i in solution
                    if i > 0]
        schedules.append(Schedule(sections=sections,
                                  preferences=preferences))
        if len(schedules) > 100:
            break
    return schedules

def grouping_dimacs_model_by_sat_solver(dimacs_model):
    # results start from 0
    appendix = list()
    model = dimacs_model
    inds = []
    i = 0
    cnfs = deepcopy(model.cnfs)
    groups = list()
    while True:
        sat_engine = pycosat.itersolve(cnfs)
        i = 0
        for sol in sat_engine:
            i += 1
            if i > 100: break
            inds.append(model.Individual(pycosatSol2binstr(sol)))
        tmp = map(list, zip(*inds))
        tmp = map(lambda x: len(set(x)), tmp)
        group1 = [i for i, j in enumerate(tmp) if j > 1]

        if len(group1) > 0:
            groups.append(group1)
        else:
            break

        addition = []
        for i, j in zip(group1, itemgetter(*group1)(inds[0])):
            if j == '0':
                addition.append([-i-1])
            else:
                addition.append([i+1])

        cnfs = cnfs + addition
        appendix.extend(inds)
        inds = []

    return groups, appendix

 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())))