fix: 样例通过一半

.gitignore

@@ -101,3 +101,4 @@ ENV/
 .mypy_cache/
 #intellij
 /.idea/
+in.cnf

formula.py

@@ -1,4 +1,5 @@
 from typing import *
+from copy import copy
 
 
 class Clause:
@@ -23,53 +24,60 @@ def undef_(self, other: int) -> None:
 
 
 class VarInfo:
-    rev: Dict[Clause, bool] = {}  # role(+-) of its occurrences in each clause
+    rev: Dict[Clause, bool]  # role(+-) of its occurrences in each clause
     # number of negatively and/or positively occurrences
-    stat: List[int] = [0, 0]
+    stat: List[int]
     n_: int
 
     def __init__(self, n: int):
         self.n_ = n
+        self.stat = [0, 0]
+        self.rev = {}
 
 
 class Formula:
     # the following members are managed by push & pop, used in the recursive process
-    cnf: Dict[int, Clause] = {}
+    raw : List[List[int]]
+    cnf: Dict[int, Clause]
     var: List[VarInfo]
-    assignment: Dict[int, Tuple[bool, # value
+    var_value: Dict[int, Tuple[bool,  # value
                                 int,  # depth
-                                Set[int]  # any edge table
-    ] ] = {}
+                                Optional[Set[int]] ] ]  # any edge table
+    model: Optional[List[int]]
     changes: List[Tuple[int, bool]]
     frame: List[int]
-    depth = 0
+    depth: int
 
-    one: Set[Clause] # guaranteed to be size 0 after bcp exits FIXME: 递归函数里面使用全局变量小心不同层被改写！
-    zero: Optional[List[int]] = None #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 assign(self, var: int, value: bool,
+    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:
-        for cl, val in self.var[var].rev:
+        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.before_cl_removed(cl)
+                self.before_unmount(cl)
                 del self.cnf[cl.i_]
             else:
-                x = cl.def_( val)
                 if x == 0:
                     self.one.remove(cl)
-                    self.zero = list(cl.undef)
+                    self.zero = list(cl.defined)
                 elif x == 1:
                     self.one.add(cl)
-        self.assignment[var] = (value, self.depth, cause)
-        self.changes.append((var, value))
+        self.changes.append((_var, value))
 
-    def unassign(self, var: int, value: bool) -> None:
-        del self.assignment[var]
-        for cl, val in reversed(self.var[var].rev):
+    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_cl_born(cl)
-            else: cl.undef_(val)
+                self.after_mounted(cl)
+            cl.undef_(_var * (-1 + 2 * val))
+        del self.var_value[_var]
 
     def push(self) -> None:
         self.depth += 1
@@ -82,16 +90,17 @@ def pop(self) -> None:
             self.unassign(x, y)
         self.depth -= 1
 
-    def after_cl_born(self, cl: Clause) -> None:
+    def after_mounted(self, cl: Clause) -> None:
         for x in cl.undef:
-            self.var[abs(x)].rev[cl] = x > 0
-            self.var[abs(x)].stat[x > 0] += 1
+            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 这个数据调完删掉
 
-    def before_cl_removed(self, cl: Clause) -> None:
+    def before_unmount(self, cl: Clause) -> None:
         for x in cl.undef:
-            self.var[abs(x)].stat[x > 0] -= 1
-            assert self.var[abs(x)].stat[x > 0] >= 0
-            del self.var[abs(x)].rev[cl]
+            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:
         while (self.zero is not None) or len(self.one):
@@ -107,9 +116,27 @@ def bcp(self) -> bool:
     def add_clause(self, cl) -> None:
         i = len(self.cnf)
         tp = self.cnf[i] = Clause(cl, i)
-        self.after_cl_born(tp)
+        self.after_mounted(tp)
+
 
     def __init__(self, n: int, cnf1: List[List[int]]):
-        self.var = [VarInfo(i) for i in range(n)]
+        self.var = [VarInfo(1 + i) for i in range(n)]
+        self.raw = cnf1
+        self.depth = 0
+        self.cnf = {}
+        self.var_value = {}
+        self.model= None
+        self.changes = []
+        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)}
+        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])
+
+

main.py

@@ -1,35 +1,39 @@
 from typing import *
+import sys
 import itertools as It
-from formula import Formula
+from search import CdclEngine
+
 
 def parse() -> Tuple[int, List]:
     tokens = iter([])
     try:
         while True:
             line1 = list(filter(None, input().strip().split()))
             if len(line1) and line1[0] != 'c':
-                tokens = It.chain(tokens, input().split())
+                tokens = It.chain(tokens, line1)
     except EOFError:
         pass
     clauses = []
     try:
         tokens = list(tokens)
-        assert(not (len(tokens) < 4 or tokens[0] != 'p' or tokens[1] != 'cnf'))
+        assert len(tokens) >= 4 and tokens[0] == 'p' and tokens[1] == 'cnf'
         n, m = map(int, tokens[2:4])
         cc = []
         for num in map(int, tokens[4:]):
             if num == 0:
                 cc = list(set(cc))
                 if len(cc):
-                    cc.sort(key = abs)
-                    x = len(cc) - 1; i = 0
-                    while i < x:
-                        if abs(cc[x]) == abs(cc[x + 1]): break
-                    if i != x: clauses.append(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)
                     cc = []
             else: cc.append(num)
         if len(cc): clauses.append(cc)
-        assert(len(cc) == m)
+        assert(len(clauses) == m)
         return n, clauses
     except (ValueError, AssertionError) as e:
         print("invalid cnf format")
@@ -38,8 +42,17 @@ def parse() -> Tuple[int, List]:
 
 def main() -> None:
     n, M = parse()
-    fm = Formula(n, M)
+    fm = CdclEngine(n, M)
+    if fm.solve():
+        print('sat')
+        for i in range(1, n + 1):
+            print("var_%d = %d"%(i, fm.model[i]))
+    else:
+        print('unsat')
+
 
 
 if __name__ == "__main__":
+    sys.stdin = open('in.cnf', 'r')
     main()
+

search.py

@@ -1,24 +1,6 @@
 from typing import *
 from formula import Formula
 
-#FIXME 检查所有的abs
-#FIXME 检查所有的not 注意空表是falsey，不像javascript
-
-'''
-        def SAT(Formula):
-            while true:
-                Formula1 = BCP(Formula)
-                Formula2 = SET_PURE_TRUE(Formula1)
-                if Formula2 == Formula1:
-                    break
-            if Formula == true:
-                return true
-            elif Formula == false:
-                return false
-            else:
-                x = CHOOSE_VAR(Formula)
-                return Formula[true/x] or Formula[false/x]
-    '''
 
 class CdclEngine(Formula):
     def __init__(self, n: int, cnf1: List[List[int]]):
@@ -27,18 +9,17 @@ def __init__(self, n: int, cnf1: List[List[int]]):
     def inflate_cause(self, cause: Iterable[int]):
         for i in cause: # 找到低阶项或者同阶自由变量，特别的是同阶决定变量要yieldfrom 边表
             i1 = abs(i)
-            val, dep, edg = self.assignment[i1]
+            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)
-#TODO 这里先乱写一个能用的，调通了再改
     def decide(self) -> bool: #True if already satisfied
         dc = (0, 0, False)
         for p in self.var:
-            if p.n_ not in self.assignment and (p.stat[0] + p.stat[1]):
+            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
@@ -62,21 +43,20 @@ def step(self) -> bool: #throws IndexError
             elif self.zero is None: return False
         assert(self.zero)
         newlst: List[Tuple[int, bool]] = list(self.inflate_cause(self.zero))
-        # 这里会出现x or -x吗 ?
         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
-            #pop两次当且仅当所有的返回项都是低阶项，TODO 反复思考这里的正确性
 
     # 哪一步调push(), 哪一步pop()
     # 向下走，push(), 向上走pop()，走向sibling: pop() & push()