Page MenuHomeFreeBSD

cmb(1) / cmb(3): import combinatorics utility and library
Needs ReviewPublic

Authored by dteske on Jul 5 2018, 3:14 AM.
Tags
None
Referenced Files
F166690747: D16132.id183333.diff
Sat, Aug 15, 3:04 PM
F166662801: D16132.id183022.diff
Sat, Aug 15, 8:25 AM
Unknown Object (File)
Fri, Aug 14, 10:22 AM
Unknown Object (File)
Fri, Aug 14, 1:58 AM
Unknown Object (File)
Thu, Aug 13, 4:37 PM
Unknown Object (File)
Wed, Aug 12, 5:59 PM
Unknown Object (File)
Wed, Aug 12, 5:58 PM
Unknown Object (File)
Wed, Aug 12, 5:33 PM

Details

Reviewers
emaste
adrian
eadler
0mp
bcr
imp
pstef
Group Reviewers
manpages
Summary

Add cmb(1) and libcmb(3) to base for enumerating combinations with
deterministic indexing, resume (-i), limits (-c/-k), and optional
OpenSSL bn(3) support for counts beyond 64-bit.

This fills the same niche as jot(1)/seq(1) for combinatorial expansion
and supports large enumerations (build-option surveys, ports option
matrices, filesystem/test corpus generation) without requiring a port.

Always built; libcrypto is optional. Without OpenSSL the library is
limited to 64-bit counts. With OpenSSL, -o still forces the non-bn(3)
path when large integers are not wanted. Use -v to check whether built
with OpenSSL.

Test Plan

Use it to generate combinations.

See the examples in the cmb(1) man-page

Diff Detail

Repository
rG FreeBSD src repository
Lint
Lint Skipped
Unit
Tests Skipped
Build Status
Buildable 75351
Build 72234: arc lint + arc unit

Event Timeline

There are a very large number of changes, so older changes are hidden. Show Older Changes

I'm going to set an ETIMEOUT of 30 days. If there is no objection, I will import to base HEAD.

Re-iterating the reasons why this should bypass ports and go to base:

This tool is being developed to ultimately aid base and ports functionality. If it exists in ports, it becomes like dialog4ports and has to be installed before you can extract all the functionality of ports.

I have ports that I want to use this in the Makefile and tools for base that I need to use this in (the build option survey, for example). Putting this in ports complicates those endeavors.

Hi Devin,

Could you elaborate more on your planned uses of this code in the base system? The build option survey looks to me like something that would live in tools/, in which case it is reasonable to depend on a port. We keep python scripts there, for example. The mailing list thread about cmb(1) and libcmb seemed to conclude with the suggestion that they be added as a port, but I can't seem to find one.

Hi markj,

Yes, it was suggested that I make a port first.

However, everybody seems to be ignoring what I am saying regarding the utility of this tool being equitable to seq, jot, and friends.

Just yesterday, I did the following:

cmb -d / {a..z} | xargs stat 2>&1 | dpv -l -

The purpose was to generate millions of stat errors so that I could work on some filesystem patches to improve the performance of stat in nfsd.

Could I have used jot? Maybe, but it would have been more difficult.
Could I have used seq? Maybe, but same problems as jot. I needed discretely unique test matter.

I have been ignoring the suggestion to put it into ports because not one single person has even addressed the use-cases for base.

How would one make an argument for jot or seq being in base? If you pretend that they are not in base, what arguments would you use to introduce them?

cmb is kind of like that -- it has a million uses. Asking why we should have it in base is kind of like asking why we should have bc in base.

cmb is a math tool. A very powerful tool that fills a myriad requirements, not to mention the following use-case which I will once-again reiterate that has once again been ignored ...

I don't care about the build option survey. It was an example.

I care about using this for combinatoric combination of ports given various options.

Let's talk about dialog4ports -- a tool that lives in ports that is required by ports. So many times this has caused me headaches and I really don't want to go down that road. It is very frustrating when you get into a situation where ports needs X from ports but you can't compile it because your base and ports frameworks have diverged so you then have to devolve into first updating your base shared Mk files relied-on by ports. It's real shit-show.

Putting cmb in base will allow it to:
a. solve math problems
b. allow me to work on base enhancements with only base (think Filesystem debugging, filesystem optimizations, memory testing, scheduler profiling, etc.)
c. be usable by ports without being stuck in the quagmire-catch-22 described above

Hi markj,

Yes, it was suggested that I make a port first.

However, everybody seems to be ignoring what I am saying regarding the utility of this tool being equitable to seq, jot, and friends.

Just yesterday, I did the following:

cmb -d / {a..z} | xargs stat 2>&1 | dpv -l -

The purpose was to generate millions of stat errors so that I could work on some filesystem patches to improve the performance of stat in nfsd.

Could I have used jot? Maybe, but it would have been more difficult.
Could I have used seq? Maybe, but same problems as jot. I needed discretely unique test matter.

I have been ignoring the suggestion to put it into ports because not one single person has even addressed the use-cases for base.

How would one make an argument for jot or seq being in base? If you pretend that they are not in base, what arguments would you use to introduce them?

cmb is kind of like that -- it has a million uses. Asking why we should have it in base is kind of like asking why we should have bc in base.

cmb is a math tool. A very powerful tool that fills a myriad requirements, not to mention the following use-case which I will once-again reiterate that has once again been ignored ...

I don't care about the build option survey. It was an example.

I care about using this for combinatoric combination of ports given various options.

Let's talk about dialog4ports -- a tool that lives in ports that is required by ports. So many times this has caused me headaches and I really don't want to go down that road. It is very frustrating when you get into a situation where ports needs X from ports but you can't compile it because your base and ports frameworks have diverged so you then have to devolve into first updating your base shared Mk files relied-on by ports. It's real shit-show.

Putting cmb in base will allow it to:
a. solve math problems
b. allow me to work on base enhancements with only base (think Filesystem debugging, filesystem optimizations, memory testing, scheduler profiling, etc.)
c. be usable by ports without being stuck in the quagmire-catch-22 described above

Regarding the prior discussion, I just see that the original thread on -announce appears to end with you saying that you would make a port. That didn't happen, and since there was some objection to putting cmb and libcmb straight into the base system, we should make sure that those objections won't be raised again after a commit. The right way to do that is to follow up on the lists, like -hackers and -arch, since only a small handful of developers are subscribed to this review.

I understand that cmb is intended to be a general-purpose utility, but that alone is not sufficient for putting it in the base system. jot(1) and seq(1) make for an interesting comparison since seq's functionality is a subset of jot's; seq was added to the base system relatively recently, specifically to make us more compatible with other unix environments. jot predates FreeBSD and comes from a time where a batteries-included approach to shipping an OS was more important than it is today.

I personally think that cmb would be an interesting addition to the base system, but there should be some concrete justification for it to be there. The build option survey is not really a compelling example. A ports target that builds a port with all possible combinations of options seems useful, but is there currently some work in progress to implement that? I understand that having the ports framework depend on a port is painful, but unless the absence of cmb from the base system is currently blocking a useful project, I don't see why this is a strong argument for not making a cmb port. You've written a number of large sh-based components of the base system - could any of them make use of cmb? My point is just that I believe that you could successfully argue for cmb's inclusion in the base system, but the idea first needs to be socialized more fully. A port is a reasonable alternative in the meantime and will make it easy for others to try using cmb.

LGTM for the man page related things.

pstef added a subscriber: pstef.

Looks good to me.

I'm playing with this utility on my stable/13 and I like the idea very much. It feels unixy to me in that the tool is abstract enough for me to apply it to various problems which may be difficult to define beforehand. But I can already see myself using this instead of generating permutations with recursive CTEs in SQL like I sometimes do.

Also, although I'm not sure anyone will find this meaningful, cmb reminds me of a problem I was solving recently at job, feeding a Cassandra table random data:

The table and its keyspace were defined as follows:
CREATE KEYSPACE test WITH REPLICATION = { 'class' : 'SimpleStrategy', 'replication_factor' : 1 };
CREATE TABLE test.base(part text, ord text, fill text, PRIMARY KEY((part), ord));

We feed the table like this:
# base32 -w 2000 < /dev/urandom | cut -b1-3,4-8,9- --output-delimiter=, | cqlsh -u $CASS_USER -e 'COPY test.base FROM STDIN'

Cutting base32 output into columns of arbitrary length gives us control over cardinality of each column; specifically we want to know the upper bound on the number of partitions and the number of rows in each partition. Given a set of k (32 in base32) characters, the number of n-tuples (n characters in a column) is k^n. For example, taking the first 3 letters of each line to use in the partitioning column gives us the upper bound of 32^3 partitions, which is 32768.

Forgive the verbosity and being Ubuntu-specific (base32, cut --output-delimiter, /dev/urandom), but I hope you get the idea: I tend to use unix tools when interacting with other tools or services, databases especially.

By the way, the util and the library seem small enough:

-r-xr-xr-x  1 root  wheel    46K Aug  5 14:17 /usr/bin/indent
-r--r--r--  1 root  wheel    21K Aug 15 17:49 /usr/lib/libcmb.so.0
-r-xr-xr-x  1 root  wheel    31K Aug 15 17:50 /usr/bin/cmb

Hi markj,

Yes, it was suggested that I make a port first.

However, everybody seems to be ignoring what I am saying regarding the utility of this tool being equitable to seq, jot, and friends.

Just yesterday, I did the following:

cmb -d / {a..z} | xargs stat 2>&1 | dpv -l -

The purpose was to generate millions of stat errors so that I could work on some filesystem patches to improve the performance of stat in nfsd.

Could I have used jot? Maybe, but it would have been more difficult.
Could I have used seq? Maybe, but same problems as jot. I needed discretely unique test matter.

I have been ignoring the suggestion to put it into ports because not one single person has even addressed the use-cases for base.

How would one make an argument for jot or seq being in base? If you pretend that they are not in base, what arguments would you use to introduce them?

cmb is kind of like that -- it has a million uses. Asking why we should have it in base is kind of like asking why we should have bc in base.

cmb is a math tool. A very powerful tool that fills a myriad requirements, not to mention the following use-case which I will once-again reiterate that has once again been ignored ...

I don't care about the build option survey. It was an example.

I care about using this for combinatoric combination of ports given various options.

Let's talk about dialog4ports -- a tool that lives in ports that is required by ports. So many times this has caused me headaches and I really don't want to go down that road. It is very frustrating when you get into a situation where ports needs X from ports but you can't compile it because your base and ports frameworks have diverged so you then have to devolve into first updating your base shared Mk files relied-on by ports. It's real shit-show.

Putting cmb in base will allow it to:
a. solve math problems
b. allow me to work on base enhancements with only base (think Filesystem debugging, filesystem optimizations, memory testing, scheduler profiling, etc.)
c. be usable by ports without being stuck in the quagmire-catch-22 described above

Regarding the prior discussion, I just see that the original thread on -announce appears to end with you saying that you would make a port. That didn't happen, and since there was some objection to putting cmb and libcmb straight into the base system, we should make sure that those objections won't be raised again after a commit. The right way to do that is to follow up on the lists, like -hackers and -arch, since only a small handful of developers are subscribed to this review.

I understand that cmb is intended to be a general-purpose utility, but that alone is not sufficient for putting it in the base system. jot(1) and seq(1) make for an interesting comparison since seq's functionality is a subset of jot's; seq was added to the base system relatively recently, specifically to make us more compatible with other unix environments. jot predates FreeBSD and comes from a time where a batteries-included approach to shipping an OS was more important than it is today.

I personally think that cmb would be an interesting addition to the base system, but there should be some concrete justification for it to be there. The build option survey is not really a compelling example. A ports target that builds a port with all possible combinations of options seems useful, but is there currently some work in progress to implement that? I understand that having the ports framework depend on a port is painful, but unless the absence of cmb from the base system is currently blocking a useful project, I don't see why this is a strong argument for not making a cmb port. You've written a number of large sh-based components of the base system - could any of them make use of cmb? My point is just that I believe that you could successfully argue for cmb's inclusion in the base system, but the idea first needs to be socialized more fully. A port is a reasonable alternative in the meantime and will make it easy for others to try using cmb.

I've had time to think about this and I believe the proper justification for being in base is to classify the behavior that it provides as missing functionality in the category of "text expanders/modifiers" which would include (as part of the base system):

glob(3)
fnmatch(3)
ls(1)
sh(1)
jot(1)
seq(1)
expand(1)
rs(1)
pr(1)
awk(1)
sed(1)
col(1)

and arguably even:

vi(1)
ed(1)

and ilk. That is to say that cmb(1) and cmb(3) are ways of taking text and expanding it in a predictable way -- maybe not in a way that is readily obvious to most people, but I would argue that the functionality performed by tbl(1) is not readily obvious to most people (and in-fact may never be used directly by the majority of people).

That being said, you are right that I should find some use-case for it in bsdconfig or some other tool already living in base first to demand its import to the base system.

In D16132#626980, @gbe wrote:

LGTM for the man page related things.

Thanks!

Looks good to me.

I'm playing with this utility on my stable/13 and I like the idea very much. It feels unixy to me in that the tool is abstract enough for me to apply it to various problems which may be difficult to define beforehand. But I can already see myself using this instead of generating permutations with recursive CTEs in SQL like I sometimes do.

Also, although I'm not sure anyone will find this meaningful, cmb reminds me of a problem I was solving recently at job, feeding a Cassandra table random data:

The table and its keyspace were defined as follows:
CREATE KEYSPACE test WITH REPLICATION = { 'class' : 'SimpleStrategy', 'replication_factor' : 1 };
CREATE TABLE test.base(part text, ord text, fill text, PRIMARY KEY((part), ord));

We feed the table like this:
# base32 -w 2000 < /dev/urandom | cut -b1-3,4-8,9- --output-delimiter=, | cqlsh -u $CASS_USER -e 'COPY test.base FROM STDIN'

Cutting base32 output into columns of arbitrary length gives us control over cardinality of each column; specifically we want to know the upper bound on the number of partitions and the number of rows in each partition. Given a set of k (32 in base32) characters, the number of n-tuples (n characters in a column) is k^n. For example, taking the first 3 letters of each line to use in the partitioning column gives us the upper bound of 32^3 partitions, which is 32768.

Forgive the verbosity and being Ubuntu-specific (base32, cut --output-delimiter, /dev/urandom), but I hope you get the idea: I tend to use unix tools when interacting with other tools or services, databases especially.

By the way, the util and the library seem small enough:

-r-xr-xr-x  1 root  wheel    46K Aug  5 14:17 /usr/bin/indent
-r--r--r--  1 root  wheel    21K Aug 15 17:49 /usr/lib/libcmb.so.0
-r-xr-xr-x  1 root  wheel    31K Aug 15 17:50 /usr/bin/cmb

Thank you pstef! I am going to try and think up a way to incorporate this into something already in base, like sysrc, bsdconfig, bsdinstall, or something else I have written to help bring it in.

pstef requested changes to this revision.Aug 25 2023, 5:57 PM

As of stable/14 this no longer compiles for me due to

/usr/src/lib/libcmb/cmb.c:854:6: error: invalid argument type 'void' to unary expression
        if (!BN_zero(count))
            ^~~~~~~~~~~~~~~
/usr/src/lib/libcmb/cmb.c:1032:7: error: invalid argument type 'void' to unary expression
                if (!BN_zero(seq))
                    ^~~~~~~~~~~~~
2 errors generated.
This revision now requires changes to proceed.Aug 25 2023, 5:57 PM
pauamma_chezdork.com added inline comments.
lib/libcmb/cmb.3
2

Needs SPDX licence ID for new files.

26

No longer required, and IIRC being removed. (Can someone confirm the latter?)

28

Bump.

41

Other than in passing in the description of CMB_OPT_EMPTY (special case), I see no description of this function or cmb_count_bn. Is the omission deliberate?

152
165
197
215

For consistency with "at most" below

247
266

I guess that should be 15.0 now.

usr.bin/cmb/cmb.1
2

SPDX license ID for new files.

26

No longer needed.

28

Bump.

62
63
64
66
73
77
98
112
116

Maybe add that the limit is 2^32-1 for people who don't have powers of 2 memorized and to explain why it's that.

217
241
374
394

I guess it's 15.0 now.

Oh, I missed that there was a new review a couple years ago. I am more than happy to dust this off. I was just talking about this to a coworker last night at the company holiday party.

Oh, this is cool!

usr.bin/cmb/cmb.1
2

We updated style.9 and https://docs.freebsd.org/en/articles/license-guide/ with the current preferred text and format

69

Macros in the width field are unpredictable

usr.bin/cmb/cmb.1
2

Thank you so much for the update and pointer

As of stable/14 this no longer compiles for me due to

/usr/src/lib/libcmb/cmb.c:854:6: error: invalid argument type 'void' to unary expression
        if (!BN_zero(count))
            ^~~~~~~~~~~~~~~
/usr/src/lib/libcmb/cmb.c:1032:7: error: invalid argument type 'void' to unary expression
                if (!BN_zero(seq))
                    ^~~~~~~~~~~~~
2 errors generated.

Thank you so much.

Here's what I have been doing lately, but need to really determine which version of OpenSSL that changed the BN_zero() function from returning something to returning nothing.

diff
--- a/depend/libcmb/cmb.c
+++ b/depend/libcmb/cmb.c
@@ -851,8 +851,12 @@ cmb_count_bn(struct cmb_config *config, uint32_t nitems)
 	/* Initialize count */
 	if ((count = BN_new()) == NULL)
 		return (NULL);
+#if 0
 	if (!BN_zero(count))
 		goto cmb_count_bn_return;
+#else
+	BN_zero(count);
+#endif
 
 	/* If entire set is requested, return 2^N[-1] */
 	if ((setinit == 1 && setdone == nitems) ||
@@ -1029,8 +1033,12 @@ cmb_bn(struct cmb_config *config, uint32_t nitems, char *items[])
 	if (seq == NULL) {
 		if ((seq = BN_new()) == NULL)
 			goto cmb_bn_return;
+#if 0
 		if (!BN_zero(seq))
 			goto cmb_bn_return;
+#else
+		BN_zero(seq);
+#endif
 	}
 
 	/* Show the empty set consisting of a single combination of no-items */

I'm working on updating this to incorporate the suggestions from folks.

Just taking a quick pass after you pointed me at the review -- I really like this idea -- solid :)!

lib/libcmb/cmb.c
855–856

OpenSSL 3 made this void. Unless you need to support OpenSSL 1.x, or libreSSL, I would just nuke the check.

  1. The FreeBSD project doesn't support any non-3.x libraries in non-EOL versions of FreeBSD. FreeBSD 13 was the last version that shipped OpenSSL 1.x.
1033–1034
lib/libcmb/tests/test3.c
27–32

(not compile-tested)
Please delete the RCS keywords in the review. @imp dropped them a few years ago, because they had diminishing returns with git and were never enabled on the main FreeBSD repos.

usr.bin/cmb/Makefile
11–15

Should this ever work without libcrypto? AFAICT, this relies specifically on libcrypto-provided algorithms/primitives, so you can simplify this Makefile and a few others.

usr.bin/cmb/cmb.c
275

I think it's save to say that you should always have bn.h and libcrypto when using this tool/library, right?

278

ERR_get_error and ERR_error_string could provide really helpful info on error. If you'd like me to go into more detail on how to use those APIs, please let me know.

292–293

Is there a better diagnostic we could feed back to the end-user with this exit string?

301–302

I'm kind of surprised that a printf extension was never developed for appending strerror(errno) to strings. That being said, you could use err(..) instead!

Side question: is there a better diagnostic we could feed back to the end-user with this exit string, e.g., "invalid range given"?

lib/libcmb/cmb.c
257–259
297

This avoids the memory leak on error.

lib/libcmb/cmb.h
291

The nitems symbol would conflict with the macro in sys/param.h with the same name. I would use a different variable name like len.
Also, size_t avoids 32-bit overflow on 64-bit architectures.

I would steer clear of naming variables nitems in the code because we have a macro that is named that already in sys/param.h.

lib/libcmb/cmb.c
126–128

style(9).

lib/libcmb/cmb.h
325–326

sprintf use: is cmb_transform_find_buf always guaranteed to be however many characters/codepoints wide in order to accept the maximum value that can be provided by cmd_transform_precision.

327–328

strcmp use: potential security concern when using this function if the caller can pass arbitrary buffers in as it could result in illegal memory accesses (buffer overflows/code execution). It would be a good idea to use strncmp instead wherever possible to avoid this.

dteske retitled this revision from New cmb(3) library and cmb(1) utility to cmb(1) / cmb(3): import combinatorics utility and library.Wed, Jul 29, 2:28 AM
dteske edited the summary of this revision. (Show Details)
dteske edited the test plan for this revision. (Show Details)
dteske marked 13 inline comments as done.

Address review feedback and modernize for current FreeBSD.

  • Rename nitems -> n_items (sys/param.h clash); keep uint32_t item counts (domain bound / EFBIG; non-BN limited by uint64_t combo counts).
  • cmb_parse: reallocf + shared return path; fix inverted fstat sense.
  • CMB_TRANSFORM_EQ_FIND: snprintf/strncmp/reallocf; find_buf sized via snprintf(NULL,0,...) before format.
  • openssl_err() via ERR_get_error / ERR_error_string_n; bare BN_zero.
  • Prefer err(3) where errno is set; fix -P diagnostic (was -n).
  • Drop RCS/$FreeBSD$; SPDX; HISTORY -> Fx 16.0.
  • Tests: PLAIN_TESTS_C under /usr/tests/lib/libcmb; test4 uses bsdpv(1); clearer RESULT output on test2/test3/test5.
  • Sync cmb(1)/libcmb versions at 3.10.0.

Note: left libcrypto optional (and the tools always built). Without
OpenSSL we stay on 64-bit counts; -v shows whether this binary was
built with OpenSSL. -o still forces the non-bn(3) path when crypto is
present.

lib/libcmb/cmb.h
291

Thanks, I went with n_items instead of len to prevent confusion of what the count holds.

On size_t: keeping uint32_t on purpose. n_items is a bounded item count (cmb_parse already caps at 0xffffffff / EFBIG), and the non-BN path is limited by uint64_t combination counts long before a 32-bit item index is the problem. BN is for the sequence / combo count, not for a larger input cardinality — those APIs still take uint32_t n_items.

325–326

Yes. Immediately above, len is computed with snprintf(NULL, 0, "%.*Lf", cmb_transform_precision, total) + 1, and cmb_transform_find_buf is grown with realloc when len exceeds cmb_transform_find_buf_size. If the realloc fails we error out before the sprintf, so by the time we format, the buffer is at least len bytes — sized for that precision and value, not a fixed maximum.

usr.bin/cmb/Makefile
11–15

Yes, it works without crypto. Without it we are limited to 64-bit integers, which is perfectly valid for “small” sets. cmb -v advertises whether the build was compiled with crypto so the limitation is clear. With crypto, -o still forces the non-OpenSSL execution path.

usr.bin/cmb/cmb.c
275

Not quite — bn.h / libcrypto are optional. Without them we stay on the 64-bit path (fine for small sets). With them we get bn(3) for larger counts. cmb -v shows which build you have, and -o can still force the non-OpenSSL path when crypto is present.

278

Great suggestion — done in the upcoming update. Those “OpenSSL Error?!” errx paths now call a small openssl_err() helper that uses ERR_get_error / ERR_error_string_n. Thanks for the offer on the APIs; that was enough to wire it up.

292–293

Yes, I went with:

err(EXIT_FAILURE,
    "-i: invalid start `%s'", optarg);
dteske marked 27 inline comments as done.

Address additional inline comments

Mark more inline comments as done

Mark paumma's request to add note that 4294967295 == 2^32-1 as done

Document transformation macros and add a sum-to-target test.

  • cmb(3): split cmb() / cmb_count() into separate paragraphs so the following cmb_bn() / cmb_count_bn() note reads as their counterparts (pauamma).
  • cmb(3): document CMB_TRANSFORM_* / cmb_xitem / find globals, with a worked example matching cmb -X add -F; add SEE ALSO.
  • tests: add test6 (CMB_TRANSFORM_OP_FIND(+, …) for combinations of {1,2,3} that sum to 4).

Mark last inline as done (pauamma)

For example, the build-option survey is not trying to solve an equation but test for combinations of build-options that break the build when combined together.

This is a cool idea.

You can do it much faster actually, as each build with n options tests n(n-1) option pairs at the same time, so only O(n) builds are needed to validate all pairs.

I had explored this topic at KIT in the context of SAT solvers as the “clause reconstruction problem.” Each build switch is a variable in a CNF formula and each tuple that fails the build is a clause. There's an oracle (running the build) where you enter an assignment of the variables and the oracle either says “SAT” (build succeeds) or gives you a clause that was not satisfied (a tuple of options causing the build to fail). It is furtherly known that each clause has no more than some k literals (i.e. we disregard failures caused by the incidence of more than k options). The goal was to design a solver that would try to reconstruct the irredundant CNF formula (i.e. find all conflicting option tuples) using as few calls to the oracle as possible. It's surprisingly hard and we never made much inroads into finding a good strategy for when most of the search space is SAT (if the search space is UNSAT then you terminate when a SAT solver proves the currently found clause set UNSAT).

Let me know if you are interested in working on this topic further.