Infrastructure to run a Sat solver as a command #4303

Coloquinte · 2024-03-28T15:13:20Z

As discussed on the slack channel, here is a patch for a solver interface using an arbitrary command (I used kissat for my test).
It also removes some unused code that was supposed to register arbitrary solvers.

As the moment, it is only usable for experimental purposes from the C++. I didn't implement any direct access from the command line (sat, equiv, ...)

povik · 2024-03-28T15:38:46Z

kernel/register.cc

-SatSolver *yosys_satsolver_list;
-SatSolver *yosys_satsolver;
-
-struct MinisatSatSolver : public SatSolver {


I am not sure we want this removed. This allowed for a plugin to register a different SAT solver, though I am not sure yosys_satsolver_list gets used anywhere, so that the other-than-default solver would ever get selected.

Looks like we are missing a command satselect, solverselect or similar which would update the yosys_satsolver pointer, but the overall approach of these SatSolver descendants appears sane. On the contrary, instead of removing this, we should arrange for an ezcommand solver to be instantiable through this.

Thanks for your explanation, now I see the benefit. I thought it was entirely unused.
I can just remove this commit and the next one: ezSATCommand would not be accessible from the global solver yet, but would at least be available from C++ plugins.

I like your idea of a solver selection command, although I don't know if there's a need for Sat solver selection. kissat or cadical are difficult to beat, and the only reason to select a non-default solver is because minisat is outdated

That's a good point. I will defer to @jix's judgement on this. Should we e.g. always override the default solver with the one from a plugin, if available?

It would be nice to have a way to override the default solver, that would also make it easier to test this PR. I don't want to change the default without an explicit command though (sat -select-solver ... could be added, there is precedent for subcommand like options and it would avoid cluttering the command list, but maybe also make it a bit hard to discover)

libs/ezsat/ezcommand.cc

povik · 2024-03-28T16:02:43Z

libs/ezsat/ezcommand.cc

+	for (auto id : assumptions)
+		extraClauses.push_back({bind(id)});
+
+	printDIMACS(dimacs, false, extraClauses);


Would there be issues with appending the extra clauses to the file from here, instead of introducing a new argument to printDIMACS? I see printDIMACS finds out the maximum term or clause number to arrange for uniform padding, but is that a requirement of the format or just a convenience for inspection?

I preferred to extend printDIMACS rather than duplicate the writing code. You'd prefer not to change the API?

It depends on how much code would be duplicated in practice. How much lines would you estimate that to be?

Not that many actually, less than 10

As pointed out by Jix, the number of clauses is in the header, so we cannot actually add this afterwards

Makefile

kernel/yosys.cc

passes/cmds/show.cc

passes/cmds/viz.cc

kernel/fstdata.cc

kernel/register.cc

kernel/yosys.cc

jix

On top of the comments I left inline, there's no easy way to actually test this without manually patching the default or writing a plugin making direct use of it. This should come with either a way to change the default solver or an example plugin with a test case.

kernel/yosys.cc

jix · 2024-04-08T11:57:37Z

libs/ezsat/ezsat.cc

@@ -1259,6 +1259,8 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
 	std::vector<std::vector<int>> all_clauses;
 	getFullCnf(all_clauses);
 	assert(cnfClausesCount == int(all_clauses.size()));
+	for (auto c : extraClauses)
+		all_clauses.push_back(c);

 	fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);


This will print a broken DIMACS CNF header with an incorrect clause count when extraClauses is non-empty.

Right I shouldn't have bolted on this part to handle assumptions as I don't use them myself

jix · 2024-04-08T12:06:21Z

libs/ezsat/ezcmdline.cc

+			}
+		}
+	};
+	if (Yosys::run_command(sat_command, line_callback) != 0) {


Many solvers follow the convention that they exit with status 10 for satisfiable and with status 20 for unsatisfiable instances, so those exit code shouldn't be treated as an error if they match result parsed from the log output.

jix · 2024-04-08T12:15:48Z

kernel/register.cc

-SatSolver *yosys_satsolver_list;
-SatSolver *yosys_satsolver;
-
-struct MinisatSatSolver : public SatSolver {


It would be nice to have a way to override the default solver, that would also make it easier to test this PR. I don't want to change the default without an explicit command though (sat -select-solver ... could be added, there is precedent for subcommand like options and it would avoid cluttering the command list, but maybe also make it a bit hard to discover)

povik assigned jix Mar 28, 2024