Symmetry breaking is a crucial technique in modern combinatorial solving, but it is difficult to be sure it is implemented correctly. The most successful approach to deal with bugs is to make solvers certifying, so that they output not just a solution, but also a mathematical proof of correctness in a standard format, which can then be checked by a formally verified checker. This requires justifying symmetry reasoning within the proof, but developing efficient methods for this has remained a long-standing open challenge. A fully general approach was recently proposed, but it relies on encoding lexicographic orders with big integers, which quickly becomes infeasible for large symmetries. In this work, we develop a method for instead encoding orders with auxiliary variables. We show that this leads to orders-of-magnitude speed-ups in both theory and practice by running experiments on proof logging and checking for SAT symmetry breaking using the state-of-the-art satsuma symmetry breaker and the VeriPB proof checking toolchain.

A constraint programming (CP) solver that implements proof logging will output a machine-checkable certificate of correctness alongside any result it obtains. This is useful for trusting claims of unsatisfiability or optimality, as well as for debugging and auditing solver implementations. Proofs can be constructed by having the solver log justifications for each inference it makes, and previous work has shown that many standard CP reasoning techniques can be efficiently justified using a pseudo-Boolean (PB) proof format. This paper extends PB justifications to propagators enforcing bounds consistency on multiplication and division constraints. We show that even though the proof system and checker operate only on linear inequalities over 0-1 variables, non-linear reasoning over bounded domains can be efficiently expressed as a sequence of PB proof steps. Additionally, we demonstrate that bespoke proof logging for bounds-consistency algorithms offers a clear advantage over constructing justifications by brute force.

Bigraph reactive systems offer a powerful and flexible mathematical framework for modelling both spatial and non-spatial relationships between agents, with practical applications in domains such as smart technologies, networks, sensor systems, and biology. While bigraphs theoretically support the identification of bisimilar agents, by simulating and comparing their corresponding minimal contextual transition systems, no known algorithm exists for computing the maximum shared structure between two bigraphs, an essential prerequisite for determining the set of possible transitions for a given agent state. In this work, we provide a definition of the maximum common bigraph problem, and present an adaptation of the McSplit maximum common induced subgraph algorithm to compute the maximum common bigraph between two bigraph states. Our approach opens a path toward supporting bisimulation checking in bigraph-based tools, which have been leveraged in other modelling paradigms for simplification, optimisation, and verification of models.

Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver.

Modern subgraph-finding algorithm implementations consist of thousands of lines of highly optimized code, and this complexity raises questions about their trustworthiness. Recently, some state-of-the-art subgraph solvers have been enhanced to output machine-verifiable proofs that their results are correct. While this significantly improves reliability, it is not a fully satisfactory solution, since end-users have to trust both the proof checking algorithms and the translation of the high-level graph problem into a low-level 0-1 integer linear program (ILP) used for the proofs. In this work, we present the first formally verified toolchain capable of full end-to-end verification for subgraph solving, which closes both of these trust gaps. We have built encoder frontends for various graph problems together with a 0-1 ILP (a.k.a. pseudo-Boolean) proof checker, all implemented and formally verified in the CakeML ecosystem. This toolchain is flexible and extensible, and we use it to build verified proof checkers for both decision and optimization graph problems, namely, subgraph isomorphism, maximum clique, and maximum common (connected) induced subgraph. Our experimental evaluation shows that end-to-end formal verification is now feasible for a wide range of hard graph problems.

Proof logging in constraint programming is an approach to certifying a conclusion reached by a solver. To allow for this, different propagators must be augmented to produce justifications for any inferences they make, so that an independent proof checker can certify correctness. The Circuit constraint is used to enforce a Hamiltonian cycle on a set of vertices, e.g. for vehicle routing. Maintaining consistency for the Circuit constraint is hard, so various ad-hoc propagation techniques have been devised and implemented in solvers. We show that standard Circuit constraint inference rules can be efficiently justified within a pseudo-Boolean proof system, either by using a simple sequence of cutting planes steps or through a conditional counting argument.

Proof logging provides an auditable way of guaranteeing that a solver has produced a correct answer using sound reasoning. This is standard practice for Boolean satisfiability solving, but for constraint programming, a challenge is that every propagator must be able to justify all inferences it performs. Here we demonstrate how to support proof logging for a wide range of previously uncertified global constraints. We do this by showing how to justify every inference that could be performed by the propagation algorithms for two families of generalised extensional constraint: "Smart Table" and "Regular Language Membership".

Proof logging provides an auditable way of guaranteeing that a solver has produced a correct answer using sound reasoning. This is standard practice for Boolean satisfiability solving, but for constraint programming, a challenge is that every propagator must be able to justify all inferences it performs. Here we demonstrate how to support proof logging for a wide range of previously uncertified global constraints. We do this by showing how to justify every inference that could be performed by the propagation algorithms for two families of generalised extensional constraint: "Smart Table" and "Regular Language Membership".

Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly.Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

We describe the design and implementation of a new constraint programming solver that can produce an auditable record of what problem was solved and how the solution was reached. As well as a solution, this solver provides an independently verifiable proof log demonstrating that the solution is correct. This proof log uses the VeriPB proof system, which is based upon cutting planes reasoning with extension variables. We explain how this system can support global constraints, variables with large domains, and reformulation, despite not natively understanding any of these concepts. 2012 ACM Subject Classification Theory of computation → Logic and verification; Theory of computation → Discrete optimization Supplementary Material Source code for the solver described in this paper can be found here: (Source Funding Stephan Gocht : Supported by the Swedish Research Council grant 2016-00782. Ciaran McCreesh : Supported by a Royal Academy of Engineering research fellowship. Jakob Nordström : Supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B.

In this paper, we revisit the approach to empirical experiments for combinatorial solvers. We provide a brief survey on tools that can help to make empirical work easier. We illustrate origins of uncertainty in modern hardware and show how strong the influence of certain aspects of modern hardware and its experimental setup can be in an actual experimental evaluation. More specifically, there can be situations where (i) two different researchers run a reasonable-looking experiment comparing the same solvers and come to different conclusions and (ii) one researcher runs the same experiment twice on the same hardware and reaches different conclusions based upon how the hardware is configured and used. We investigate these situations from a hardware perspective. Furthermore, we provide an overview on standard measures, detailed explanations on effects, potential errors, and biased suggestions for useful tools. Alongside the tools, we discuss their feasibility as experiments often run on clusters to which the experimentalist has only limited access. Our work sheds light on a number of benchmarking-related issues which could be considered to be folklore or even myths.

The subgraph isomorphism problem is to find a small “pattern” graph inside a larger “target” graph. There are excellent dedicated solvers for this problem, but they require substantial programming effort to handle the complex side constraints that often occur in practical applications of the problem; however, general purpose constraint solvers struggle on more difficult graph instances. We show how to combine the state of the art Glasgow Subgraph Solver with the Minion constraint programming solver to get a “subgraphs modulo theories” solver that is both performant and flexible. We also show how such an approach can be driven by the Essence high level modelling language, giving ease of modelling and prototyping to non-expert users. We give practical examples involving temporal graphs, typed graphs from software engineering, and costed subgraph isomorphism problems.

Graph homomorphism problems involve finding adjacency-preserving mappings between two given graphs. Although theoretically hard, these problems can often be solved in practice using constraint programming algorithms. We show how techniques from the state-of-the-art in subgraph isomorphism solving can be applied to broader graph homomorphism problems, and introduce a new form of filtering based upon clique-finding. We demonstrate empirically that this filtering is effective for the locally injective graph homomorphism and subgraph isomorphism problems, and gives the first practical constraint programming approach to finding general graph homomorphisms.

Bigraphs simultaneously model the spatial and non-spatial relationships between entities, and have been used for systems modelling in areas including biology, networking, and sensors. Temporal evolution can be modelled through a rewriting system, driven by a matching algorithm that identifies instances of bigraphs to be rewritten. The previous state-of-the-art matching algorithm for bigraphs with sharing is based on Boolean satisfiability (SAT), and suffers from a large encoding that limits scalability and makes it hard to support extensions. This work instead adapts a subgraph isomorphism solver that is based upon constraint programming to solve the bigraph matching problem. This approach continues to support bigraphs with sharing, is more open to other extensions and side constraints, and improves performance by over two orders of magnitude on a range of problem instances drawn from real-world mixed-reality, protocol, and conference models.

A set of 11176 test instances for comparing the existing SAT solver found in BigraphER with the new Subgraph based solver using the Glasgow subgraph solver. See README for details. Also included in results.tar.xz are those presented in the paper.

Modern subgraph isomorphism solvers carry out sophisticated reasoning using graph invariants such as degree sequences and path counts. We show that all of this reasoning can be justified compactly using the cutting planes proofs studied in complexity theory. This allows us to extend a state of the art subgraph isomorphism enumeration solver with proof logging support, so that the solutions it outputs may be audited and verified for correctness and completeness by a simple third party tool which knows nothing about graph theory.