组合测试

from pysat.formula import CNF
from pysat.solvers import Solver

VALUE_TO_VAR = {
  ("P1", 0): 1,   # x1
  ("P1", 1): 2,   # x2
  ("P2", 0): 3,   # x3
  ("P2", 1): 4,   # x4
  ("P3", 0): 5,   # x5
  ("P3", 1): 6,   # x6
  ("P3", 2): 7,   # x7
  ("P4", 0): 8,   # x8
  ("P4", 1): 9,   # x9
  ("P4", 2): 10,  # x10
}

# DIMACS 风格的 CNF：正数表示 x，负数表示 not x。
FORMULA = CNF(from_clauses=[
  # at-least & at-most
  [1, 2],[-1, -2],
  [3, 4],
  [-3, -4],
  [5, 6, 7],
  [-5, -6],
  [-5, -7],
  [-6, -7],
  [8, 9, 10],
  [-8, -9],
  [-8, -10],
  [-9, -10],
  # forbidden tuple
  [-4, -6],
])

class ConstraintSolver:
  def __init__(self) -> None:
    self._solver = Solver(bootstrap_with=FORMULA)

  def isSatisfied(self, test_case: dict[str, int]) -> bool:
    assumptions = [VALUE_TO_VAR[item] for item in test_case.items()]
    result = self._solver.solve(assumptions=assumptions)
    print(assumptions, result)
    return result

  def close(self) -> None:
    self._solver.delete()

if __name__ == "__main__":
  solver = ConstraintSolver()

  solver.isSatisfied({"P1": 0, "P2": 0, "P3": 1, "P4": 2})  # True
  solver.isSatisfied({"P2": 1, "P3": 1})  # False
  solver.isSatisfied({"P2": 1})           # True

  solver.close()

from itertools import combinations, count, product
from pathlib import Path
from pysat.formula import CNF
from pysat.solvers import Solver

PARAMETERS = [
  [0, 1],     # P1
  [0, 1],     # P2
  [0, 1, 2],  # P3
  [0, 1, 2],  # P4
]

ARRAY_SIZE = 9
CNF_FILE = Path(__file__).with_name("demo_ca.cnf")

def encode(array_size: int) -> tuple[CNF, dict[tuple[int, int, int], int]]:
  formula = CNF()
  new_var = count(1)

  # x[row, parameter, value] 表示该行的参数取这个值。
  x = {
    (row, parameter, value): next(new_var)
    for row in range(array_size)
    for parameter, values in enumerate(PARAMETERS)
    for value in values
  }

  for row in range(array_size):
    for parameter, values in enumerate(PARAMETERS):
      variables = [x[row, parameter, value] for value in values]

      # 每个参数至少取一个值，并且至多取一个值。
      formula.append(variables)
      for first, second in combinations(variables, 2):
        formula.append([-first, -second])

    # forbidden tuple: not (P2 = 1 and P3 = 1)
    formula.append([-x[row, 1, 1], -x[row, 2, 1]])

  # 每个合法的 2-way 组合都必须至少出现在一行中。
  for first_parameter, second_parameter in combinations(range(4), 2):
    for first_value, second_value in product(
      PARAMETERS[first_parameter], PARAMETERS[second_parameter]
    ):
      if (first_parameter, first_value, second_parameter, second_value) == (1, 1, 2, 1):
        continue

      witnesses = []
      for row in range(array_size):
        witness = next(new_var)
        witnesses.append(witness)
        first = x[row, first_parameter, first_value]
        second = x[row, second_parameter, second_value]

        # witness <-> (first and second)
        formula.append([-witness, first])
        formula.append([-witness, second])
        formula.append([witness, -first, -second])

      formula.append(witnesses)

  return formula, x

def generate_covering_array() -> list[list[int]]:
  formula, x = encode(ARRAY_SIZE)
  formula.to_file(CNF_FILE)

  with Solver(bootstrap_with=formula) as solver:
    if not solver.solve():
      raise RuntimeError(f"array size = {ARRAY_SIZE} is UNSAT")

    model = set(solver.get_model())
    return [
      [
        next(value for value in values if x[row, parameter, value] in model)
        for parameter, values in enumerate(PARAMETERS)
      ]
      for row in range(ARRAY_SIZE)
    ]

if __name__ == "__main__":
  covering_array = generate_covering_array()

  print(f"CNF written to {CNF_FILE}")
  print(f"array size = {len(covering_array)}")
  print("P1 P2 P3 P4")
  for test_case in covering_array:
    print(*test_case)