如何使z3返回多个unsat核心，多个令人满意的分配 [英] How to get z3 to return multiple unsat cores, multiple satisfying assignments

查看：170 发布时间：2020/7/6 5:40:28 z3 smt sat

本文介绍了如何使z3返回多个unsat核心，多个令人满意的分配的处理方法，对大家解决问题具有一定的参考价值，需要的朋友们下面随着小编来一起学习吧！

问题描述

我正在研究一种研究工具；我有兴趣检索(针对QF_LRA)

I am working on a component of a research tool; I am interested in retrieving (for QF_LRA)

-多个(最小或其他)UNSAT核心和
-多个SAT作业

-multiple (minimal or otherwise) UNSAT cores and
-multiple SAT assignments

我已经在论坛上检查了有关此主题的较早讨论，例如，如何获取不同的unsat核心在逻辑QF_LRA上使用z3时

I have checked the forum for earlier discussions on this topic e.g., How to get different unsat cores when using z3 on logic QF_LRA

它们指的是z3 Python教程例如 http://rise4fun.com/Z3Py/tutorial/musmss

They refer to the z3 Python tutorial(s) e.g, http://rise4fun.com/Z3Py/tutorial/musmss

，目前似乎已离线.我尝试了github等的其他建议来找到提到的教程，但是没有运气.

which seems to be offline for now. I have tried other suggestions of github etc to find the mentioned tutorial, but have had no luck.

我正在使用z3 Java API；但很乐意转向其他选择.

I am using the z3 Java API; but happy to switch to alternatives.

算法思想

该算法的主要思想是保持两个逻辑上下文并在它们之间交换信息:

Idea of the Algorithm

The main idea of the algorithm is to maintain two logical contexts and exchange information between them:

MapSolver 用于枚举尚未使用的子句集现有无法满足的核心的超集，并且还不是最大满意分配的子集. MapSolver 每个 soft 子句使用一个唯一的原子谓词，因此它枚举原子谓词集.对于每个最小的无法满足的核心，例如，由谓词表示 p ₁，p ₂，p ₅ ， MapSolver 包含条款¬ p ₁∨ &不是; p ₂∨ &不是; p ₅ . 对于每个最大可满足子集，例如，由谓词表示 p ₂，p ₃，p ₅ ， MapSolver 包含一个子句，该子句对应于所有文字的析取不在最大可满足子集中 p ₁∨ p ₄∨ p ₆ .
SubsetSolver 包含一个集合软子句(带有唯一指示符原子的子句被否定). MapSolver 向其提供一组子句(指示原子). 回想一下，这些还不是现有最小值的超集. 不满意的核心，或最大满意分配的子集. 如果断言这些原子使 SubsetSolver 上下文不可行，然后找到对应于这些原子的最小不满足子集. 如果断言原子与 SubsetSolver 一致，则它最大程度地扩展了这组原子，使之令人满意.

The MapSolver is used to enumerate sets of clauses that are not already supersets of an existing unsatisfiable core and not already a subset of a maximal satisfying assignment. The MapSolver uses one unique atomic predicate per soft clause, so it enumerates sets of atomic predicates. For each minimal unsatisfiable core, say, represented by predicates p₁, p₂, p₅, the MapSolver contains the clause ¬ p₁ ∨ ¬ p₂ ∨ ¬ p₅. For each maximal satisfiable subset, say, represented by predicats p₂, p₃, p₅, the MapSolver contains a clause corresponding to the disjunction of all literals not in the maximal satisfiable subset, p₁ ∨ p₄ ∨ p₆.
The SubsetSolver contains a set of soft clauses (clauses with the unique indicator atom occurring negated). The MapSolver feeds it a set of clauses (the indicator atoms). Recall that these are not already a superset of an existing minimal unsatisfiable core, or a subset of a maximal satisfying assignment. If asserting these atoms makes the SubsetSolver context infeasible, then it finds a minimal unsatisfiable subset corresponding to these atoms. If asserting the atoms is consistent with the SubsetSolver, then it extends this set of atoms maximally to a satisfying set.

from Z3 import *

def main():
    x, y = Reals('x y')
    constraints = [x > 2, x < 1, x < 0, Or(x + y > 0, y < 0), Or(y >= 0, x >= 0), Or(y < 0, x < 0), Or(y > 0, x < 0)]
    csolver = SubsetSolver(constraints)
    msolver = MapSolver(n=csolver.n)
    for orig, lits in enumerate_sets(csolver, msolver):
        output = "%s %s" % (orig, lits)
        print(output)



def get_id(x):
    return Z3_get_ast_id(x.ctx.ref(),x.as_ast())

def MkOr(clause):
    if clause == []:
       return False
    else:
       return Or(clause)

SubsetSolver:

class SubsetSolver:
   constraints = []
   n = 0
   s = Solver()
   varcache = {}
   idcache = {}

   def __init__(self, constraints):
       self.constraints = constraints
       self.n = len(constraints)
       for i in range(self.n):
           self.s.add(Implies(self.c_var(i), constraints[i]))

   def c_var(self, i):
       if i not in self.varcache:
          v = Bool(str(self.constraints[abs(i)]))
          self.idcache[get_id(v)] = abs(i)
          if i >= 0:
             self.varcache[i] = v
          else:
             self.varcache[i] = Not(v)
       return self.varcache[i]

   def check_subset(self, seed):
       assumptions = self.to_c_lits(seed)
       return (self.s.check(assumptions) == sat)

   def to_c_lits(self, seed):
       return [self.c_var(i) for i in seed]

   def complement(self, aset):
       return set(range(self.n)).difference(aset)

   def seed_from_core(self):
       core = self.s.unsat_core()
       return [self.idcache[get_id(x)] for x in core]

   def shrink(self, seed):       
       current = set(seed)
       for i in seed:
          if i not in current:
             continue
          current.remove(i)
          if not self.check_subset(current):
             current = set(self.seed_from_core())
          else:
             current.add(i)
       return current

   def grow(self, seed):
       current = seed
       for i in self.complement(current):
           current.append(i)
           if not self.check_subset(current):
              current.pop()
       return current

MapSolver:

class MapSolver:
    def __init__(self, n):
        """Initialization.
           Args:
            n: The number of constraints to map.
        """
       self.solver = Solver()
       self.n = n
       self.all_n = set(range(n))  # used in complement fairly frequently

   def next_seed(self):
       """Get the seed from the current model, if there is one. 
            Returns:
            A seed as an array of 0-based constraint indexes.
       """
       if self.solver.check() == unsat:
            return None
       seed = self.all_n.copy()  # default to all True for "high bias"
       model = self.solver.model()
       for x in model:
           if is_false(model[x]):
              seed.remove(int(x.name()))
       return list(seed)

   def complement(self, aset):
       """Return the complement of a given set w.r.t. the set of mapped constraints."""
       return self.all_n.difference(aset)

   def block_down(self, frompoint):
       """Block down from a given set."""
       comp = self.complement(frompoint)
       self.solver.add( MkOr( [Bool(str(i)) for i in comp] ) )

   def block_up(self, frompoint):
       """Block up from a given set."""
       self.solver.add( MkOr( [Not(Bool(str(i))) for i in frompoint] ) )



  def enumerate_sets(csolver, map):
      """Basic MUS/MCS enumeration, as a simple example."""
      while True:
        seed = map.next_seed()
        if seed is None:
           return
        if csolver.check_subset(seed):
           MSS = csolver.grow(seed)
           yield ("MSS", csolver.to_c_lits(MSS))
           map.block_down(MSS)
        else:
           MUS = csolver.shrink(seed)
           yield ("MUS", csolver.to_c_lits(MUS))
           map.block_up(MUS)

   main()

这篇关于如何使z3返回多个unsat核心，多个令人满意的分配的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！

查看全文

如何使z3返回多个unsat核心，多个令人满意的分配 [英] How to get z3 to return multiple unsat cores, multiple satisfying assignments

问题描述

推荐答案

算法思想

Idea of the Algorithm

相关文章

其他开发最新文章

热门教程

热门工具

登录关闭

如何使z3返回多个unsat核心，多个令人满意的分配 [英] How to get z3 to return multiple unsat cores, multiple satisfying assignments

问题描述

推荐答案

算法思想

Idea of the Algorithm

相关文章

其他开发最新文章

热门教程

热门工具

登录 关闭

登录关闭