OptiLog
0.6.0

Contents:

  • Installation
  • End-user OptiLog API
    • Modelling Module
      • Basic Problem Modelling
      • Operators and parsing options
      • Equivalence of Python operators, Expression classes, and textual description
      • Solving a Problem with a SAT solver
      • Encoding Pseudo Boolean Expressions
    • Formulas Module
      • CNF Formula
        • CNF
        • CNFException
        • Methods sumary
      • WCNF Formula
        • WCNF
        • WCNFException
        • Methods sumary
      • QCNF Formula
        • QCNF
        • QCNFException
        • Methods sumary
      • VarManager
        • VarManager.copy()
        • VarManager.extend_vars()
        • VarManager.set_minimum_vars()
        • VarManager.add_var()
        • VarManager.max_var()
        • VarManager.new_var()
        • VarManager.get_lit()
      • Methods sumary
      • Formula Loading utilities
        • load_cnf()
        • load_wcnf()
        • load_qcnf()
      • Formula visualization
        • print_clauses_color()
    • Encoders Module
      • PB Encoder
        • Non-incremental encoders
        • Incremental encoders
    • Solvers Module
      • SAT Solver
        • Integrated SAT solvers
    • Tuning Module
      • Configurable parameters
        • Bool
        • Int
        • Real
        • Categorical
        • Choice
        • Dict
        • CfgCall
        • CfgCls
        • CfgObj
      • Configurable functions
        • Global configurable functions
        • Local configurable functions
        • Entrypoint functions
      • Configurable BlackBox
        • BlackBox Class as entrypoint
        • BlackBox Object as entrypoint
        • Extract BlackBox Command
        • BlackBox Class as global configurable
        • BlackBox as configurable parameter
      • Configurable utilities
        • The Choice parameter
      • Configuration scenario
        • TuningEntrypointType
        • TuningGlobalConfigurableType
        • GGAScenario
        • SMACScenario
      • Parsing Output
        • GGAParser
        • SMACParser
      • Usage example: Automatic Configuration of the Linear MaxSAT algorithm
    • Running Module
      • Introduction to the Running Module
      • Generating execution scenario
        • RunningSolverType
        • RunningScenario
        • Scenario with binary programs
        • Scenario with functions or BlackBox
      • Running the scenario
      • Examples for submit_file
        • Task Spooler
        • SGE
      • Parsing an execution scenario
        • parse_scenario()
        • ParsingInfo
    • BlackBox Module
      • Execution Constraints
        • ExecutionConstraints
        • RunSolver
        • DockerEnforcer
      • System Black Box
        • SystemBlackBox
        • BlackBoxRedirection
      • Satex Black Box
        • SatexBlackBox
  • Solver Developer
    • iSAT Interface
      • iSAT class
      • Solver states and Variables values
    • How to add a new solver to OptiLog
      • Implementing the iSAT interface
      • The Linking Functions
      • Compiling as a library
      • Loading the solver
  • Use Cases
    • The Slitherlink Problem
      • Modelling the Slitherlink Problem
      • Solving the Slitherlink Problem
        • Analyzing Inconsistent Subproblems
      • Tuning the Slitherlink Problem
      • Running the Slitherlink Problem
        • Processing Experimental Results
    • MaxSAT Competitions
      • Competition Generation
      • Competition Running
      • Competition Parsing
    • SAT Competitions
      • Competition Generation
      • Competition Running
      • Competition Parsing
  • References
  • Changelog
    • 0.6.0
    • 0.5.3
    • 0.5.2
    • 0.5.1
    • 0.5.0
    • 0.4.2
    • 0.4.1
    • 0.3.6
    • 0.3.5
    • 0.3.4
    • 0.3.3
    • 0.3.2
    • 0.3.1
    • 0.3.0
  • License
OptiLog
  • Use Cases
  • The Slitherlink Problem
  • Solving the Slitherlink Problem
  • View page source

Solving the Slitherlink Problem

In this section, we describe an incremental SAT-based solving approach (implemented in function solve_slitherlink) for the Slitherlink problem. We use the encoding described in the previous section to obtain a solution to the CNF formula generated in line~3 that guarantees that for each cell exactly the amount of edges described by the number associated with the cell are selected and they form a continuous path.

 1def solve_slitherlink(instance, seed, remove_unconstr_subcycles):
 2    sl = SlitherLink(instance)
 3    cnf = encode_slitherlink(sl)
 4    s = Cadical()
 5    s.set("seed", seed)
 6    s.add_clauses(cnf.clauses)
 7    while s.solve() is True:
 8        # The removal of unconstrained subcycles
 9        # (i.e. those that do not have any number)
10        # is optional, as there might be too many of them.
11        n_cycles = sl.manage_subcycles(s, cnf, remove_unconstr_subcycles)
12        if n_cycles == 1:
13            sl.visualize(s.model(), cnf)
14            print("s YES", flush=True)
15            return cnf.decode_dimacs(s.model())
16    print("s NO", flush=True)

Lines 4 and 5 instantiate the Cadical SAT solver and initialize it with a seed for the random number generator of the solver, and in line 6 we add to the solver the clauses generated by function encode_slitherlink. Then, we iteratively query the SAT solver (line 7) to provide a solution (a model).

In line 11, we call function manage_subcycles (which is part of the SlitherLink class) that checks the solution reported by the SAT solver. If there is more than one cycle it adds to the SAT solver the clauses that forbid these cycles in the solution. To find the cycles it uses the function find_cycles. To discard a cycle just adds to the SAT solver as a clause the negation of all the edges that conform to the cycle.

We also parameterize an option to remove the unconstrained cycles (those cycles that do not have any number), as there might be too many of them. On the other hand, it could be beneficial for the SAT solver to remove them. We will analyze this more in depth in the Tuning Slitherlink section.

1def manage_subcycles(self, solver, cnf, remove_unconstr_subcycles):
2    model = solver.model()
3    constr_cycles, unconstr_cycles = self.find_cycles(cnf.decode_dimacs(model))
4    if len(constr_cycles) > 1:
5        cycles = constr_cycles + unconstr_cycles if remove_unconstr_subcycles else constr_cycles
6        for subcycle in cycles:
7            negate_subcycle = [Not(edge) for edge in subcycle]
8            solver.add_clause(cnf.to_dimacs(negate_subcycle))
9    return len(constr_cycles)

Then, if only one cycle was found we are done and we have found a solution. We return the solution once decoded the model provided by the SAT solver (line 16). Otherwise, we will exit the main loop (line 7) if there is not a solution with just one cycle and we report the problem has no solution.

The full code for the find_cycles method (also part of the SlitherLink class) is shown below:

 1def unpack_edge(self, line):
 2    _, i, j, dir = line.name.split("_")
 3    return int(i), int(j), dir
 4
 5def find_cycles(self, model):
 6    activated = [edge for edge in model if not isinstance(edge, Not)]
 7    activated_map = {e.name: i for i, e in enumerate(activated)}
 8    seen = set()
 9    cycles = []
10    for i, init_edge in enumerate(activated):
11        if i in seen:
12            continue
13        cycle = []
14        cycles.append(cycle)
15        edge = init_edge
16        seen.add(i)
17        while edge is not None:
18            assert not isinstance(edge, int)
19            cycle.append(edge)
20            j, edge = self.find_next_activated(edge, activated_map, seen)
21            if j is not None:
22                seen.add(j)
23
24    constr_cycle, unconstr_cycle = [], []
25    for cycle in cycles:
26        if self.is_constr_cycle(cycle):
27            constr_cycle.append(cycle)
28        else:
29            unconstr_cycle.append(cycle)
30    return constr_cycle, unconstr_cycle
31
32def satisfies_cell(self, cycle):
33    for edge in cycle:
34        for i, j in self.get_nearby_cells(edge):
35            if self.cells[j][i] is not None:
36                return True
37    return False
38
39def get_nearby_cells(self, edge):
40    i, j, dir = self.unpack_edge(edge)
41    delta_i, delta_j = (0, 1) if dir == "right" else (1, 0)
42    cells = []
43    if i < self.m and j < self.n:
44        cells += [(i, j)]
45    if 0 < i and 0 < j:
46        cells += [(i - delta_i, j - delta_j)]
47    return cells
48
49def find_next_activated(self, edge, activated_map, seen):
50    for continues in self.get_continuation(edge):
51        j = activated_map.get(continues.name, None)
52        if j is None or j in seen:
53            continue
54        return j, continues
55    return None, None
56
57def get_continuation(self, edge):
58    i, j, _ = self.unpack_edge(edge)
59    ci, cj = self.get_pointing_coordinate(edge)
60    return self.vertex_edges(i, j) + self.vertex_edges(ci, cj)
61
62def get_pointing_coordinate(self, edge):
63    i, j, dir = self.unpack_edge(edge)
64    delta_i, delta_j = (1, 0) if dir == "right" else (0, 1)
65    return i + delta_i, j + delta_j

Analyzing Inconsistent Subproblems

In other solving strategies, the SAT solver can be used to check whether a partial assignment can be extended to a complete solution to the problem. This is the case for large problems solved through Large Neighborhood Search [PR10] techniques where we heuristically identify promising subproblems (neighbourhoods) and solve them completely, for example, with a SAT solver. If the subproblem is satisfiable we are done, if it is not, we can retrieve from the SAT solver the reason for this unsatisfiability which is referred to as the unsatisfiable core.

To define the subproblem we call the SAT solver on a set of assumptions that encode decisions on the edges. If there is no solution we can query the SAT solver about the core of unsatisfiability, i.e., a subset of assumptions that makes the problem unsatisfiable, as shown in the following example.

(...)
assumptions = cnf.to_dimacs(fixed_edges)
if not s.solve(assumptions):
    return cnf.decode_dimacs(s.core())
(...)

Equipped with the core, now we can decide which decisions in the core should be revoked. This can be done automatically or even with human support, depending on the application.

Previous Next

© Copyright 2023, Logic and Optimization Group.

Built with Sphinx using a theme provided by Read the Docs.