Lipen
/ sets-jaccard.mzn
Created
September 19, 2025 16:29
MiniZinc model for Jaccard similarity problem data generation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| int: n_objects = 9; | |
| int: n_sets = 6; | |
| int: min_set_size = 3; | |
| int: max_set_size = 4; | |
| set of int: OBJ = 1..n_objects; | |
| set of int: SET = 1..n_sets; | |
| array[SET, OBJ] of var bool: membership; | |
| array[SET] of var min_set_size..max_set_size: set_size; | |
| array[SET, SET] of var 0.0 .. 1.0: jaccard; |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import org.junit.jupiter.api.Test | |
| fun <T> combine(sequences: List<Sequence<T>>): Sequence<List<T>> = sequence { | |
| if (sequences.isEmpty()) return@sequence | |
| if (sequences.size == 1) { | |
| for (x in sequences[0]) { | |
| yield(listOf(x)) | |
| } | |
| return@sequence |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| import mmap | |
| import tqdm | |
| def parse_binary_drat_mmap(path): | |
| with open(path, "rb") as f: | |
| with mmap.mmap(f.fileno(), 0, access=mmap.ACCESS_READ) as mm: | |
| state = 0 | |
| # state = 0 -- reading the mode: b'a' or b'd' | |
| # state = 1 -- reading the clause | |
| mode = None # "a" or "d", for user |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| #!/usr/bin/env python | |
| # coding: utf-8 | |
| def quicksort(A, p=0, r=None): | |
| if r is None: | |
| r = len(A) - 1 | |
| if p < r: | |
| q = partition(A, p, r) | |
| quicksort(A,p,q-1) | |
| quicksort(A,q+1,r) |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| %%% Graph Coloring | |
| %% Constants. | |
| int: V; | |
| int: E = length(edges1d) div 2; | |
| int: k; | |
| set of int: NODES = 1..V; | |
| set of int: EDGES = 1..E; | |
| set of int: COLORS = 1..k; |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| ; EXPECT: unsat | |
| ; COMMAND-LINE: --lang=sygus2 | |
| (set-logic ALL) | |
| (synth-fun f ((x Bool) (y Bool) (z Bool)) Bool | |
| ((Start Bool)) ( | |
| (Start Bool ( | |
| x y z | |
| (not Start) | |
| (and Start Start) |
Lipen
/ minimum-vertex-cover.py
Created
August 20, 2020 07:56
Minimum Vertex Cover using RC2 MaxSAT Solver from PySAT
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from pysat.examples.rc2 import RC2 | |
| from pysat.formula import WCNF, IDPool | |
| vpool = IDPool(start_from=1) | |
| def cover(v): | |
| return vpool.id(f'cover@{v}') | |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| from pysat.formula import CNF, IDPool | |
| from pysat.solvers import Minisat22 as Solver | |
| from enum import Enum | |
| NodeType = Enum("NodeType", "VAR AND OR NOT") | |
| class BFSynthesizer: | |
| def __init__(self, n: int, tt: str, P: int): | |
| assert len(tt) == 2 ** n, "Incorrect truth table size" |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| package examples.einstein | |
| import com.github.lipen.satlib.op.exactlyOne | |
| import com.github.lipen.satlib.op.imply | |
| import com.github.lipen.satlib.op.implyOr | |
| import com.github.lipen.satlib.solver.MiniSatSolver | |
| import com.github.lipen.satlib.solver.Solver | |
| import com.github.lipen.satlib.solver.newDomainVarArray | |
| import com.github.lipen.satlib.utils.DomainVarArray | |
| import com.github.lipen.satlib.utils.convert |
NewerOlder