Seeking Expert Review for SAT Challenge Competition

The Innovation Game (TIG) are looking for an expert who can review the design of our 3-SAT challenge. The challenge is described here: https://www.tig.foundation/challenges/satisfiability.

About the TIG Protocol

TIG designs algorithmic challenges rooted in mathematics and related fields (computer science, physics, statistics, biology, etc.). The purpose of these challenges is to stimulate fundamental research and drive the development of novel algorithms with real-world applicability. Challenges are not intended to solve one-off practical instances. Instead, they are constructed to encourage participants to advance algorithmic methods.

For example, a SAT challenge should promote progress in SAT algorithm design as a field, rather than merely solving a single instance.

Algorithms may be implemented on either CPU or GPU, with the choice depending on which is more likely to produce innovation.

Core Requirements of a TIG Challenge

Importance: The problem should address a significant question in science or technology.
Asymmetry: Finding a solution for a given instance should require significantly more computational effort (time, resources) than checking whether a proposed solution is correct. e.g., for a given assignment of variables in a SAT problem, it is quick to check that a state evaluates to True.
Tuneable difficulty: A challenge includes at least two independent difficulty parameters. Increasing either parameter makes the problem harder or more computationally demanding. e.g., in SAT we use the number of variables and the ratio of clauses to variables.
Instance generation:
1. Unlimited: For a given fixed choice of difficulty parameters, the challenge must support unlimited i.i.d. instance generation. The generation process should consistently produce a high proportion of solvable (feasible) problems, though not every instance needs to have a guaranteed solution, e.g., in SAT, a generated instance that is UNSAT.
2. Non-trivial and Public: The generation process is public and available to all participants. Instance generation must therefore not trivially reveal the solution, e.g., an instance cannot be generated from a known solution.

For further details see the attached [official TIG challenge guide](https://github.com/tig-foundation/tig-monorepo/blob/blank_slate/docs/guides/challenge_design.pdf).

Particular Ask for This Bounty

We are looking for an expert to review and suggest improvements to the design of our 3-SAT challenge.

Key questions we would like input on include:

Choice of problem variant: Is 3-SAT a good/interesting choice of problem variant? Or would unrestricted SAT be more industrially/academically interesting?
Choice of difficulty parameters: Are the clauses to variables ratio and number of variables a suitable choice for the difficulty parameters (i.e., the instance difficulty increases monotonically with these parameters)? Additionally, should these parameters be capped to ensure instances remain in a feasible/interesting difficulty range?
Instance Generation: Is the current generation process of random 3-SAT instances interesting or should this be updated to include multiple types of 3-SAT instances, e.g., industrially relevant instances?
Reward Incentive: Currently, algorithms are rewarded for finding the most solutions, i.e, SAT instances, without taking into account that some of the generated instances are UNSAT (we cannot verify UNSAT instances due to the asymmetric requirement.) Is there a better way to reward the algorithms e.g., ensure we generate only SAT instances?

The full challenge description can be found here:https://www.tig.foundation/challenges/satisfiability.

Seeking Expert Review for SAT Challenge Competition

Seeking Expert Review for SAT Challenge Competition

Topics

DOI