f = xy + xy'
  = x(y + y')    [分配律]
  = x · 1        [补集律]
  = x            [同一律]

f = x + x'y
  = (x + x')(x + y)    [分配律]
  = 1 · (x + y)        [补集律]
  = x + y              [同一律]

f = xy + x'z + yz
  = xy + x'z + yz(x + x')    [因为 x+x'=1]
  = xy + x'z + xyz + x'yz
  = xy(1+z) + x'z(1+y)
  = xy + x'z                 [吸收律]

y
     0   1
x 0 [m0][m1]
  1 [m2][m3]

yz
     00  01  11  10
x 0 [m0][m1][m3][m2]
  1 [m4][m5][m7][m6]

wz
     00  01  11  10
xy 00 [  ][  ][  ][  ]
   01 [  ][  ][  ][  ]
   11 [  ][  ][  ][  ]
   10 [  ][  ][  ][  ]

# 检查第k位是否为1
if x & (1 << k):
    ...

# 设置第k位
x |= (1 << k)

# 清除第k位
x &= ~(1 << k)

# 切换第k位
x ^= (1 << k)

# 获取最低位的1
lowest_bit = x & (-x)

# 计算popcount（1的个数）
def popcount(x):
    count = 0
    while x:
        count += x & 1
        x >>= 1
    return count

# 原始
if (x > 0 and y > 0) or (x > 0 and z > 0):
    ...

# 化简后（提取公因子）
if x > 0 and (y > 0 or z > 0):
    ...

# 使用德摩根定律
if not (a and b):
    # 等价于
if not a or not b:
    ...

FLAGS_READ = 1    # 0b001
FLAGS_WRITE = 2   # 0b010
FLAGS_EXEC = 4    # 0b100

permissions = FLAGS_READ | FLAGS_WRITE

if permissions & FLAGS_READ:
    print("可读")

# 清除权限
permissions &= ~FLAGS_WRITE

# 检查是否是2的幂
def is_power_of_two(x):
    return x > 0 and (x & (x - 1)) == 0

# 交换两个数（不使用临时变量）
a ^= b
b ^= a
a ^= b

# 绝对值（对于整数）
def abs_val(x):
    mask = x >> 31  # 获取符号位
    return (x ^ mask) - mask

# 错误
if not a and b:  # 实际是 (not a) and b

# 正确
if not (a and b):

# 安全：如果x为None，不会评估x.value
if x is not None and x.value > 0:
    ...

# 危险：可能抛出异常
if x.value > 0 and x is not None:
    ...

# 位运算
x & y   # 逐位AND

# 逻辑运算
x and y  # 布尔AND

# 负数右移的行为在不同语言中可能不同
# Python: 算术右移（保持符号）
# C/C++: 实现定义

"""
布尔函数表示和化简工具
"""


class BooleanFunction:
    """布尔函数类"""
    
    def __init__(self, num_vars, minterms):
        """
        初始化布尔函数
        
        参数:
            num_vars: 变量数量
            minterms: 最小项列表（输出为1的输入组合的十进制表示）
        """
        self.num_vars = num_vars
        self.minterms = sorted(minterms)
    
    def to_truth_table(self):
        """生成真值表"""
        table = []
        for i in range(2 ** self.num_vars):
            inputs = [(i >> j) & 1 for j in range(self.num_vars - 1, -1, -1)]
            output = 1 if i in self.minterms else 0
            table.append((inputs, output))
        return table
    
    def print_truth_table(self):
        """打印真值表"""
        vars_list = [chr(ord('x') + i) for i in range(self.num_vars)]
        header = " | ".join(vars_list) + " | f"
        print(header)
        print("-" * len(header))
        
        for inputs, output in self.to_truth_table():
            row = " | ".join(str(b) for b in inputs) + f" | {output}"
            print(row)
    
    def to_sop(self):
        """
        转换为最小项之和形式
        
        返回: SOP字符串
        """
        terms = []
        for m in self.minterms:
            bits = [(m >> j) & 1 for j in range(self.num_vars - 1, -1, -1)]
            term = ""
            for i, b in enumerate(bits):
                var = chr(ord('x') + i)
                if b == 1:
                    term += var
                else:
                    term += var + "'"
            terms.append(term)
        
        return " + ".join(terms) if terms else "0"
    
    def to_pos(self):
        """
        转换为最大项之积形式
        
        返回: POS字符串
        """
        maxterms = [i for i in range(2 ** self.num_vars) if i not in self.minterms]
        terms = []
        for m in maxterms:
            bits = [(m >> j) & 1 for j in range(self.num_vars - 1, -1, -1)]
            term_parts = []
            for i, b in enumerate(bits):
                var = chr(ord('x') + i)
                if b == 0:
                    term_parts.append(var)
                else:
                    term_parts.append(var + "'")
            terms.append("(" + " + ".join(term_parts) + ")")
        
        return " · ".join(terms) if terms else "1"


def demonstrate_boolean_function():
    """演示布尔函数"""
    
    print("=== 多数函数（3输入） ===")
    
    # 多数函数：至少2个输入为1时输出1
    # 最小项：3(011), 5(101), 6(110), 7(111)
    maj = BooleanFunction(3, [3, 5, 6, 7])
    
    maj.print_truth_table()
    print(f"\nSOP形式: {maj.to_sop()}")
    print(f"POS形式: {maj.to_pos()}")
    
    print("\n=== XOR函数 ===")
    
    # XOR：输入不同时输出1
    xor = BooleanFunction(2, [1, 2])
    
    xor.print_truth_table()
    print(f"\nSOP形式: {xor.to_sop()}")
    print(f"POS形式: {xor.to_pos()}")


if __name__ == "__main__":
    demonstrate_boolean_function()

"""
卡诺图可视化和化简
"""


def print_kmap_2var(minterms):
    """打印2变量卡诺图"""
    print("2变量卡诺图:")
    print("     y")
    print("    0   1")
    
    for x in [0, 1]:
        row = f"x={x} "
        for y in [0, 1]:
            idx = x * 2 + y
            val = 1 if idx in minterms else 0
            row += f"[{val}] "
        print(row)


def print_kmap_3var(minterms):
    """打印3变量卡诺图"""
    print("3变量卡诺图:")
    print("      yz")
    print("     00  01  11  10")
    
    for x in [0, 1]:
        row = f"x={x} "
        for yz in [0, 1, 3, 2]:  # Gray code order
            idx = x * 4 + yz
            val = 1 if idx in minterms else 0
            row += f"[{val}] "
        print(row)


def print_kmap_4var(minterms):
    """打印4变量卡诺图"""
    print("4变量卡诺图:")
    print("      wz")
    print("     00  01  11  10")
    
    gray_code = [0, 1, 3, 2]
    
    for xy in range(4):
        # Use Gray code for rows too
        if xy == 0: gx, gy = 0, 0
        elif xy == 1: gx, gy = 0, 1
        elif xy == 2: gx, gy = 1, 1
        else: gx, gy = 1, 0
        
        row = f"{gx}{gy} "
        for wz in gray_code:
            idx = gx * 8 + gy * 4 + wz
            val = 1 if idx in minterms else 0
            row += f"[{val}] "
        print(row)


def demonstrate_kmap():
    """演示卡诺图"""
    
    print("=== 2变量卡诺图 ===")
    print_kmap_2var([1, 2, 3])  # x + y
    print()
    
    print("=== 3变量卡诺图 ===")
    print_kmap_3var([1, 2, 4, 7])  # XOR-like
    print()
    
    print("=== 4变量卡诺图 ===")
    print_kmap_4var([0, 1, 2, 4, 5, 6, 8, 9, 10, 12, 13, 14])


if __name__ == "__main__":
    demonstrate_kmap()

"""
逻辑门模拟和电路设计
"""


def AND(*args):
    return all(args)


def OR(*args):
    return any(args)


def NOT(x):
    return not x


def NAND(*args):
    return not AND(*args)


def NOR(*args):
    return not OR(*args)


def XOR(a, b):
    return a != b


def half_adder(a, b):
    """半加器"""
    sum_out = XOR(a, b)
    carry_out = AND(a, b)
    return sum_out, carry_out


def full_adder(a, b, cin):
    """全加器"""
    s1, c1 = half_adder(a, b)
    sum_out, c2 = half_adder(s1, cin)
    carry_out = OR(c1, c2)
    return sum_out, carry_out


def demonstrate_gates():
    """演示逻辑门"""
    
    print("=== 基本逻辑门 ===")
    
    print(f"AND(1, 1) = {int(AND(1, 1))}")
    print(f"OR(0, 1) = {int(OR(0, 1))}")
    print(f"NOT(1) = {int(NOT(1))}")
    print(f"NAND(1, 1) = {int(NAND(1, 1))}")
    print(f"XOR(0, 1) = {int(XOR(0, 1))}")
    
    print("\n=== 半加器 ===")
    for a in [0, 1]:
        for b in [0, 1]:
            s, c = half_adder(a, b)
            print(f"  {a} + {b} = {c}{s}")
    
    print("\n=== 全加器 ===")
    for a in [0, 1]:
        for b in [0, 1]:
            for cin in [0, 1]:
                s, cout = full_adder(a, b, cin)
                print(f"  {a} + {b} + {cin} = {cout}{s}")


if __name__ == "__main__":
    demonstrate_gates()

"""
简单的SAT求解器（DPLL算法）
"""


def dpll(clauses, assignment=None):
    """
    DPLL算法求解SAT
    
    参数:
        clauses: 子句列表，每个子句是文字列表
                 正数表示正文字，负数表示负文字
        assignment: 当前的变量赋值字典
    
    返回:
        满足赋值或None
    """
    if assignment is None:
        assignment = {}
    
    # 简化子句
    simplified = []
    for clause in clauses:
        satisfied = False
        new_clause = []
        for lit in clause:
            var = abs(lit)
            if var in assignment:
                if (lit > 0 and assignment[var]) or (lit < 0 and not assignment[var]):
                    satisfied = True
                    break
            else:
                new_clause.append(lit)
        if not satisfied:
            if not new_clause:
                return None  # 冲突
            simplified.append(new_clause)
    
    if not simplified:
        return assignment  # 所有子句满足
    
    # 单元传播
    unit_clauses = [c for c in simplified if len(c) == 1]
    for uc in unit_clauses:
        lit = uc[0]
        var = abs(lit)
        value = lit > 0
        assignment[var] = value
    
    # 重新简化
    new_clauses = []
    for clause in simplified:
        satisfied = False
        for lit in clause:
            var = abs(lit)
            if var in assignment:
                if (lit > 0 and assignment[var]) or (lit < 0 and not assignment[var]):
                    satisfied = True
                    break
        if not satisfied:
            new_clause = [lit for lit in clause if abs(lit) not in assignment]
            if not new_clause:
                return None
            new_clauses.append(new_clause)
    
    # 选择未赋值变量
    unassigned = set()
    for clause in new_clauses:
        for lit in clause:
            unassigned.add(abs(lit))
    
    if not unassigned:
        return assignment
    
    var = next(iter(unassigned))
    
    # 尝试赋值为True
    new_assignment = assignment.copy()
    new_assignment[var] = True
    result = dpll(new_clauses, new_assignment)
    if result is not None:
        return result
    
    # 尝试赋值为False
    new_assignment = assignment.copy()
    new_assignment[var] = False
    return dpll(new_clauses, new_assignment)


# 测试
clauses = [[1, 2], [-1, 3], [-2, -3]]
result = dpll(clauses)
print(f"\nSAT求解结果: {result}")