Life

前段时间晚上跑步顶不住，太冷了，现在温度稍微好转，一周两次五公里吧。做点室内的锻炼活动。

每天五十个俯卧撑。。。

每周还是有个固定时间看看电视，游戏放松下。

这周没有吃外卖，健康的一周 😊。

感觉双休日每次吃完饭可以散步半小时左右。

Share

SAT Solver

repo 写了个 Sudoku 使用 SAT 来解(Boolean satisfiability problem)

例如 3\*3 的 board
X X 3
4 X 6
7 8 X

条件有：
外维数组是里的元素是and的关系
里面子数组里的元素是or的关系
[
  [((0,2,3), True)], //表示(0,2)的位置是3 And
  ...
  [((2,1,8), True)],
  // 按下面的思想, 继续列出所有条件，这里只举例
  // 即 (0,0)==2 and (0,1)!=2 and (0,2)!=2
  [((0,0,2), True)]
  [((0,1,2), False)]
  [((0,2,2), False)]

  ...
]

思想:

  • 初始化已经在 board 上确定的元素的条件。
  • 对于每个 cell 要求只能是 1-9 中的数，并且不能出现两种情况(即是 1 又是 2)。
  • 每行，每列要求只能出现一次是 1-9。如行要求举例:Pos(0,0)=1 时要求 Pos(0,1)..Pos(0,8)不能是 1。
  • 同理对 3*3 块做要求。
// SudokuBoardToSatFormula converts a sudoku board to a SAT formula
func SudokuBoardToSatFormula(sudokuBoard [][]int) Formula {
	N := 9
	n := 3
	formula := Formula{}

	// Initial state constraints
	for r := 0; r < N; r++ {
		for c := 0; c < N; c++ {
			d := sudokuBoard[r][c]
			if d != 0 {
				literal := Literal{Variable: literalVar(r, c, d), Value: true}
				clause := Clause{literal}
				formula = append(formula, clause)
			}
		}
	}

	// Cell constraints
	for r := 0; r < N; r++ {
		for c := 0; c < N; c++ {
			// At least one number in each cell
			clause := Clause{}
			for d := 1; d <= N; d++ {
				clause = append(clause, Literal{Variable: literalVar(r, c, d), Value: true})
			}
			formula = append(formula, clause)

			// At most one number in each cell
			for i := 1; i <= N; i++ {
				clause = Clause{}
				for j := i + 1; j <= N; j++ {
					clause = append(clause, Literal{Variable: literalVar(r, c, i), Value: false},
						Literal{Variable: literalVar(r, c, j), Value: false})
				}
				if len(clause) > 0 {
					formula = append(formula, clause)
				}
			}
		}
	}

	// Row and Column constraints
	for d := 1; d <= N; d++ {
		for r := 0; r < N; r++ {
			// Row constraint
			clause := Clause{}
			for c := 0; c < N; c++ {
				clause = append(clause, Literal{Variable: literalVar(r, c, d), Value: true})
			}
			formula = append(formula, clause)

			// Column constraint
			clause = Clause{}
			for c := 0; c < N; c++ {
				clause = append(clause, Literal{Variable: literalVar(c, r, d), Value: true})
			}
			formula = append(formula, clause)

			// At most one number in each row and column
			for c1 := 0; c1 < N; c1++ {
				for c2 := c1 + 1; c2 < N; c2++ {
					formula = append(formula, Clause{
						Literal{Variable: literalVar(r, c1, d), Value: false},
						Literal{Variable: literalVar(r, c2, d), Value: false},
					}, Clause{
						Literal{Variable: literalVar(c1, r, d), Value: false},
						Literal{Variable: literalVar(c2, r, d), Value: false},
					})
				}
			}
		}
	}

	// Block constraints
	for d := 1; d <= N; d++ {
		for br := 0; br < n; br++ {
			for bc := 0; bc < n; bc++ {
				// At least one number in each block
				clause := Clause{}
				for rr := 0; rr < n; rr++ {
					for cc := 0; cc < n; cc++ {
						clause = append(clause, Literal{Variable: literalVar(br*n+rr, bc*n+cc, d), Value: true})
					}
				}
				formula = append(formula, clause)

				// At most one number in each block
				for i := 0; i < n*n; i++ {
					for j := i + 1; j < n*n; j++ {
						r1, c1 := i/n, i%n
						r2, c2 := j/n, j%n
						formula = append(formula, Clause{
							Literal{Variable: literalVar(br*n+r1, bc*n+c1, d), Value: false},
							Literal{Variable: literalVar(br*n+r2, bc*n+c2, d), Value: false},
						})
					}
				}
			}
		}
	}

	return formula
}

在一台机器上模拟 Kubernetes 的方式

Algorithm

1235. Maximum Profit in Job Scheduling

思路:

  • 首先对每个 job 按 start time 排序
  • DFS 搜索，对于 job[i]，只有选，不选两个选项
    • 不选，那么就遍历 job[i+1]
    • 选，寻找 job[i] end time 后 job[j]
      • 这里可以使用二分搜索优化，找第一个>=job[i][endtime]
  • 结果就是对两个选择取 max
from typing import List
import bisect

class Solution:
    def jobScheduling(
        self, startTime: List[int], endTime: List[int], profit: List[int]
    ) -> int:
        """
        DFS搜索: 对当前i job是否选或不选两种情况遍历。
        """
        intervals = sorted(zip(startTime, endTime, profit))
        cache = {}

        def dfs(i: int):
            if i == len(intervals):
                return 0
            if i in cache:
                return cache[i]

            # dont include i job
            res = dfs(i + 1)

            # include i job
            # j = i + 1
            # while j < len(intervals):
            #     if intervals[i][1] <= intervals[j][0]:
            #         break
            #     j += 1
            j = bisect.bisect_left(intervals, (intervals[i][1], -1, -1))
            cache[i] = res = max(res, intervals[i][2] + dfs(j))

            return res

        return dfs(0)