docs: def adapt_am1(self):
          """
              Detect and adapt intrinsic AtMost1 constraints. Assume
              there is a subset of soft clauses
              :math:`\\mathcal{S}'\subseteq \\mathcal{S}` s.t.
              :math:`\sum_{c\in\\mathcal{S}'}{c\leq 1}`, i.e. at most
              one of the clauses of :math:`\\mathcal{S}'` can be
              satisfied.
  
              Each AtMost1 relationship between the soft clauses can be
              detected in the following way. The method traverses all
              soft clauses of the formula one by one, sets one
              respective selector literal to true and checks whether
              some other soft clauses are forced to be false. This is
              checked by testing if selectors for other soft clauses are
              unit-propagated to be false. Note that this method for
              detection of AtMost1 constraints is *incomplete*, because
              in general unit propagation does not suffice to test
              whether or not :math:`\\mathcal{F}\wedge l_i\\models
              \\neg{l_j}`.
  
              Each intrinsic AtMost1 constraint detected this way is
              handled by calling :func:`process_am1`.
          """
  
          # literal connections
          conns = collections.defaultdict(lambda: set([]))
          confl = []
  
          # prepare connections
          for l1 in self.sels:
              st, props = self.oracle.propagate(assumptions=[l1], phase_saving=2)
              if st:
                  for l2 in props:
                      if -l2 in self.sels_set:
                          conns[l1].add(-l2)
                          conns[-l2].add(l1)
              else:
                  # propagating this literal results in a conflict
                  confl.append(l1)
  
          if confl:  # filtering out unnecessary connections
              ccopy = {}
              confl = set(confl)
  
              for l in conns:
                  if l not in confl:
                      cc = conns[l].difference(confl)
                      if cc:
                          ccopy[l] = cc
  
              conns = ccopy
              confl = list(confl)
  
              # processing unit size cores
              for l in confl:
                  self.core, self.minw = [l], self.wght[l]
                  self.core_sels, self.core_sums = [l], []
                  self.process_core()
  
              if self.verbose > 1:
                  print('c unit cores found: {0}; cost: {1}'.format(len(confl),
                      self.cost))
  
          nof_am1 = 0
          len_am1 = []
          lits = set(conns.keys())
          while lits:
              am1 = [min(lits, key=lambda l: len(conns[l]))]
  
              for l in sorted(conns[am1[0]], key=lambda l: len(conns[l])):
                  if l in lits:
                      for l_added in am1[1:]:
                          if l_added not in conns[l]:
                              break
                      else:
                          am1.append(l)
  
              # updating remaining lits and connections
              lits.difference_update(set(am1))
              for l in conns:
                  conns[l] = conns[l].difference(set(am1))
  
              if len(am1) > 1:
                  # treat the new atmost1 relation
                  self.process_am1(am1)
                  nof_am1 += 1
                  len_am1.append(len(am1))
  
          # updating the set of selectors
          self.sels_set = set(self.sels)
  
          if self.verbose > 1 and nof_am1:
              print('c am1s found: {0}; avgsz: {1:.1f}; cost: {2}'.format(nof_am1,
                  sum(len_am1) / float(nof_am1), self.cost))