Biểu thức Boolean cho vấn đề Queens đã sửa đổi

Question

Tôi đã thấy các biểu thức boolean cho bài toán N Queens từ đây .

Quy tắc N nữ hoàng đã sửa đổi của tôi đơn giản hơn:

Đối với bàn cờ ap * p, tôi muốn đặt N quân hậu theo cách sao cho

1. Các nữ hoàng sẽ được đặt liền kề, các hàng sẽ được điền trước.
2. p * p kích thước bàn cờ sẽ được điều chỉnh cho đến khi nó có thể chứa N quân hậu

Ví dụ: giả sử N = 17, thì chúng ta cần một bàn cờ 5 * 5 và vị trí sẽ là:

Q_Q_Q_Q_Q
Q_Q_Q_Q_Q
Q_Q_Q_Q_Q
Q_Q_*_*_*
*_*_*_*_*

Câu hỏi là tôi đang cố gắng đưa ra một biểu thức boolean cho vấn đề này .

Answer 1

Vấn đề này có thể được giải quyết bằng cách sử dụng các gói Python humanizevà omega.

"""Solve variable size square fitting."""
import humanize
from omega.symbolic.fol import Context


def pick_chessboard(q):
    ctx = Context()
    # compute size of chessboard
    #
    # picking a domain for `p`
    # requires partially solving the
    # problem of computing `p`
    ctx.declare(p=(0, q))
    s = '''
       (p * p >= {q})  # chessboard fits the queens, and
       /\ ((p - 1) * (p - 1) < {q})  # is the smallest such board
       '''.format(q=q)
    u = ctx.add_expr(s)
    d, = list(ctx.pick_iter(u))  # assert unique solution
    p = d['p']
    print('chessboard size: {p}'.format(p=p))
    # compute number of full rows
    ctx.declare(x=(0, p))
    s = 'x = {q} / {p}'.format(q=q, p=p)  # integer division
    u = ctx.add_expr(s)
    d, = list(ctx.pick_iter(u))
    r = d['x']
    print('{r} rows are full'.format(r=r))
    # compute number of queens on the last row
    s = 'x = {q} % {p}'.format(q=q, p=p)  # modulo
    u = ctx.add_expr(s)
    d, = list(ctx.pick_iter(u))
    n = d['x']
    k = r + 1
    kword = humanize.ordinal(k)
    print('{n} queens on the {kword} row'.format(
        n=n, kword=kword))


if __name__ == '__main__':
    q = 10  # number of queens
    pick_chessboard(q)

Biểu diễn phép nhân (và phép chia số nguyên và mô đun) bằng sơ đồ quyết định nhị phân có độ phức tạp theo cấp số nhân với số lượng biến, như được chứng minh trong: https://doi.org/10.1109/12.73590