•  19
    Clause tableaux for maximum and minimum satisfiability
    with Josep Argelich, Felip Manyà, and Joan Ramon Soler
    Logic Journal of the IGPL 29 (1): 7-27. 2021.
    The inference systems proposed for solving SAT are unsound for solving MaxSAT and MinSAT, because they preserve satisfiability but not the minimum and maximum number of clauses that can be falsified, respectively. To address this problem, we first define a clause tableau calculus for MaxSAT and prove its soundness and completeness. We then define a clause tableau calculus for MinSAT and also prove its soundness and completeness. Finally, we define a complete clause tableau calculus for solving b…Read more
  •  11
  •  10
    A resolution calculus for MinSAT
    with Fan Xiao and Felip Manyà
    Logic Journal of the IGPL 29 (1): 28-44. 2021.
    The logical calculus for SAT are not valid for MaxSAT and MinSAT because they preserve satisfiability but not the number of unsatisfied clauses. To overcome this drawback, a MaxSAT resolution rule preserving the number of unsatisfied clauses was defined in the literature. This rule is complete for MaxSAT when it is applied following a certain strategy. In this paper we first prove that the MaxSAT resolution rule also provides a complete calculus for MinSAT if it is applied following the strategy…Read more
  •  7
    Vlsi architecture design for bnn speech recognition
    with Jia-Ching Wang and Jhing-Fa Wang
    Signal Processing, Pattern Recognition, and Applications. 2003.
  •  6
    Clause vivification by unit propagation in cdcl sat solvers
    with Fan Xiao, Mao Luo, Felip Manyà, Zhipeng Lü, and Yu Li
    Artificial Intelligence 279 (C): 103197. 2020.
  •  4
    Optimizing with minimum satisfiability
    with Zhu Zhu, Felip Manyà, and Laurent Simon
    Artificial Intelligence 190 (C): 32-44. 2012.