MCP Solver

In multi-state problems (like colored nonograms or multi-skill scheduling), cells/slots of one state can act as separators for runs of another state.

The Anti-Pattern: Requiring every non-empty cell to belong to a run. This over-constrains the model and causes false UNSAT results because it forbids the 'separator' cells.

The Correct Pattern: Focus ONLY on enforcing the properties of the runs themselves (position, length, color) and let the solver determine the separators naturally.

1. Generate Run Positions: Use choice rules to pick starting positions for runs.
2. Enforce Run Consistency: Constrain cells within the run to match the required color/state.
3. Enforce Ordering: Ensure runs appear in the correct sequence.
4. Enforce Separation for Identical States: Only require gaps between runs of the same color/state. Different states/colors are allowed to be adjacent.

Multi-Color Nonogram Pattern:

% 1. Define possible starting positions
{ row_run_pos(R, RunIdx, StartCol) : possible_start(StartCol) } 1 :- row_clue(R, RunIdx, _, _).

% 2. Cells within run must match run's color
:- row_run_pos(R, RunIdx, Start), row_clue(R, RunIdx, ReqColor, Len), 
   col(C), C >= Start, C < Start + Len, 
   cell(R, C, ActualColor), ActualColor != ReqColor.

% 3. Runs must appear in order
:- row_run_pos(R, I1, C1), row_run_pos(R, I2, C2), 
   row_clue(R, I1, _, L1), I2 = I1 + 1, C2 < C1 + L1.

% 4. Runs of SAME color must be separated
:- row_run_pos(R, I1, C1), row_run_pos(R, I2, C2), 
   row_clue(R, I1, SameColor, L1), row_clue(R, I2, SameColor, _), 
   I1 < I2, C2 < C1 + L1 + 1.

% Runs of SAME color must be separated (different colors can touch)
:- row_run_pos(R, I1, C1), row_run_pos(R, I2, C2), 
   row_clue(R, I1, SameColor, L1), row_clue(R, I2, SameColor, _), 
   I1 < I2, C2 < C1 + L1 + 1.

Every variable in an ASP rule MUST be grounded. A variable is grounded if it appears in at least one positive, non-aggregate, non-arithmetic literal in the rule's body. This tells the solver which domain of values to check.

Grounding with Negation (not)

Any variable used inside a not literal must be grounded by a positive literal elsewhere in the same rule body.

• Incorrect: unassigned(T) :- not assigned(T, W). (Variable W is unsafe because the solver doesn't know which workers to check).
• Correct: unassigned(T) :- task(T), not assigned(T, _). (task(T) grounds T, and _ is used for the unknown worker).

Grounding in Choice Rules

Variables in choice rules {...} must be grounded either in the choice domain or in the rule body.

• Incorrect: {chosen(X, Var1, Var2)} :- domain(X). (Var1 and Var2 are unsafe).
• Correct (Option 1 - Choice Domain): {chosen(X, Var1, Var2) : property1(Var1), property2(Var2)} :- domain(X).
• Correct (Option 2 - Rule Body): {chosen(X, Var1, Var2)} :- domain(X), property1(Var1), property2(Var2).

% SAFE: Variable S is grounded by shelf(S)
:- item(I), shelf(S), not on_shelf(I, S).

% SAFE: Grounding in choice domain
{assign(Task, Worker, Priority) : worker(Worker), priority(Priority)} :- task(Task).

The clingo.Model object passed to the on_model callback is only valid during the execution of that callback.

CRITICAL: Do not store the Model object itself in a global variable or any structure that outlives the callback. Accessing a Model object after ctl.solve() has returned will cause a segmentation fault (exit code 139) because the underlying memory has been freed.

Correct Pattern: Inside the on_model callback, iterate through the symbols and extract the necessary data into plain Python types (strings, integers, tuples, or dictionaries).

# WRONG - causes segmentation fault
saved = None
def on_model(m):
    global saved
    saved = m
ctl.solve(on_model=on_model)
atoms = saved.symbols(atoms=True) # SIGSEGV

# CORRECT - extract data into plain Python objects
result = []
def on_model(m):
    for a in m.symbols(atoms=True):
        if a.match("assigned", 2):
            # Convert to plain tuple of strings
            result.append((str(a.arguments[0]), str(a.arguments[1])))
ctl.solve(on_model=on_model)
# 'result' is safe to use here

In Answer Set Programming (ASP), distinguishing between constants and variables is critical to avoid 'unsafe variable' errors.

• Constants (Symbols): Must start with a lowercase letter, be a number, or be enclosed in double quotes "". Use double quotes for any input data that contains uppercase letters.

  • item(apple). (lowercase)
  • cost(100). (number)
  • amino_acid(1, "H"). (quoted string)

• Variables: Must start with an uppercase letter or an underscore _.

  • has_color(Item, Color) :- ...
  • cost(X, C) :- ...

Common Mistakes:

• amino_acid(1, H). $\rightarrow$ Incorrect (H is treated as an undefined variable).
• amino_acid(1, "H"). $\rightarrow$ Correct.
• player(P1). $\rightarrow$ Incorrect (P1 is an uppercase variable).
• player(p1). or player("P1"). $\rightarrow$ Correct.

% Correct usage of constants and variables
item(apple).
cost(100).
amino_acid(1, "H").

% Correct usage of variables in rules
has_color(Item, Color) :- item(Item), color(Color).