Skip to content
GitLab
  • Menu
Projects Groups Snippets
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
    • Contribute to GitLab
  • Sign in
  • sat4j sat4j
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
  • Issues 57
    • Issues 57
    • List
    • Boards
    • Service Desk
    • Milestones
  • Merge requests 1
    • Merge requests 1
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
  • Deployments
    • Deployments
    • Environments
    • Releases
  • Packages & Registries
    • Packages & Registries
    • Container Registry
  • Monitor
    • Monitor
    • Incidents
  • Analytics
    • Analytics
    • Value stream
    • CI/CD
    • Repository
  • Wiki
    • Wiki
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • SAT4J
  • sat4jsat4j
  • Merge requests
  • !5

Prefbones

  • Review changes

  • Download
  • Email patches
  • Plain diff
Open Jonas Bollgrün requested to merge apoth/sat4j:prefbones into master Jan 01, 2020
  • Overview 33
  • Commits 10
  • Pipelines 8
  • Changes 6

This fork contains two improvements in the domain of backbones

  1. Implementation of Prefbones, proposed in "A Preference-based Approach to Backbone Computation with Application to Argumentation" by Previti and Järvisalo. This algorithm generally runs faster for real world instances, but slower for difficult instances like those used in the SAT competitions. This is available as pbb() in the Backbone class.
  2. Implementation of a stronger model reduction for the purpose of backbone computation, which is the intersection of all implicants in the found model (also known as unrotatable literals). This reduction disqualifies more literals per SAT call (depending on the instance of course) and also usually executes much faster than the prime implicant computation. This approach was described in "Algorithms for computing backbones of propositional formulae" by Marques-Silva,Janota and Lynce with an implementation hint described in section 4.1 of "Towards backbone computing: A Greedy-Whitening based approach" by Zhang,Zhang,Pu,Song and Li. I changed the backbone algorithms BB,IBB and my own to always use this reduction.

This code is an optimized reimplementation of what I created for my own master thesis (https://github.com/apothecarius/masterthesis). Feel free to give feedback before accepting this code into the main repository. I also plan to investigate whether it can be predicted reliably whether a preference based algorithm runs faster than ordinary algorithms (BB/IBB) by looking at the number of conflicts in the first SAT call.

Assignee
Assign to
Reviewer
Request review from
Time tracking
Source branch: prefbones