#BooleanSatisfiability

2025-02-03

Happy Monday everyone!

Here's something to brighten up the start of your week: a paper about solving mathemusical problems with ILP and SAT, from our latest issue:

Computing aperiodic tiling rhythmic canons via SAT models
link.springer.com/article/10.1

To make this Monday extra sweet: the authors use MapleSAT!

#Mathematics
#Music
#ConstraintProgramming
#AI
#Rhythm
#AcademicMastodon
#BooleanSatisfiability
#AperiodicTiling
#MapleSAT
#ILP
#CombinatorialAlgorithms
#ArtificialIntelligence

2024-02-29

Survey of Theme One Program • 6
inquiryintoinquiry.com/2024/02

This is a Survey of resources for the Theme One Program I worked on all through the 1980s. The aim was to develop fundamental algorithms and data structures for integrating empirical learning with logical reasoning. I had earlier developed separate programs for basic components of those tasks, namely, two‑level formal language learning and propositional constraint satisfaction, the latter using an extension of C.S. Peirce's logical graphs as a syntax for propositional logic. Thus arose the question of how well it might be possible to get “empiricist” and “rationalist” modes of operation to cooperate. The long-term vision is the design and implementation of an Automated Research Tool able to double as a platform for Inquiry Driven Education.

Please follow the above link for the full set of resources.
A collection of articles on the core ideas is linked below.

Wiki Hub —

Theme One Program • Overview
oeis.org/wiki/Theme_One_Progra

Documentation —

Theme One Program • Pascal Source Code
academia.edu/5210987/Theme_One

Theme One Program • User Guide
academia.edu/5211369/Theme_One

Theme One Program • Exposition
oeis.org/wiki/Theme_One_Progra

Applications —

Applications of a Propositional Calculator • Constraint Satisfaction Problems
academia.edu/4727842/Applicati

Exploratory Qualitative Analysis of Sequential Observation Data
oeis.org/wiki/User:Jon_Awbrey/

References —

An Architecture for Inquiry • Building Computer Platforms for Discovery
academia.edu/1270327/An_Archit

Exploring Research Data Interactively • Theme One : A Program of Inquiry
academia.edu/1272839/Exploring

#Peirce #Logic #LogicalGraphs #ThemeOneProgram
#BooleanSatisfiability #DeclarativeProgramming

Dr. Anna Latouranna@mathstodon.xyz
2023-08-26

Last week, I presented the work I did with prof. Kuldeep Meel and prof. Arunabha Sen at IJCAI 2023.

We showed the benefits of reducing a problem to a computationally harder problem (yes, you read that right!), by demonstrating how it allows us to solve much larger problem instances.

It was so much fun to finally share this work with so many fantastic researchers at IJCAI! Thank you to all organisers for making this conference possible. I'm also super grateful to the reviewers who gave us great feedback!

Please find our paper, slides, poster, a short video, and our open source tool, gismo, here: www.annalatour.nl/publication/2023-08-01-Solving-the-Identifying-Code-Set-Problem-with-Grouped-Independent-Support

#IJCAI2023 #IJCAI #AcademicMastodon #FOSS #PostdocLife #ConstraintProgramming #BooleanSatisfiability #Complexity #AcademicChatter #OpenSource #OpenSourceSoftware

A picture of a conference room with a decor that seems to have been selected by Louis XIV's personal interior decorator, on a day on which he wanted to leave work early to watch a duelling match. I am standing next to a big monitor, with an enormous name badge around my neck, in the middle of explaining something. The slide is the title slide of my presentation, and reads:  Solving the Identifying Code Set Problem with Grouped Independent Support  Anna L.D. Latour, Arunabha Sen and Kuldeep S. Meel  School of Computing, National University of Singapore Computer Science and Engineering Faculty, Arizona State University  IJCAI, 23 August 2023, MacauMe, a young woman with long blonde hair wearing a pink blouse, standing in front of an academic poster, smilingly posing as if I am explaining it to someone. The poster is titled "Solving the Identifying Code Set Problem with Grouped Independent Support", and has a big pink block with white letters in the middle, which reads "by reducing to a computationally harder problem, we can exponentially decrease the encoding size, and solve much larger instances."
Dr. Anna Latouranna@mathstodon.xyz
2023-08-23
Dr. Anna Latouranna@mathstodon.xyz
2023-08-06
2023-05-19

Inquiry Into Inquiry • On Initiative 1
inquiryintoinquiry.com/2022/07

Re: R.J. Lipton and K.W. Regan • Sorting and Proving
rjlipton.wpcomstaging.com/2022

❝GPT‑3 works by playing a game of “guess the next word” in a phrase.
This is akin to “guess the next move” in chess and other games, and
we will have more to say about it.❞

My Observation —
rjlipton.wpcomstaging.com/2022

As a person who struggles on a daily basis to rise to the level of sentience
I've learned it has more to do with beginning than ending this sentence.

Resources —

Survey of Inquiry Driven Systems
inquiryintoinquiry.com/2023/04

Survey of Theme One Program
inquiryintoinquiry.com/2023/03

#Peirce #Logic #Inquiry #InquiryDrivenSystems #InquiryIntoInquiry
#BooleanSatisfiability #ComputationalComplexity #GödelsLostLetter
#AbductionDeductionInduction #IntelligentSystems #GPT #LLM #SAT

Dr. Anna Latouranna@mathstodon.xyz
2023-04-22

Very happy that our paper "Solving the Identifying Code Set Problem with Grouped Independent Support" was accepted to IJCAI 2023!

I did this work together with Prof. Kuldeep Meel and from NUS and Prof. Arunabha Sen from ASU. It was a great pleasure to work with them, and I learned a lot from both of them during this project. We have some ideas for further research, so I hope this story is to be continued...

Shout-out and many thanks to @msoos for his last-minute help to fix a bug in the code!

This is my first accepted conference paper that I worked on without my PhD advisor Dr. Siegfried Nijssen Dr. Behrouz Babaki. It felt a little bit weird doing this without them, but I guess that's part of the job.

Many thanks to everyone who contributed to this work in conversation, encouragement, feedback, or just simply making our office a nice place to work at 🙂

If you're planning to attend IJCAI in Macau, and want to meet up, let me know!

#IJCAI #IJCAI2023 #AcademicMastodon #AcademicChatter #PostdocLife #ArtificialIntelligence #AI #CombinatorialOptimisation #BooleanSatisfiability

2023-04-20

Survey of Theme One Program
inquiryintoinquiry.com/2023/03

This is a Survey of resources for the Theme One Program I worked on all through the 1980s. The aim was to develop fundamental algorithms and data structures for integrating empirical learning with logical reasoning. I had earlier developed separate programs for basic components of those tasks, namely, 2-level formal language learning and propositional constraint satisfaction, the latter using an extension of C.S. Peirce's logical graphs as a syntax for propositional logic. Thus arose the question of how well it might be possible to get “empiricist” and “rationalist” modes of operation to cooperate. The long-term vision is the design and implementation of an Automated Research Tool able to double as a platform for Inquiry Driven Education.

Please follow the above link for the full set of resources. An initial sample is linked below.

Wiki Hub —

Theme One Program • Overview
oeis.org/wiki/Theme_One_Progra

Documentation —

Theme One Program • Pascal Source Code
academia.edu/5210987/Theme_One

Theme One Program • User Guide
academia.edu/5211369/Theme_One

Theme One Program • Exposition
oeis.org/wiki/Theme_One_Progra

Applications —

Applications of a Propositional Calculator • Constraint Satisfaction Problems
academia.edu/4727842/Applicati

Exploratory Qualitative Analysis of Sequential Observation Data
oeis.org/wiki/User:Jon_Awbrey/

References —

An Architecture for Inquiry • Building Computer Platforms for Discovery
academia.edu/1270327/An_Archit

Exploring Research Data Interactively • Theme One : A Program of Inquiry
academia.edu/1272839/Exploring

#Peirce #Logic #LogicalGraphs #ThemeOneProgram #IdeaProcessor
#BooleanSatisfiability #CactusLanguage #DeclarativeProgramming

Dr. Anna Latouranna@mathstodon.xyz
2022-11-23

The results of the 2022 Model Counting competition have been published! github.com/msoos/model-countin

Thanks to Markus Hecher and Johannes Fichte for organising, and thanks to @msoos for uploading.

Now go play with those data and improve your counters!

#PropositionalModelCounting #ModelCounting #BeyondNP #AI #BooleanSatisfiability #FormalMethods #ArtificialIntelligence #Reasoning #Counting #ModelCounting

Dr. Anna Latouranna@mathstodon.xyz
2022-11-23

@cjmuise @terri Creating a Mosaic Knitting pattern generator could be an interesting place to start. There are quite some limitations to mosaic knitting patterns, and they are typically geometric. It could be an interesting challenge to capture the rules of mosaic knitting into a CNF and have a solver generate solutions, then visualise them as patterns and allow the user to select one they like?

#knitting #geometry #programming #SATSolving #BooleanSatisfiability

Client Info

Server: https://mastodon.social
Version: 2025.07
Repository: https://github.com/cyevgeniy/lmst