fix: hole3通过！

.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

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,64 +70,79 @@ 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:
                     self.one.discard(cl)
                     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
-

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 !!