The remainder of the spec is merely
(s/fdef reduce-k-to-3-sat
:args (s/cat :cnf-expression ::cnf-expression)
:ret ::cnf-expression)
(stest/summarize-results (first (stest/test `reduce-k-to-3-sat)))
reduce-k-to-3-sat does something like a 3x magnification of the input.
On Monday, July 4, 2016 at 10:17:59 PM UTC+2, Alex Miller wrote:
>
> This is a common problem with data generators (whether test.check or any
> other generator I know of). In general the problem of "giving me random
> (but not ridiculous) data that will also effectively act as a test" is
> hard. test.check has a number of controls that can be applied; spec exposes
> some of those, provides some other controls (like :gen-max in coll-of etc),
> and allows the ability to override generators either in the spec definition
> or at later points via either name or path. There is a tension between spec
> conciseness and generator robustness and finding the right balance is a bit
> of an art.
>
> If you could share a bit more about how you are testing this, it might
> suggest some other options. Are you generating data with gen/generate or
> gen/sample, using clojure.spec.test/test, or something else?
>
>
> On Monday, July 4, 2016 at 1:19:22 PM UTC-5, Sebastian Oberhoff wrote:
>>
>> I set myself the exercise of converting k-SAT CNF-formulas to 3-SAT
>> formulas, a task that most theoretical computer scientists will be familiar
>> with. For that purpose I defined the spec
>>
>>
>> (s/def ::literal (s/or :symbol symbol? :negated-symbol (s/spec (s/cat :
>> not #{'not} :symbol symbol?))))
>>
>> (s/def ::disjunction (s/spec (s/cat :or #{'or} :literals (s/+
>> ::literal))))
>>
>> (s/def ::cnf-expression (s/spec (s/cat :and #{'and} :disjunctions (s/+
>> ::disjunction))))
>>
>> Examples for this would be
>> '(and (or a b c d) (or e f))
>>
>> '(and (or a b c) (or d) (or e f g h i j))
>>
>> So basically an AND of ORs. However after running some generative tests
>> my computer began getting really hot. The problem here isn't that I am
>> trying to solve an NP-complete problem. I am only testing the reduction. I
>> don't care at this point whether any of these formulas are actually
>> satisfiable. The problem turned out to be that test.check was generating
>> absurdly large CNF-formulas from this spec. I'm talking symbol names ~1000
>> characters long and the overall formula containing ~1000 symbols.
>> I could probably mend this problem by overwriting the appropriate
>> generators. But seeing how this is the very first spec I'm using for
>> generative testing and I'm already running into this after just 3 lines of
>> specs, I can easily imagine that I'd end up peppering every spec I'll ever
>> write with custom generators saying "this list should only contain 50
>> elements", "this string should not contain emoji's" etc... And even that
>> might not suffice once I begin composing specs into larger hierarchies
>> since the size of the test cases would grow exponentially in the number of
>> layers of abstraction.
>> Is there a more workable solution for this problem?
>>
>
--
You received this message because you are subscribed to the Google
Groups "Clojure" group.
To post to this group, send email to [email protected]
Note that posts from new members are moderated - please be patient with your
first post.
To unsubscribe from this group, send email to
[email protected]
For more options, visit this group at
http://groups.google.com/group/clojure?hl=en
---
You received this message because you are subscribed to the Google Groups
"Clojure" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
For more options, visit https://groups.google.com/d/optout.
