SAT — propositional CNF

% at-least-one per row (n clauses):
(q(1,1)∨q(1,2)∨q(1,3)∨q(1,4)), (q(2,1)∨…), …
% at-most-one per row (n·C(n,2) clauses):
(¬q(1,1)∨¬q(1,2)), (¬q(1,1)∨¬q(1,3)), …
% col uniqueness + diagonal: similarly
…

ASP — requires auxiliary predicate

{ queen(R,C) } :- row(R), col(C).
atrow(R) :- queen(R,C).      % ← not in the problem statement
:- row(R), not atrow(R).
…
:- queen(R,C1), queen(R,C2), C1 != C2.
:- queen(R1,C), queen(R2,C), R1 != R2.
:- queen(R1,C1), queen(R2,C2),
   R1 != R2, |R1-R2| == |C1-C2|.

Form

#false :- B1, B2, …, Bm.

Usually written with the head omitted: :- B1, …, Bm.

Constraint rule: remove any stable model where $B_1 \land \cdots \land B_m$ holds.

Intuition: "it must never be the case that …" — a hard pruning rule.

Example — adding a constraint

a :- not b.
b :- not a.
:- b.        % b must not hold

Without constraint: stable models {a} and {b}.

list: heap sequence of values ending at nil — base + inductive case, separating conjunction *

We want more: a sorted list tracking its payload set $S$
→ predicate srtl(x, S)

Why hard to write?

• Separating conjunction *: non-trivial disjoint-heap reasoning
• Recursion + existentials: base case, inductive case, pointer ∃j
• Pure payload constraint: min_set(V, S) embedded in recursion

Can we synthesise them automatically from examples?

Specificity order on candidate predicates:

f2 is strictly more specific than f1 — f1 is redundant and pruned.

Candidate search space normalised by entailment:
each equivalence class under $\models_{SL}$ contains only one representative — the most specific member. ILP then searches over these classes, not raw predicates.

A transition system $\mathcal{T} = \langle S, I, T \rangle$:

• $S$: set of FO states over vocabulary $\Sigma$ (nodes, quorums, messages, …)
• $I(V) \subseteq S$: initial states
• $T(V,V') \subseteq S \times S$: transition relation (protocol actions)

Safety: every reachable state must lie in $P$.
Cannot be proved by simulation (a.k.a. model checking) alone, via inductive invariant $\mathit{Inv}$ instead.

For Paxos, the invariant is a conjunction of 6+ FOL formulas over 5 relations — non-trivial to find manually.

DuoAI (OSDI '22)

• Enumerate all FOL formulas satisfied by protocol traces
• Houdini: iteratively prune to strongest consistent subset
• Implication graph: avoid re-testing formulas implied by checked ones
• Handles Paxos, FlexiblePaxos, Multi-Paxos, …

Scalability gap: Paxos 60.4 s  ·  MultiPaxos 1549 s
Enumeration dominates — each root formula prunes very few leaves.

State of the art: DuoAI

• Enumerate + Houdini: finds all FOL formulas satisfied by example traces
• Implication graph: pruning satisfied roots skips implied leaves
• Successfully handles Paxos, FlexPaxos, and more

Scalability limit: enumeration dominates at scale
Paxos: 60.4 s  |  MultiPaxos: 1549 s

FORCE: improve the synthesis sub-routine itself — applicable to both one-shot and multi-shot inference frameworks.

Definition

Given: bounded search space $\Omega_0$ + a set of FO structures $\sigma = \{M_1,\ldots,M_k\}$

Find: $\Phi \subseteq \Omega_0$ s.t. every $\phi \in \Phi$:

1. $\forall M \in \sigma.\ M \models \phi$   (satisfies all structures)
2. is closed (no free variables)
3. is non-tautological
4. no formula in $\Phi$ entails another   (most precise set)

Instantiated for invariant synthesis: $\sigma$ = protocol traces; $\Omega_0$ = prenex-DNF formulas over the protocol vocabulary. The conjunction of $\Phi$ is the candidate invariant.

Tiny example

Output $\Phi$:

$\forall X.\ p(X) \lor q(X)$

$\forall X.\ p(X) \lor \neg r(X)$

Both satisfied by $M_1$ and $M_2$; neither entails the other.

Core ASP encoding:

{ holds(I,J) } :- clause(I), lit(J).   % choose literals
:- holds(I,J), holds(I,K), neg(J,K).   % no P and ¬P in same clause
      

Static pruning via constraints:

• Symmetry: permute quantifier variables to canonical form
• Decomposability: if $A \equiv B \land C$, prune $A$ (search $B$ and $C$ separately)

250 + 80 lines of ASP encoding the entire search space and pruning rules.

SAT — CNF

% each cell exactly one number:
∧R,C(∨A l(R,C,A)) ∧ ∧R,C,A1<A2(¬l(R,C,A1)∨¬l(R,C,A2))
% row uniqueness (at-most-one per row):
∧R,A,C1<C2(¬l(R,C1,A)∨¬l(R,C2,A))
% col uniqueness (at-most-one per col):
∧C,A,R1<R2(¬l(R1,C,A)∨¬l(R2,C,A))
% n=10: >12,000 clauses — enumerate all manually

ASP — requires auxiliary predicate

{ l(R,C,A) } :- dom(R), dom(C), dom(A).
latin_aux(R,C) :- l(R,C,A).    % ← auxiliary: not in the problem
:- dom(R), dom(C), not latin_aux(R,C).
:- dom(R), dom(C), l(R,C,A1),  l(R,C,A2),  A1 < A2.
:- dom(R), dom(A), l(R,C1,A),  l(R,C2,A),  C1 < C2.
:- dom(C), dom(A), l(R1,C,A),  l(R2,C,A),  R1 < R2.

SetLah! — direct FOL

l(R,C,A) ?:- dom(R), dom(C), dom(A).
∀R,C. (∃A. l(R,C,A) ∧ ∀A1,A2. l(R,C,A1)∧l(R,C,A2)→A1=A2)
∀R,A,C1,C2. l(R,C1,A) ∧ l(R,C2,A) → C1=C2
∀C,A,R1,R2. l(R1,C,A) ∧ l(R2,C,A) → R1=R2

Reads as the problem statement · compiled automatically to ASP

First-Order Integrity Constraint (IC)

Universal formula with $\bot$ as consequent:

$\forall \bar{x}.\ \varphi(\bar{x}) \rightarrow \bot$

Equivalently: $\neg\exists\bar{x}.\ \varphi(\bar{x})$ — no model of $\varphi$ should exist.

Native ASP rule: :- Body.  $\longleftrightarrow$  $\forall \bar{x}.\ \underbrace{\mathit{Body}(\bar{x})}_{\varphi} \rightarrow \bot$

Gap: quantifier alternation (e.g., $\forall\exists$) makes formula non-IC.
SetLah! compiles any FOL constraint into IC form.

Compilation target: IC (+ auxiliary atoms/aggregates) — ready for the ASP grounder.

✓ "At most one" per cell — IS IC:

$\forall R,C,A_1,A_2.\ l(R,C,A_1)\wedge l(R,C,A_2) \rightarrow A_1=A_2$

:- l(R,C,A1), l(R,C,A2), A1 != A2.

Pure implication — no existential. Directly expressible as IC.

✗ "Exactly one" per cell — cannot be expressed as IC:

$\forall R,C.\ \bigl(\exists A.\ l(R,C,A)\bigr)\ \wedge\ \bigl(\forall A_1,A_2.\ l(R,C,A_1)\wedge l(R,C,A_2)\to A_1=A_2\bigr)$

Two Latin squares l, g on the same grid: every pair $(l(R,C), g(R,C))$ appears in exactly one cell.

blue = l  ·  green = g

SetLah! — three stratified blocks

[dom(1). dom(2). dom(3).]             % Block 1: domain

[  % Block 2 — Latin square l
  l(R,C,A) ?:- dom(R), dom(C), dom(A).
  ∀R,C. (∃A. l(R,C,A) ∧ ∀A1,A2. l(R,C,A1)∧l(R,C,A2)→A1=A2)
  ∀R,A,C1,C2. l(R,C1,A) ∧ l(R,C2,A) → C1=C2
  ∀C,A,R1,R2. l(R1,C,A) ∧ l(R2,C,A) → R1=R2
]

[  % Block 3 — Latin square g + orthogonality
  g(R,C,B) ?:- dom(R), dom(C), dom(B).
  ∀R,C. (∃B. g(R,C,B) ∧ ∀B1,B2. g(R,C,B1)∧g(R,C,B2)→B1=B2)
  ∀R,B,C1,C2. g(R,C1,B) ∧ g(R,C2,B) → C1=C2
  ∀C,B,R1,R2. g(R1,C,B) ∧ g(R2,C,B) → R1=R2
  ∀A,B. ∃R,C. l(R,C,A) ∧ g(R,C,B)   % orthogonality: each pair once
]

Euler's conjecture (1782): no GL-square for $n \equiv 2 \pmod{4}$. Disproved ~180 years later.
SetLah! finds a counterexample for $n{=}10$ in 10 minutes.