rosejn/cortex

Solver research direction

Open

#254 opened on Dec 28, 2017

View on GitHub
 (5 comments) (0 reactions) (0 assignees)Clojure (1,269 stars) (109 forks)batch import
harderhelp wanted

Description

https://arxiv.org/abs/1710.09278

We demonstrate this exponential gain by comparing a sequential MatLab implementation of our solver with the winners of the 2016 Max-SAT competition on a variety of hard optimization instances. We show empirical evidence that our solver scales linearly with the size of the problem, both in time and memory, and argue that this property derives from the collective behavior of the simulated physical circuit. Our approach can be applied to other types of optimization problems and the results presented here have far-reaching consequences in many fields.

Contributor guide

Tech stack
None
Domain
machine learning
Issue type
research
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
5
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
over 1 week
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
stale
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
unclear
Prerequisites
Understanding of Max SAT problemsFamiliarity with the referenced paperKnowledge of ClojureBackground in optimization algorithms
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
10
Research direction
This issue proposes implementing a Max SAT solver based on the paper 'The Divide and Conquer Approach to Max SAT' (arXiv:1710.09278). The first step is to review the paper and understand the algorithm. Then, a prototype should be developed in the cortex framework, likely in Clojure. The implementation should be evaluated against existing Max SAT benchmarks.