From 1f4aaf1f1e7b416a58fa00e30a74058836147207 Mon Sep 17 00:00:00 2001 From: prwang Date: Sun, 16 Jul 2017 16:25:18 +0800 Subject: [PATCH] =?UTF-8?q?fix:=20hole3=E9=80=9A=E8=BF=87=EF=BC=81?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .gitignore | 2 - formula.py | 148 ++++++++++++++++++++++++++++------------------------- in.cnf | 97 +++++++++++++++++++++++++++++++++++ main.py | 13 +++-- 4 files changed, 184 insertions(+), 76 deletions(-) create mode 100644 in.cnf diff --git a/.gitignore b/.gitignore index e1252cd..2a75e23 100644 --- a/.gitignore +++ b/.gitignore @@ -1,6 +1,5 @@ # Byte-compiled / optimized / DLL files __pycache__/ -*.py[cod] *$py.class # C extensions @@ -101,4 +100,3 @@ ENV/ .mypy_cache/ #intellij /.idea/ -in.cnf diff --git a/formula.py b/formula.py index 8f0fa0b..104de8e 100644 --- a/formula.py +++ b/formula.py @@ -1,5 +1,7 @@ from typing import * +from itertools import * from copy import copy +import logging class Clause: @@ -8,9 +10,9 @@ class Clause: defined: Set[int] i_: int - def __init__(self, v: Iterable, i_: int): - self.undef = set(v) - self.defined = set() + def __init__(self, undef: Iterable[int], defined: Iterable[int], i_: int): + self.undef = set(undef) + self.defined = set(defined) self.i_ = i_ def def_(self, other: int) -> int: @@ -37,22 +39,10 @@ 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') + __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]] cnf: Dict[int, Clause] @@ -61,10 +51,10 @@ class Formula: int, # depth Optional[Set[int]]]] # any edge table model: Optional[List[int]] - changes: List[Union[int, Asg_sideaff]] + changes: List[int] frame: List[int] depth: int - clacnt : 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) @@ -80,7 +70,7 @@ def assign(self, _var: int, value: bool, for cl, role in self.get_var(_var).rev.items(): x = cl.def_(_var * (-1 + 2 * role)) if role == value: - self.before_unmount(cl) + self.before_unmount(cl, _var) # privatize these clauses del self.cnf[cl.i_] else: if x == 0: @@ -88,56 +78,71 @@ def assign(self, _var: int, value: bool, self.zero = list(cl.defined) elif x == 1: self.one.add(cl) - self.changes.append(Asg_sideaff(_var, cl, value, role)) + + def after_mounted(self, cl: Clause, father: int) -> None: + for x in chain(cl.undef, cl.defined): + if x == father or -x == father: continue + self.get_var(x).rev[cl] = x > 0 + self.get_var(x).stat[x > 0] += 1 + assert self.get_var(x).stat[x > 0] + + def before_unmount(self, cl: Clause, father: int) -> None: + for x in chain(cl.undef, cl.defined): + if x == father or -x == father: continue + 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 push(self) -> None: self.depth += 1 - print('push called, depth = %d'% self.depth) + logging.debug('push called, depth = %d' % self.depth) self.frame.append(len(self.changes)) + def unassign(self, _var: int) -> None: + value = self.var_value[_var][0] + for cl, role in self.get_var(_var).rev.items(): + if role == value: + self.cnf[cl.i_] = cl + self.after_mounted(cl, _var) + cl.undef_(_var * (-1 + 2 * role)) + del self.var_value[_var] + def pop(self) -> None: last = self.frame.pop() while len(self.changes) > last: - 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] + p = self.changes.pop() # throws IndexError indicating unsat + if type(p) == int: + self.unassign(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] - - def before_unmount(self, cl: Clause) -> None: + logging.debug('pop called, depth = %d' % self.depth) - 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 } + 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: - print('bcp returned false!') + logging.debug('bcp returned false!') return False y = self.one.pop() assert (len(y.undef) == 1) m = next(iter(y.undef)) self.assign(abs(m), m > 0, y.defined) + logging.debug('--must assign %d to var_%d because %s' % ( + m > 0, abs(m), str(y.defined))) return True - def add_clause(self, cl) -> None: - tp = self.cnf[self.clacnt] = Clause(cl, self.clacnt) - self.after_mounted(tp) + def add_clause(self, cl: Iterable[int]) -> None: + ud, dd = (set(), set()) + for x in cl: + if x in self.var_value: + assert self.var_value[x][0] != (x > 0) + dd.add(x) + else: + ud.add(x) + assert (not dd or len(ud) == 1) + tp = self.cnf[self.clacnt] = Clause(ud, dd, self.clacnt) + self.after_mounted(tp, 0) self.clacnt += 1 def __init__(self, n: int, cnf1: List[List[int]]): @@ -160,18 +165,6 @@ def validate(self) -> None: 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(): @@ -181,37 +174,51 @@ def decide(self) -> bool: # True if already satisfied 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 + dc = (p.stat[1], p.n_, True) + break elif not p.stat[1]: - self.assign(p.n_, False, None) - return False + dc = (p.stat[0], p.n_, False) + break 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 + return True # SAT x, y, w = dc self.assign(y, w, None) + logging.debug('--decided to assign %d to var_%d' % (w, y)) return False def step(self) -> bool: # throws IndexError + def inflate_cause(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 inflate_cause(edg) + if self.bcp(): self.push() - if self.decide(): #FIXME 异常 + if self.decide(): 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 } + logging.debug('::zero = ' + str(self.zero)) + newlst: List[Tuple[int, bool]] = list(inflate_cause(self.zero)) + self.zero = {x[0] for x in newlst} + self.pop() # must pop at first, or getting wrong number of undecided vars if any(x[1] for x in newlst): self.add_clause(self.zero) self.zero = None - self.pop() return False def solve(self) -> bool: @@ -221,4 +228,3 @@ def solve(self) -> bool: return True except IndexError: return False - diff --git a/in.cnf b/in.cnf new file mode 100644 index 0000000..b7ec4e4 --- /dev/null +++ b/in.cnf @@ -0,0 +1,97 @@ +c pigeon-3: placing 4 pigeons into 3 holes +c +c File generated by 'pigeonhole', (c) Tjark Weber +c +c The SAT encoding of this problem is very straightforward. For each pigeon i +c and each hole j we have a variable x_{n*(i-1)+j} which means that pigeon i +c is placed in hole j. Then we have n+1 clauses which say that a pigeon has +c to be placed in some hole. Then for each hole we have a set of clauses +c ensuring that only one single pigeon is placed into that hole. +c +c This encoding leads to a total of (n+1) * n propositional variables and +c (n+1) + n * (n * (n+1) / 2) clauses. +c +c The resulting SAT problem is unsatisfiable. +c +c run log +p cnf 12 22 +1 2 3 0 +4 5 6 0 +7 8 9 0 +10 11 12 0 +-1 -4 0 +-1 -7 0 +-1 -10 0 +-4 -7 0 +-4 -10 0 +-7 -10 0 +-2 -5 0 +-2 -8 0 +-2 -11 0 +-5 -8 0 +-5 -11 0 +-8 -11 0 +-3 -6 0 +-3 -9 0 +-3 -12 0 +-6 -9 0 +-6 -12 0 +-9 -12 0 +c push called, depth = 1` +c --decided to assign 0 to var_1 +c push called, depth = 2 +c --decided to assign 0 to var_2 +c --must assign 1 to var_3 because {1, 2, 3} +c --must assign 0 to var_6 because {-6, -3} +c --must assign 0 to var_12 because {-12, -3} +c --must assign 0 to var_9 because {-3, -9} +c push called, depth = 3 +c --decided to assign 0 to var_4 +c --must assign 1 to var_5 because {4, 5, 6} +c --must assign 0 to var_8 because {-8, -5} +c --must assign 0 to var_11 because {-5, -11} +c --must assign 1 to var_7 because {8, 9, 7} +c --must assign 1 to var_10 because {10, 11, 12} +c bcp returned false! +c ::zero = [-7, -10] +c pop called, depth = 2 +c --must assign 1 to var_4 because {9, 12, 4, 6} +c --must assign 0 to var_10 because {-4, -10} +c --must assign 0 to var_7 because {-7, -4} +c --must assign 1 to var_11 because {10, 11, 12} +c --must assign 1 to var_8 because {8, 9, 7} +c bcp returned false! +c ::zero = [-8, -11] +c pop called, depth = 1 +c --must assign 1 to var_4 because {9, 12, 4, 6} 9, 12 get popped, why here +c 当弹出6的时候，我们期望调用{9 12 4 6}的undef，将6变成一个defined的变量， +c 然而，发现6的rev里面并没有这一项 +c after-mounted只考虑undef的部分，因此只修改了4的rev， +c 现在4知道了自己是和新学习的句子相关的， +c 然而var 9， 12， 6并不了解自己和新学习的句子相关。 +c rev的定义是什么：变量知道所有未被满足的从句。 +c 一个已经被决定的变量（将来有可能撤销）是否有权利知道自己有多少未被满足的从句？ +c 有的。特别的，如果从来没有加入从句进去， +c 一个变量是否自古以来就知道自己在多少从句中未被满足？ +c 必须是这样，因为撤销这个赋值的时候，要利用rev去通知所有从句，where自己被丢在垃圾桶里 +c 让他们把自己从垃圾桶里捡出来 +c **以上更改已执行！** +c 又再次出现了dic changed during iter +c 原因大概是对变量赋值->导致从句消失->从句在unmount中改变rev +c 因为这个从句想让别的变量知道，自己已经被满足，不需要再管我了 +c 但是负责这个从句的这个变量显然不能“不再管”这个从句 +c 之前的所谓fix是考虑顺序，使得先做cl.def，因此由于错误的版本里面只考虑undef +c ，就管不到自己了。但事实上是，即使是defined，也得进行考虑。 +c 能否通过增加tabu的关系，禁止这个过程访问到自己？ +c 已解决！ +c --must assign 1 to var_2 because {1, 2} +c --must assign 0 to var_11 because {-11, -2} +c --must assign 0 to var_5 because {-5, -2} +c --must assign 0 to var_10 because {-4, -10} +c --must assign 0 to var_7 because {-7, -4} +c --must assign 0 to var_8 because {-8, -2} +c --must assign 1 to var_9 because {8, 9, 7} +c --must assign 1 to var_12 because {10, 11, 12} +c bcp returned false! +c ::zero = [-12, -9] +c GET CYCLIC !! \ No newline at end of file diff --git a/main.py b/main.py index e0ff5ea..50d3436 100644 --- a/main.py +++ b/main.py @@ -2,6 +2,9 @@ import sys import itertools as It from formula import Formula +import logging +from datetime import datetime +import re def parse() -> Tuple[int, List]: tokens = iter([]) @@ -10,6 +13,7 @@ def parse() -> Tuple[int, List]: line1 = list(filter(None, input().strip().split())) if len(line1) and line1[0] != 'c': tokens = It.chain(tokens, line1) + logging.debug(line1) except EOFError: pass clauses = [] @@ -25,14 +29,17 @@ def parse() -> Tuple[int, List]: cc = [] else: cc.append(num) if len(cc): clauses.append(cc) - assert(len(clauses) == m) #FIXME + assert(len(clauses) == m) return n, clauses except (ValueError, AssertionError) as e: print("invalid cnf format") raise e - def main() -> None: + logging.basicConfig(filename='run%s.log'% + re.sub('\W+','_', str(datetime.now())) + , level=logging.DEBUG) + logging.debug('original file is:') n, M = parse() fm = Formula(n, M) if fm.solve(): @@ -45,6 +52,6 @@ def main() -> None: if __name__ == "__main__": - sys.stdin = open('./testfiles/aim/aim-50-1_6-no-1.cnf', 'r') + sys.stdin = open('in.cnf', 'r', encoding='utf-8') main()