From 8063853085c1c581ae045b6af6937f019a8bdf39 Mon Sep 17 00:00:00 2001 From: prwang Date: Sat, 15 Jul 2017 13:31:02 +0800 Subject: [PATCH] =?UTF-8?q?fix:=20=E6=A0=B7=E4=BE=8B=E9=80=9A=E8=BF=87?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- formula.py | 152 +++++++++++++++++++++++++++++++++++++++++------------ main.py | 18 ++----- search.py | 63 ---------------------- 3 files changed, 122 insertions(+), 111 deletions(-) delete mode 100644 search.py diff --git a/formula.py b/formula.py index 19d512c..8f0fa0b 100644 --- a/formula.py +++ b/formula.py @@ -24,6 +24,8 @@ def undef_(self, other: int) -> None: class VarInfo: + __slots__ = ('n_', 'stat', 'rev') + undef: Set[int] rev: Dict[Clause, bool] # role(+-) of its occurrences in each clause # number of negatively and/or positively occurrences stat: List[int] @@ -35,108 +37,188 @@ def __init__(self, n: int): self.rev = {} +class Asg_sideaff: + __slots__ = ('var', 'cl', 'value', 'role') + var: int + cl: Clause + value: bool + role: bool + + def __init__(self, _var: int, _cl: Clause, _value: bool, _role: bool): + self.var = _var + self.cl = _cl + self.value = _value + self.role = _role + + class Formula: + __slots__ = ('raw', 'cnf', 'var', 'var_value', 'model', 'changes', 'frame', 'depth', 'one', 'zero', 'clacnt') # the following members are managed by push & pop, used in the recursive process - raw : List[List[int]] + raw: List[List[int]] cnf: Dict[int, Clause] var: List[VarInfo] var_value: Dict[int, Tuple[bool, # value - int, # depth - Optional[Set[int]] ] ] # any edge table + int, # depth + Optional[Set[int]]]] # any edge table model: Optional[List[int]] - changes: List[Tuple[int, bool]] + changes: List[Union[int, Asg_sideaff]] frame: List[int] depth: int + clacnt : int - one: Set[Clause] # guaranteed to be size 0 after bcp exits - zero: Optional[List[int]] #not None during the inflating process(backjumping) + one: Set[Clause] # guaranteed to be size 0 after bcp exits + zero: Optional[List[int]] # not None during the inflating process(backjumping) - def get_var(self, x) -> VarInfo: return self.var[abs(x) - 1] + def get_var(self, x) -> VarInfo: + return self.var[abs(x) - 1] def assign(self, _var: int, value: bool, cause: Optional[Set[int]] = None) -> None: self.var_value[_var] = (value, self.depth, None if cause is None else copy(cause)) - for cl, val in self.get_var(_var).rev.items(): - x = cl.def_(_var * (-1 + 2 * val)) - if val == value: + self.changes.append(_var) + for cl, role in self.get_var(_var).rev.items(): + x = cl.def_(_var * (-1 + 2 * role)) + if role == value: self.before_unmount(cl) del self.cnf[cl.i_] else: if x == 0: - self.one.remove(cl) + self.one.discard(cl) self.zero = list(cl.defined) elif x == 1: self.one.add(cl) - self.changes.append((_var, value)) - - def unassign(self, _var: int, value: bool) -> None: - for cl, val in self.get_var(_var).rev.items(): # FIXME rev是不可靠的，因为会新产生从句，导致rev变大 - #TODO 新开一个list真的记一下这些修改，这是容易办到的事情 - if val == value: - self.cnf[cl.i_] = cl - self.after_mounted(cl) - cl.undef_(_var * (-1 + 2 * val)) - del self.var_value[_var] + self.changes.append(Asg_sideaff(_var, cl, value, role)) def push(self) -> None: self.depth += 1 + print('push called, depth = %d'% self.depth) self.frame.append(len(self.changes)) def pop(self) -> None: - last = self.frame.pop() # throws IndexError indicating unsat + last = self.frame.pop() while len(self.changes) > last: - x, y = self.changes.pop() - self.unassign(x, y) + p = self.changes.pop()# FIXME really ? throws IndexError indicating unsat + if type(p) == Asg_sideaff: + if p.value == p.role: + self.cnf[p.cl.i_] = p.cl + self.after_mounted(p.cl) + p.cl.undef_(p.var * (-1 + 2 * p.role)) + elif type(p) == int: + del self.var_value[p] + else: + assert False self.depth -= 1 + print('pop called, depth = %d'% self.depth) def after_mounted(self, cl: Clause) -> None: for x in cl.undef: self.get_var(x).rev[cl] = x > 0 self.get_var(x).stat[x > 0] += 1 - assert self.get_var(x).stat[x > 0] <= 2 #TODO 这个数据调完删掉 + assert self.get_var(x).stat[x > 0] def before_unmount(self, cl: Clause) -> None: + for x in cl.undef: self.get_var(x).stat[x > 0] -= 1 assert self.get_var(x).stat[x > 0] >= 0 del self.get_var(x).rev[cl] - def bcp(self) -> bool: + self.one = { i for k, i in self.cnf.items() if len(i.undef) == 1 } while (self.zero is not None) or len(self.one): if self.zero is not None: - self.one.clear() + print('bcp returned false!') return False y = self.one.pop() - assert(len(y.undef) == 1) + assert (len(y.undef) == 1) m = next(iter(y.undef)) self.assign(abs(m), m > 0, y.defined) return True def add_clause(self, cl) -> None: - i = len(self.cnf) - tp = self.cnf[i] = Clause(cl, i) + tp = self.cnf[self.clacnt] = Clause(cl, self.clacnt) self.after_mounted(tp) - + self.clacnt += 1 def __init__(self, n: int, cnf1: List[List[int]]): self.var = [VarInfo(1 + i) for i in range(n)] self.raw = cnf1 - self.depth = 0 + self.clacnt = self.depth = 0 self.cnf = {} self.var_value = {} - self.model= None + self.model = None self.changes = [] - self.frame = [] + self.frame = [] self.one = set() self.zero = None for cl in cnf1: self.add_clause(cl) def validate(self) -> None: n = len(self.var) - self.model = { (i + 1) : False for i in range(n)} + self.model = {(i + 1): False for i in range(n)} for x, (y, p1, p2) in self.var_value.items(): self.model[x] = y assert all([any([self.model[abs(j)] == (j > 0) for j in i]) for i in self.raw]) + def inflate_cause(self, cause: Iterable[int]): + for i in cause: # 找到低阶项或者同阶自由变量，特别的是同阶决定变量要yieldfrom 边表 + i1 = abs(i) + val, dep, edg = self.var_value[i1] + if val: i1 = -i1 + # if it's been an positive assignment before, + # now it's to be forced false, and vice versa + if dep < self.depth or edg is None: + yield (i1, edg is None) + else: + yield from self.inflate_cause(edg) + + def decide(self) -> bool: # True if already satisfied + assert not self.one and not self.zero + for q, cl in self.cnf.items(): + if len(cl.undef) == 0: + assert False + dc = (0, 0, False) + for p in self.var: + if p.n_ not in self.var_value and (p.stat[0] + p.stat[1]): + if not p.stat[0]: # pure + self.assign(p.n_, True, None) + return False + elif not p.stat[1]: + self.assign(p.n_, False, None) + return False + elif p.stat[0] > dc[0]: + dc = (p.stat[0], p.n_, False) + elif p.stat[1] > dc[0]: + dc = (p.stat[1], p.n_, True) + if dc[0] == 0: + assert len(self.cnf) == 0; + return True + x, y, w = dc + self.assign(y, w, None) + return False + + def step(self) -> bool: # throws IndexError + if self.bcp(): + self.push() + if self.decide(): #FIXME 异常 + return True + elif self.zero is None: + return False + assert self.zero + self.one.clear() + newlst: List[Tuple[int, bool]] = list(self.inflate_cause(self.zero)) + self.zero = { x[0] for x in newlst } + if any(x[1] for x in newlst): + self.add_clause(self.zero) + self.zero = None + self.pop() + return False + + def solve(self) -> bool: + try: + while not self.step(): pass + self.validate() + return True + except IndexError: + return False diff --git a/main.py b/main.py index 1e08df1..e0ff5ea 100644 --- a/main.py +++ b/main.py @@ -1,8 +1,7 @@ from typing import * import sys import itertools as It -from search import CdclEngine - +from formula import Formula def parse() -> Tuple[int, List]: tokens = iter([]) @@ -21,19 +20,12 @@ def parse() -> Tuple[int, List]: cc = [] for num in map(int, tokens[4:]): if num == 0: - cc = list(set(cc)) if len(cc): - cc.sort(key=abs) - N = len(cc) - 1; i = 0 - while i < N: - if abs(cc[i]) == abs(cc[i + 1]): break - i += 1 - if i == N: - clauses.append(cc) + clauses.append(cc) cc = [] else: cc.append(num) if len(cc): clauses.append(cc) - assert(len(clauses) == m) + assert(len(clauses) == m) #FIXME return n, clauses except (ValueError, AssertionError) as e: print("invalid cnf format") @@ -42,7 +34,7 @@ def parse() -> Tuple[int, List]: def main() -> None: n, M = parse() - fm = CdclEngine(n, M) + fm = Formula(n, M) if fm.solve(): print('sat') for i in range(1, n + 1): @@ -53,6 +45,6 @@ def main() -> None: if __name__ == "__main__": - sys.stdin = open('in.cnf', 'r') + sys.stdin = open('./testfiles/aim/aim-50-1_6-no-1.cnf', 'r') main() diff --git a/search.py b/search.py deleted file mode 100644 index 05e5eec..0000000 --- a/search.py +++ /dev/null @@ -1,63 +0,0 @@ -from typing import * -from formula import Formula - - -class CdclEngine(Formula): - def __init__(self, n: int, cnf1: List[List[int]]): - super().__init__(n, cnf1) - - def inflate_cause(self, cause: Iterable[int]): - for i in cause: # 找到低阶项或者同阶自由变量，特别的是同阶决定变量要yieldfrom 边表 - i1 = abs(i) - val, dep, edg = self.var_value[i1] - if val: i1 = -i1 - # if it's been an positive assignment before, - # now it's to be forced false, and vice versa - if dep < self.depth or edg is None: - yield (i1, edg is None) - else: yield from self.inflate_cause(edg) - def decide(self) -> bool: #True if already satisfied - dc = (0, 0, False) - for p in self.var: - if p.n_ not in self.var_value and (p.stat[0] + p.stat[1]): - if not p.stat[0]: # pure - self.assign(p.n_, True, None) - return False - elif not p.stat[1]: - self.assign(p.n_, False, None) - return False - elif p.stat[0] > dc[0]: - dc = (p.stat[0], p.n_, False) - elif p.stat[1] > dc[0]: - dc = (p.stat[1], p.n_, True) - if dc[0] == 0: - assert len(self.cnf) == 0; - return True - x, y, w = dc - self.assign(y, w, None) - return False - def step(self) -> bool: #throws IndexError - if self.bcp(): - self.push() - if self.decide(): return True - elif self.zero is None: return False - assert(self.zero) - newlst: List[Tuple[int, bool]] = list(self.inflate_cause(self.zero)) - self.zero = [x[0] for x in newlst] - if any(x[1] for x in newlst): - self.add_clause(self.zero) - self.zero = None - self.pop() - return False - - def solve(self) -> bool: - try: - while not self.step(): pass - self.validate() - return True - except IndexError: - return False - - # 哪一步调push(), 哪一步pop() - # 向下走，push(), 向上走pop()，走向sibling: pop() & push() - #最开始做了0次假设，每push一次代表多做了一次假设