Recent searches

No recent searches

Search options

Only available when logged in.
toad.social is one of the many independent Mastodon servers you can use to participate in the fediverse.
Mastodon server operated by David Troy, a tech pioneer and investigative journalist addressing threats to democracy. Thoughtful participation and discussion welcome.

Administered by:

Server stats:

251
active users

toad.social: AboutProfiles directoryPrivacy policy

Mastodon: AboutGet the appKeyboard shortcutsView source codev4.4.1

#z3

0 posts0 participants0 posts today
*
🇺🇦 haxadecimal

A few months ago I tried to write a Binate Covering Problem (BCP) solver, and haven't yet gotten it working.
But today I realized that writing one is a waste of time. BCP can be solved by a Max-SAT solver, and a huge amount of effort has been invested by very smart people to make those work efficiently. My feeble attempt at a BCP solver couldn't possibly do better.
Here's Python code to solve BCP using Z3's Python bindings:
github.com/brouhaha/bcp-z3-pyt
#BCP #BinateCoveringProblem #SAT #Z3

Binate Covering Problem solver using the Z3 SMT solver Python API - brouhaha/bcp-z3-python
GitHubGitHub - brouhaha/bcp-z3-python: Binate Covering Problem solver using the Z3 SMT solver Python APIBinate Covering Problem solver using the Z3 SMT solver Python API - brouhaha/bcp-z3-python
cohan

It seems like the #TimeOfFlowers #season has barely begun and I'm already hopelessly behind on sharing photos! Things move fast at this time of year, new things opening every day or so, previous waves of flowering wrapping up.. These are from 10 days ago, some finished or on the way out.. White Draba dedeana Yellow Draba aizoides and D. bruniifolia ssp olympica. Tulipa urumiensis (or something..) #garden #RockGarden #spring #NaturalGardening #Alberta #Canada #z3

ALTA

Long Hei Matthew Lam from Monash University has given the oral presentation titled A Closer Look at Tool-based Logical Reasoning with #LLMs: The Choice of Tool Matters.

In this paper, he fills the gaps in the comparison between symbolic solvers, including #Z3, #Pyke, and
#Prover9 with #LLMs augmented.

Nadiah Kristensen

I recently read a paper by Kleshnina and others and used it to teach myself some evolutionary game theory techniques.

This is a little obscure, so I'll thread below about why this topic matters for humans and the environment 🧵

nadiah.org/2024/11/20/kleshnin

Nadiah Pardede Kristensen · Check if an iterated Prisoner’s Dilemma strategy is a subgame perfect Nash equilibriumI recently read a paper by Kleshnina et al. (2023), The effect of environmental information on evolution of cooperation in stochastic games, which provided an opportunity to teach myself about how to analyse iterated games. In particular, the problem they investigated admits 64 possible scenarios with 256 possible strategies each, and I was interested in writing code that could automate the analysis. The solution I eventually landed on (Github repo) used a combination of SymPy, NetworkX, SageMath, the Z3 Theorem Prover, and PyEDA for Boolean minimisation, but I think my approach could be improved.
#GameTheory#PrisonersDilemma#iteratedGame
*
Mark Gritter

A nice little graph coloring problem, solved (or rather shown to be unsatisfiable) using #Z3 :
quora.com/Is-it-possible-for-a

My interpretation of what was asked: take the dodecahedron graph and make it directed (by doubling edges):
* Every vertex is the source of one red, one green, and one blue arrow.
* Every vertex is the target of one red, one green, and one blue arrow.
* The two opposite-direction arrows between vertices must be of different colors.

QuoraIs it possible for all the vertices of a dodecahedron to have coloured arrows of red, blue and green, pointing to and from them along the...Mark Gritter's answer: I think what you mean is that: * Every vertex is the source of one red, one green, and one blue arrow. * Every vertex is the target of one red, one green, and one blue arrow. * Every edge has exactly two opposite-direction arrows, which must be of different colors. Unde...
Mark Gritter

This approach to writing a #Z3 model is not gonna cut it. (Simulating the Rogue room generation algorithm and bogged down on the very first nested loop.) Am I gonna have to write my own DSL that is compiled to Z3?

There's got to be a better way to generate the model. My mental picture is as a tree where edges correspond to computational steps in the original algorithm -- maybe I can make that explicit in some form. Write successor functions for each possible state.

Achim D. Brucker

We have an exciting opportunity for a PostDoc
to work applying formal methods to enterprise systems: We will develop
techniques to detect faults and vulnerabilities in complex business-process-driven systems, contributing to
protecting critical workflows such as manufacturing, or logistics.

Apply until the 18th April 2024:
jobs.exeter.ac.uk/hrpr_webrecr

#Fedihire #Job #BPMN #BPL #FormalMethods #AcademicChatter #Security #ITP #Z3 #postdoc #unijobs
#ModelChecking #EnterpriseSecurity

Replied in thread
*
Quincy

@grillchen @SpaceLifeForm

It looks to me as if one could formulate the problem of optimality as a (QF-!)NRA #SMT instance and in principle* decide it with a solver though?

two variables x_i and y_i for the coordinates of every centre

quadratic constraints: distances between centres must be >=1

relate this to the conjectured optimal configuration by asserting smaller max distance from origin

and (check-sat)

* I think #z3 won't be able to do it in any reasonable amount of time (if at all)

Continued thread
Andreas Zeller

Acknowledgments! We thank our families for their support, @BjornerNikolaj@twitter.com for his work on #Z3, @johnregehr@twitter.com for inspiration, Andreas' students at @CISPA@twitter.com for lots of beta testing, and the @FSEconf@twitter.com reviewers for their helpful feedback. Enjoy #ISLa! – Dominic + Andreas

TrendingLive feeds
About